21.1. 逻辑模型🔗

从概念上讲，Lean 将项的评估或减少与副作用的执行区分开来。期限缩减由 β 和 δ 等规则指定，这些规则可能随时随地发生。 Lean 的逻辑中抽象地描述了必须按正确顺序执行的副作用。当程序运行时，Lean运行时系统负责实际执行所描述的效果。

IO α 类型是一个进程的描述，通过执行副作用，该进程应该返回 α 类型的值或引发错误。它可以被认为是一个状态单子，其中状态就是整个世界。正如 StateM Nat Bool 类型的值计算 Bool 同时能够改变自然数一样，IO Bool 类型的值在计算 Bool 的同时可能会改变世界。错误处理是通过在其之上分层适当的异常 monad 转换器来完成的。

由于整个世界无法在内存中表示，因此实际实现使用代表其状态的抽象标记。 Lean 运行时系统负责在程序运行时提供初始令牌，每个原始操作接受一个代表世界的令牌，并在完成时返回另一个令牌。这确保了效果以正确的顺序发生，并且它清楚地将副作用的执行与 Lean 术语的约简语义分开。

通过一般递归实现的非终止与 IO 描述的效果分开处理。由于无限循环而无法终止的程序必须定义为 partial 函数。从逻辑角度来看，它们被视为任意常数；不需要 IO。

IO 的一个非常重要的特性是值无法“逃逸”。如果不使用几个明确标记的不安全运算符之一，程序就无法从 IO Nat 中提取纯 Nat。这可以确保保留副作用的正确顺序，并确保具有副作用的程序被明确标记。

21.1.1. `IO`、`EIO` 和 `BaseIO` Monad🔗

有两个 monad 通常用于与现实世界交互的程序：

IO 中的操作可能会引发 IO.Error 类型的异常或修改世界。
BaseIO 中的操作不能引发异常，但它们可以修改世界。

这种区别使得可以通过查看操作的类型签名来判断是否可能出现异常。 BaseIO 操作会根据需要自动升级为 IO。

def

BaseIO (α : Type) : Type
BaseIO (α : Type) : Type

An IO monad that cannot throw exceptions.

def

IO : Type → Type
IO : Type → Type

A monad that supports arbitrary side effects and throwing exceptions of type IO.Error.

IO 是 EIO 的一个实例，其中错误类型是一个参数。特别地，IO 被定义为EIO IO.Error。在某些情况下，例如绑定到非 Lean 库，可以方便地将 EIO 与自定义错误类型一起使用，这可确保在这些操作与其他 IO 操作之间的边界处处理错误。

def

EIO (ε α : Type) : Type
EIO (ε α : Type) : Type

A monad that can have side effects on the external world or throw exceptions of type ε.

BaseIO is a version of this monad that cannot throw exceptions. IO sets the exception type to IO.Error.

def

IO.lazyPure {α : Type} (fn : Unit → α) : IO α
IO.lazyPure {α : Type} (fn : Unit → α) :
  IO α

Creates an IO action that will invoke fn if and when it is executed, returning the result.

def

BaseIO.toIO {α : Type} (act : BaseIO α) : IO α
BaseIO.toIO {α : Type} (act : BaseIO α) :
  IO α

Runs a BaseIO action, which cannot throw an exception, as an IO action.

This function is usually used implicitly via automatic monadic lifting rather than being called explicitly.

def

BaseIO.toEIO {α ε : Type} (act : BaseIO α) : EIO ε α
BaseIO.toEIO {α ε : Type}
  (act : BaseIO α) : EIO ε α

Runs a BaseIO action, which cannot throw an exception, in any other EIO monad.

This function is usually used implicitly via automatic monadic lifting rather being than called explicitly.

def

EIO.toBaseIO {ε α : Type} (act : EIO ε α) : BaseIO (Except ε α)
EIO.toBaseIO {ε α : Type}
  (act : EIO ε α) : BaseIO (Except ε α)

Converts an EIO ε action that might throw an exception of type ε into an exception-free BaseIO action that returns an Except value.

def

