21.1. 逻辑模型🔗

在概念上，Lean 将项的求值或归约与副作用的执行区分开来。项归约由 β、δ 等规则规定，而这些归约随时可能在任意位置发生。必须按正确顺序执行的副作用，在 Lean 逻辑中以抽象方式描述。程序运行时，由 Lean 运行时系统负责真正实施所描述的副作用。

类型 IO α 描述一个通过执行副作用而运行的过程；该过程要么返回 α 类型的值，要么抛出错误。可以把它看作一种以整个世界为状态的状态单子。正如 StateM Nat Bool 类型的值在计算 Bool 的同时能够修改一个自然数，IO Bool 类型的值在计算 Bool 的同时也可能改变世界。错误处理则通过在其上叠加适当的异常单子变换器来实现。

由于无法在内存中表示整个世界，实际实现使用一个抽象令牌来代表世界的状态。程序运行时，Lean 运行时系统负责提供初始令牌；每个原语动作接收一个代表世界的令牌，并在完成后返回另一个令牌。这既确保副作用按正确顺序发生，也明确区分了副作用的执行与 Lean 项的归约语义。

由一般递归导致的不终止，与 IO 所描述的副作用分开处理。可能因无限循环而不终止的程序必须定义为 partial 函数。从逻辑角度看，它们被视为任意常量，并不需要 IO。

IO 的一项非常重要的性质是，其中的值无法“逃逸”。除非使用少数几个明确标记为不安全的运算符，否则程序无法从 IO Nat 中提取出纯的 Nat。这既保证了副作用的正确顺序，也保证了带副作用的程序会得到明确标记。

21.1.1. `IO`、`EIO` 与 `BaseIO` 单子🔗

与现实世界交互的程序通常使用两种单子：

IO 中的动作可以抛出 IO.Error 类型的异常，也可以修改世界。
BaseIO 中的动作不能抛出异常，但可以修改世界。

这一区分使人们只需查看动作的类型签名，就能判断它是否可能抛出异常。 BaseIO 动作会在需要时自动提升为 IO。

定义

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

不会抛出异常的 IO 单子。

定义

IO : Type → Type
IO : Type → Type

支持任意副作用并可抛出 IO.Error 类型异常的单子。

IO 是 EIO 在错误类型取 IO.Error 时的特例。具体而言，IO 被定义为 EIO IO.Error。在某些场合（例如绑定非 Lean 库），为 EIO 使用自定义错误类型会很方便；这样可确保错误在这些动作与其他 IO 动作的边界处得到处理。

定义

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

一个可以对外部世界产生副作用，或抛出 ε 类型异常的单子。

BaseIO 是此单子的不抛异常版本。IO 则将异常类型设为 IO.Error。

定义

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

创建一个 IO 动作；当且仅当它被执行时，才会调用 fn，并返回其结果。

定义

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

将一个不会抛出异常的 BaseIO 动作作为 IO 动作运行。

此函数通常通过自动单子提升隐式使用，而不是显式调用。

定义

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

在任意其他 EIO 单子中运行一个不会抛出异常的 BaseIO 动作。

此函数通常通过自动单子提升隐式使用，而不是显式调用。

定义

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

将一个可能抛出 ε 类型异常的 EIO ε 动作，转换为一个不抛异常、返回 Except 值的 BaseIO 动作。

定义

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

使用 f 将其抛出的任何异常翻译为 IO.Error，从而把 EIO ε 动作转换为 IO 动作。

定义

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

将一个可能抛出 ε 类型异常的 EIO ε 动作，转换为一个不抛异常、返回 Except 值的 IO 动作。

定义

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

在某个其他 EIO 单子中运行一个 IO 动作，并用 f 转换 IO 异常。

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

IO 单子使用的错误处理设施与其他异常单子相同。具体来说，异常的抛出与捕获使用 MonadExceptOf 类型类的方法。 IO 中抛出的异常具有 IO.Error 类型。该类型的构造器表示多数操作系统中会发生的底层错误，例如文件不存在。最常用的构造器是 userError；它涵盖其余所有情况，并包含一个描述问题的字符串。

