6.1.Β Logical Model

Conceptually, Lean distinguishes evaluation or reduction of terms from execution of side effects. Term reduction is specified by rules such as Ξ² and Ξ΄, which may occur anywhere at any time. Side effects, which must be executed in the correct order, are abstractly described in Lean's logic. When programs are run, the Lean runtime system is responsible for actually carrying out the described effects.

The type IO Ξ± is a description of a process that, by performing side effects, should either return a value of type Ξ± or throw an error. It can be thought of as a state monad in which the state is the entire world. Just as a value of type StateM Nat Bool computes a Bool while having the ability to mutate a natural number, a value of type IO Bool computes a Bool while potentially changing the world. Error handling is accomplished by layering an appropriate exception monad transformer on top of this.

Because the entire world can't be represented in memory, the actual implementation uses an abstract token that stands for its state. The Lean runtime system is responsible for providing the initial token when the program is run, and each primitive action accepts a token that represents the world and returns another when finished. This ensures that effects occur in the proper order, and it clearly separates the execution of side effects from the reduction semantics of Lean terms.

Non-termination via general recursion is treated separately from the effects described by IO. Programs that may not terminate due to infinite loops must be defined as partial functions. From the logical perspective, they are treated as arbitrary constants; IO is not needed.

A very important property of IO is that there is no way for values to β€œescape”. Without using one of a few clearly-marked unsafe operators, programs have no way to extract a pure Nat from an IO Nat. This ensures that the correct ordering of side effects is preserved, and it ensures that programs that have side effects are clearly marked as such.

6.1.1.Β The IO, EIO and BaseIO Monads

There are two monads that are typically used for programs that interact with the real world:

  • Actions in IO may throw exceptions of type IO.Error or modify the world.

  • Actions in BaseIO can't throw exceptions, but they can modify the world.

The distinction makes it possible to tell whether exceptions are possible by looking at an action's type signature. BaseIO actions are automatically promoted to IO as necessary.

πŸ”—def
IO : Type β†’ Type
πŸ”—def
BaseIO : Type β†’ Type

An EIO monad that cannot throw exceptions.

Both IO and BaseIO are instances of EIO, in which the type of errors is a parameter. IO is defined as EIO IO.Error, while BaseIO is defined as EIO Empty. In some circumstances, such as bindings to non-Lean libraries, it can be convenient to use EIO with a custom error type, which ensures that errors are handled at the boundaries between these and other IO actions.

πŸ”—def
EIO (Ξ΅ : Type) : Type β†’ Type
πŸ”—def
IO.lazyPure {Ξ± : Type} (fn : Unit β†’ Ξ±) : IO Ξ±
πŸ”—def
BaseIO.toIO {Ξ± : Type} (act : BaseIO Ξ±) : IO Ξ±
πŸ”—def
BaseIO.toEIO {Ξ± Ξ΅ : Type} (act : BaseIO Ξ±)
    : EIO Ξ΅ Ξ±
πŸ”—def
EIO.toBaseIO {Ξ΅ Ξ± : Type} (act : EIO Ξ΅ Ξ±)
    : BaseIO (Except Ξ΅ Ξ±)
πŸ”—def
EIO.toIO {Ξ΅ Ξ± : Type} (f : Ξ΅ β†’ IO.Error)
    (act : EIO Ξ΅ Ξ±) : IO Ξ±
πŸ”—def
EIO.toIO' {Ξ΅ Ξ± : Type} (act : EIO Ξ΅ Ξ±)
    : IO (Except Ξ΅ Ξ±)
πŸ”—def
IO.toEIO {Ξ΅ Ξ± : Type} (f : IO.Error β†’ Ξ΅)
    (act : IO Ξ±) : EIO Ξ΅ Ξ±

6.1.2.Β Errors and Error Handling

Error handling in the IO monad uses the same facilities as any other exception monad. In particular, throwing and catching exceptions uses the methods of the MonadExceptOf type class. The exceptions thrown in IO have the type IO.Error. The constructors of this type represent the low-level errors that occur on most operating systems, such as files not existing. The most-used constructor is userError, which covers all other cases and includes a string that describes the problem.

πŸ”—inductive type
IO.Error : Type

Imitate the structure of IOErrorType in Haskell: https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType

Constructors

πŸ”—def
IO.Error.toString : IO.Error β†’ String
πŸ”—def
IO.ofExcept.{u_1} {Ξ΅ : Type u_1} {Ξ± : Type}
    [ToString Ξ΅] (e : Except Ξ΅ Ξ±) : IO Ξ±
πŸ”—def
EIO.catchExceptions {Ξ΅ Ξ± : Type} (act : EIO Ξ΅ Ξ±)
    (h : Ξ΅ β†’ BaseIO Ξ±) : BaseIO Ξ±
πŸ”—def
IO.userError (s : String) : IO.Error
Throwing and Catching Errors

This program repeatedly demands a password, using exceptions for control flow. The syntax used for exceptions is available in all exception monads, not just IO. When an incorrect password is provided, an exception is thrown, which is caught by the loop that repeats the password check. A correct password allows control to proceed past the check, terminating the loop, and any other exceptions are re-thrown.

def accessControl : IO Unit := do IO.println "What is the password?" let password ← (← IO.getStdin).getLine if password.trim != "secret" then throw (.userError "Incorrect password") else return def repeatAccessControl : IO Unit := do repeat try accessControl break catch | .userError "Incorrect password" => continue | other => throw other def main : IO Unit := do repeatAccessControl IO.println "Access granted!"

When run with this input:

stdinpublicinfosecondtrysecret

the program emits:

stdoutWhat is the password?What is the password?What is the password?Access granted!

6.1.2.1.Β Constructing IO Errors

πŸ”—def
IO.Error.mkUnsupportedOperation
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkUnsatisfiedConstraints
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkProtocolError
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkResourceBusy
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkResourceVanished
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkNoSuchThing
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkNoSuchThingFile
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkEofError : Unit β†’ IO.Error
πŸ”—def
IO.Error.mkPermissionDenied
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkNoFileOrDirectory
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkTimeExpired
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.fopenErrorToString (gist fn : String)
    (code : UInt32) : Option String β†’ String
πŸ”—def
IO.Error.mkAlreadyExists
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkInvalidArgument
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkHardwareFault
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkResourceExhausted
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkInappropriateType
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkOtherError
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.otherErrorToString (gist : String)
    (code : UInt32) : Option String β†’ String
πŸ”—def
IO.Error.mkInvalidArgumentFile
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkResourceExhaustedFile
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkAlreadyExistsFile
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkIllegalOperation
    : UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkPermissionDeniedFile
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkInterrupted
    : String β†’ UInt32 β†’ String β†’ IO.Error
πŸ”—def
IO.Error.mkInappropriateTypeFile
    : String β†’ UInt32 β†’ String β†’ IO.Error