EIO.toIO {ε α : Type} (f : ε → IO.Error) (act : EIO ε α) : IO α
EIO.toIO {ε α : Type} (f : ε → IO.Error)
  (act : EIO ε α) : IO α

Converts an EIO ε action into an IO action by translating any exceptions that it throws into IO.Errors using f.

def

EIO.toIO' {ε α : Type} (act : EIO ε α) : IO (Except ε α)
EIO.toIO' {ε α : Type} (act : EIO ε α) :
  IO (Except ε α)

Converts an EIO ε action that might throw an exception of type ε into an exception-free IO action that returns an Except value.

def

IO.toEIO {ε α : Type} (f : IO.Error → ε) (act : IO α) : EIO ε α
IO.toEIO {ε α : Type} (f : IO.Error → ε)
  (act : IO α) : EIO ε α

Runs an IO action in some other EIO monad, using f to translate IO exceptions.

21.1.2. `IO` 中的错误和错误处理🔗

IO monad 中的错误处理使用与任何其他异常 monad 相同的设施。特别是，抛出和捕获异常使用 MonadExceptOf type class 的方法。 IO 中引发的异常的类型为 IO.Error。这种类型的构造函数代表大多数操作系统上发生的低级错误，例如文件不存在。最常用的构造函数是 userError，它涵盖所有其他情况并包含描述问题的字符串。

inductive type

IO.Error : Type
IO.Error : Type

Exceptions that may be thrown in the IO monad.

Many of the constructors of IO.Error correspond to POSIX error numbers. In these cases, the documentation string lists POSIX standard error macros that correspond to the error. This list is not necessarily exhaustive, and these constructor includes a field for the underlying error number.

Constructors

IO.Error.alreadyExists (filename : Option String)
  (osCode : UInt32) (details : String) : IO.Error

The operation failed because a file already exists.

This corresponds to POSIX errors EEXIST, EINPROGRESS, and EISCONN.

IO.Error.otherError (osCode : UInt32) (details : String) :
  IO.Error

Some error not covered by the other constructors of IO.Error occurred.

This also includes POSIX error EFAULT.

IO.Error.resourceBusy (osCode : UInt32) (details : String) :
  IO.Error

A necessary resource was busy.

This corresponds to POSIX errors EADDRINUSE, EBUSY, EDEADLK, and ETXTBSY.

IO.Error.resourceVanished (osCode : UInt32)
  (details : String) : IO.Error

A necessary resource is no longer available.

This corresponds to POSIX errors ECONNRESET, EIDRM, ENETDOWN, ENETRESET, ENOLINK, and EPIPE.

IO.Error.unsupportedOperation (osCode : UInt32)
  (details : String) : IO.Error

An operation was not supported.

This corresponds to POSIX errors EADDRNOTAVAIL, EAFNOSUPPORT, ENODEV, ENOPROTOOPT ENOSYS, EOPNOTSUPP, ERANGE, ESPIPE, and EXDEV.

IO.Error.hardwareFault (osCode : UInt32)
  (details : String) : IO.Error

The operation failed due to a hardware problem, such as an I/O error.

This corresponds to the POSIX error EIO.

IO.Error.unsatisfiedConstraints (osCode : UInt32)
  (details : String) : IO.Error

A constraint required by an operation was not satisfied (e.g. a directory was not empty).

This corresponds to the POSIX error ENOTEMPTY.

IO.Error.illegalOperation (osCode : UInt32)
  (details : String) : IO.Error

An inappropriate I/O control operation was attempted.

This corresponds to the POSIX error ENOTTY.

IO.Error.protocolError (osCode : UInt32)
  (details : String) : IO.Error

A protocol error occurred.

This corresponds to the POSIX errors EPROTO, EPROTONOSUPPORT, and EPROTOTYPE.

IO.Error.timeExpired (osCode : UInt32) (details : String) :
  IO.Error

An operation timed out.

This corresponds to the POSIX errors ETIME, and ETIMEDOUT.

IO.Error.interrupted (filename : String) (osCode : UInt32)
  (details : String) : IO.Error

The operation was interrupted.

This corresponds to the POSIX error EINTR.

IO.Error.noFileOrDirectory (filename : String)
  (osCode : UInt32) (details : String) : IO.Error