归纳类型

IO.Error : Type
IO.Error : Type

可在 IO 单子中抛出的异常。

IO.Error 的许多构造子都对应 POSIX 错误号。在这些情况下，文档字符串会列出与该错误相对应的 POSIX 标准错误宏。该列表不一定穷尽全部情况，并且这些构造子还包含一个字段，用于保存底层错误号。

构造子

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

操作失败，因为文件已存在。

这对应 POSIX 错误 EEXIST、EINPROGRESS 和 EISCONN。

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

发生了 IO.Error 其他构造子未覆盖的某种错误。

这还包括 POSIX 错误 EFAULT。

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

某个必需资源正忙。

这对应 POSIX 错误 EADDRINUSE、EBUSY、EDEADLK 和 ETXTBSY。

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

某个必需资源已不再可用。

这对应 POSIX 错误 ECONNRESET、EIDRM、ENETDOWN、ENETRESET、ENOLINK 和 EPIPE。

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

某项操作不受支持。

这对应 POSIX 错误 EADDRNOTAVAIL、EAFNOSUPPORT、ENODEV、ENOPROTOOPT、 ENOSYS、EOPNOTSUPP、ERANGE、ESPIPE 和 EXDEV。

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

操作因硬件问题而失败，例如 I/O 错误。

这对应 POSIX 错误 EIO。

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

操作所需的某个约束未被满足（例如目录非空）。

这对应 POSIX 错误 ENOTEMPTY。

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

尝试了不恰当的 I/O 控制操作。

这对应 POSIX 错误 ENOTTY。

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

发生了协议错误。

这对应 POSIX 错误 EPROTO、EPROTONOSUPPORT 和 EPROTOTYPE。

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

某项操作超时。

这对应 POSIX 错误 ETIME 和 ETIMEDOUT。

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

操作被中断。

这对应 POSIX 错误 EINTR。

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

没有这样的文件或目录。

这对应 POSIX 错误 ENOENT。

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

I/O 操作的某个实参无效。

这对应 POSIX 错误 ELOOP、ENAMETOOLONG、EDESTADDRREQ、EILSEQ、EINVAL、 EDOM、EBADF、ENOEXEC、ENOSTR、ENOTCONN 和 ENOTSOCK。

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

操作因权限不足而失败。

这对应 POSIX 错误 EACCES、EROFS、ECONNABORTED、EFBIG 和 EPERM。

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

某种资源已耗尽。

这对应 POSIX 错误 EMFILE、ENFILE、ENOSPC、E2BIG、EAGAIN、EMLINK、 EMSGSIZE、ENOBUFS、ENOLCK、ENOMEM 和 ENOSR。

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

某个实参具有错误的类型（例如需要文件时却给了目录）。

这对应 POSIX 错误 EISDIR、EBADMSG 和 ENOTDIR。

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

某个必需资源不存在。

这对应 POSIX 错误 ENXIO、EHOSTUNREACH、ENETUNREACH、ECHILD、 ECONNREFUSED、ENODATA、ENOMSG 和 ESRCH。

IO.Error.unexpectedEof : IO.Error

遇到了意外的文件结束标记。

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

发生了某种其他错误。

定义

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

将 IO.Error 转换为描述性的字符串。

IO.Error.userError 会被转换为其内嵌消息。其他构造子则会以保留结构化信息的方式转换，例如错误码和文件名，这些信息有助于诊断问题。

定义

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

将一个 Except ε 动作转换为 IO 动作。

如果该 Except ε 动作抛出异常，则会使用异常类型的 ToString 实例将其转换为 IO.Error 并抛出；否则返回其中的值。

定义

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

处理 EIO ε 动作可能抛出的任何异常，并将其转换为一个不抛异常的 BaseIO 动作。

定义

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

从字符串构造一个 IO.Error。

IO.Error 是 IO 单子所抛出异常的类型。

抛出和捕获错误

该程序反复要求输入密码，并使用异常控制流程。异常所用的语法适用于所有异常单子，而不只适用于 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 单子🔗

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

21.1.1. `IO`、`EIO` 与 `BaseIO` 单子🔗

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