No such file or directory.

This corresponds to the POSIX error ENOENT.

IO.Error.invalidArgument (filename : Option String)
  (osCode : UInt32) (details : String) : IO.Error

An argument to an I/O operation was invalid.

This corresponds to the POSIX errors ELOOP, ENAMETOOLONG, EDESTADDRREQ, EILSEQ, EINVAL, EDOM, EBADF ENOEXEC, ENOSTR, ENOTCONN, and ENOTSOCK.

IO.Error.permissionDenied (filename : Option String)
  (osCode : UInt32) (details : String) : IO.Error

An operation failed due to insufficient permissions.

This corresponds to the POSIX errors EACCES, EROFS, ECONNABORTED, EFBIG, and EPERM.

IO.Error.resourceExhausted (filename : Option String)
  (osCode : UInt32) (details : String) : IO.Error

A resource was exhausted.

This corresponds to the POSIX errors EMFILE, ENFILE, ENOSPC, E2BIG, EAGAIN, EMLINK, EMSGSIZE, ENOBUFS, ENOLCK, ENOMEM, and ENOSR.

IO.Error.inappropriateType (filename : Option String)
  (osCode : UInt32) (details : String) : IO.Error

An argument was the wrong type (e.g. a directory when a file was required).

This corresponds to the POSIX errors EISDIR, EBADMSG, and ENOTDIR.

IO.Error.noSuchThing (filename : Option String)
  (osCode : UInt32) (details : String) : IO.Error

A required resource does not exist.

This corresponds to the POSIX errors ENXIO, EHOSTUNREACH, ENETUNREACH, ECHILD, ECONNREFUSED, ENODATA, ENOMSG, and ESRCH.

IO.Error.unexpectedEof : IO.Error

An unexpected end-of-file marker was encountered.

IO.Error.userError (msg : String) : IO.Error

Some other error occurred.

def

IO.Error.toString : IO.Error → String
IO.Error.toString : IO.Error → String

Converts an IO.Error to a descriptive string.

IO.Error.userError is converted to its embedded message. The other constructors are converted in a way that preserves structured information, such as error codes and filenames, that can help diagnose the issue.

def

IO.ofExcept.{u_1} {ε : Type u_1} {α : Type} [ToString ε]
  (e : Except ε α) : IO α
IO.ofExcept.{u_1} {ε : Type u_1}
  {α : Type} [ToString ε]
  (e : Except ε α) : IO α

Converts an Except ε action into an IO action.

If the Except ε action throws an exception, then the exception type's ToString instance is used to convert it into an IO.Error, which is thrown. Otherwise, the value is returned.

def

EIO.catchExceptions {ε α : Type} (act : EIO ε α) (h : ε → BaseIO α) :
  BaseIO α
EIO.catchExceptions {ε α : Type}
  (act : EIO ε α) (h : ε → BaseIO α) :
  BaseIO α

Handles any exception that might be thrown by an EIO ε action, transforming it into an exception-free BaseIO action.

def

IO.userError (s : String) : IO.Error
IO.userError (s : String) : IO.Error

Constructs an IO.Error from a string.

IO.Error is the type of exceptions thrown by the IO monad.

Throwing and Catching Errors

该程序反复要求输入密码，并使用控制流异常。用于异常的语法在所有异常 monad 中都可用，而不仅仅是 IO。当提供的密码不正确时，会引发异常，该异常会被重复密码检查的循环捕获。正确的密码允许控制继续通过检查，终止循环，并重新抛出任何其他异常。

def accessControl : IO Unit := do
  IO.println "What is the password?"
  let password ← (← IO.getStdin).getLine
  if password.trimAscii.copy != "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!"

使用此输入运行时：

stdinpublicinfosecondtrysecret

程序发出：

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

21.1. 逻辑模型🔗

21.1.1. IO、EIO 和 BaseIO Monad🔗

21.1.2. IO 中的错误和错误处理🔗

Constructors

21.1.1. `IO`、`EIO` 和 `BaseIO` Monad🔗

21.1.2. `IO` 中的错误和错误处理🔗