IO 单子具有非常多的作用，用于编写需要与外部世界交互的程序。
专门的一节对它进行了介绍。
使用 IO 的程序本质上是黑箱：它们通常并不特别适合验证。
许多算法只需少得多的作用便能最方便地表达。 这些作用往往可以模拟；例如，可以通过传递同时包含程序值和状态的元组来模拟可变状态。 这些模拟出来的作用更容易进行形式化推理，因为它们是用普通代码而非新的语言原语定义的。
标准库提供了用于处理常见作用的抽象。 许多常用作用可归入少数几类：
若计算可以访问某些可能被计算的其他部分修改的数据，它就使用了可变状态。
状态有多种实现方式，详见状态单子一节，并由 MonadState 类型类刻画。
大多数编程语言都存在能够读取上下文所提供参数值的计算，但许多将状态和异常作为一等特性的语言并没有内置定义新参数化计算的设施。
通常，调用这类计算时会向它提供一个参数值，有时还可以局部覆盖该值。
参数值具有动态作用域：使用的是调用栈中最近提供的值。
可以在一连串函数调用中原样传递某个值来模拟它们；但这种技巧会使代码更难阅读，还可能不慎把错误的值传给后续调用。
也可以借助可变状态来模拟，但必须谨慎约束状态的修改。
维护一个参数、并可能允许在调用栈某段中覆盖该参数的单子称为读取器单子。
读取器单子由 MonadReader 类型类刻画。
此外，允许局部覆盖参数值的读取器单子由 MonadWithReader 类型类刻画。
可能以异常值提前终止的计算使用异常。
通常用和类型对其建模：一个构造器表示正常终止，另一个构造器表示因错误而提前终止。
异常单子一节介绍了异常单子，它们由 MonadExcept 类型类刻画。
使用 MonadState 和 MonadExcept 这样的类型类，可以让客户端代码对单子具有多态性。
结合自动提升，程序便能在许多不同的单子中复用，也更能适应重构。
必须注意，单子中的作用并不一定只有一种交互方式。 例如，同时具有状态和异常的单子在抛出异常时可能回滚状态变更，也可能不回滚。 如果这会影响函数的正确性，就应使用更具体的签名。
函数 sumNonFives 使用状态单子对列表内容求和，遇到 5 时提前终止。
def sumNonFives {m}
[Monad m] [MonadState Nat m] [MonadExcept String m]
(xs : List Nat) :
m Unit := do
for x in xs do
if x == 5 then
throw "Five was encountered"
else
modify (· + x)
在一种单子中运行它，会返回遇到 5 时的状态：
#eval
sumNonFives (m := ExceptT String (StateM Nat))
[1, 2, 3, 4, 5, 6] |>.run |>.run 0
在另一种单子中，状态会被丢弃：
#eval
sumNonFives (m := StateT Nat (Except String))
[1, 2, 3, 4, 5, 6] |>.run 0
在第二种情况下，异常处理器会把状态回滚到 Lean.Parser.Term.termTry : termtry 开始时的值。
因此，下列函数并不正确：
/-- 计算列表中首个 5 之前前缀的元素之和。 -/
def sumUntilFive {m}
[Monad m] [MonadState Nat m] [MonadExcept String m]
(xs : List Nat) :
m Nat := do
MonadState.set 0
try
sumNonFives xs
catch _ =>
pure ()
get
在一种单子中，答案正确：
#eval
sumUntilFive (m := ExceptT String (StateM Nat))
[1, 2, 3, 4, 5, 6] |>.run |>.run' 0
在另一种单子中，答案不正确：
#eval
sumUntilFive (m := StateT Nat (Except String))
[1, 2, 3, 4, 5, 6] |>.run' 0
一个单子可以支持同一种作用的多个版本。
例如，可以同时有可变的 Nat 和可变的 String，也可以有两个独立的读取器参数。
只要它们类型不同，就应当能方便地访问二者。
在典型用法中，类型类所重载的某些单子操作拥有可供实例合成使用的类型信息，而另一些操作则没有。
例如，传给 set 的参数决定了要使用的状态类型，而 get 不接受这样的参数。
当存在多个状态时，可以利用 set 应用中的类型信息选择正确实例。这表明可变状态的类型应当是输入参数或半输出参数，以便用它选择实例。
另一方面，get 的使用中缺少类型信息，这表明可变状态的类型在 MonadState 中应当是输出参数，从而让类型类合成根据单子本身确定状态类型。
许多作用类型类都提供两个版本，以此解决这种两难。
带半输出参数的版本以后缀 -Of 命名，其操作会按需显式接收类型。
例如 MonadStateOf、MonadReaderOf 和 MonadExceptOf。
带显式类型参数的操作以 -The 结尾，例如 getThe、readThe 和 tryCatchThe。
带输出参数的版本名称不加修饰。
标准库会根据典型用法中推断行为的优劣，从各类型类的 -Of 版本和无修饰版本中混合导出操作。
操作 | 来源类型类 | 说明 |
|---|---|---|
| 输出参数改善类型推断 | |
半输出参数使用 | ||
需要输出参数，以允许不带标注的函数 | ||
| 需要输出参数，以允许不带标注的函数 | |
实参没有提供类型信息，因此需要输出参数 | ||
半输出参数使用所提供的类型引导合成 | ||
输出参数免去了在函数上添加类型标注的需要 | ||
半输出参数使用所提供的类型引导合成 | ||
输出参数使异常可以使用构造器点记法 | ||
半输出参数使用所提供的类型引导合成 | ||
输出参数使异常可以使用构造器点记法 | ||
半输出参数使用所提供的类型引导合成 |
状态单子 M 有两个独立状态：一个 Nat 和一个 String。
abbrev M := StateT Nat (StateM String)
由于 get 是 MonadState.get 的别名，状态类型是输出参数。
这意味着 Lean 会自动选择状态类型；在此例中，它选择最外层单子变换器的状态类型：
#check (get : M _)
因为状态类型是输出参数，所以只能使用最外层的状态。
#check (get : M String)
使用 MonadStateOf 中的 getThe 显式提供状态类型，就可以读取两种状态。
#check ((getThe String, getThe Nat) : M String × M Nat)
两种类型的状态都可以设置，因为状态类型在 MonadStateOf 上是半输出参数。
#check (set 4 : M Unit)
#check (set "Four" : M Unit)
单子变换器是一个函数：给它一个单子，它会返回一个新单子。 通常，新单子具有原单子的全部作用，并附加一些作用。
单子变换器由以下部分组成：
函数 T，从已有单子构造新单子的类型
run 函数，将 T m α 转换为 m 的某种形式；它通常需要额外参数，并返回 m 下更具体的类型
MonadLift 的实例，使原单子的代码可在变换后的单子中使用
如果可能，还包括 MonadControl m (T m) 的实例，使变换后单子中的动作可在原单子中使用
通常，单子变换器还会提供一个或多个类型类的实例，用以描述它所引入的作用。
变换器的 Monad 和 MonadLift 实例使得在变换后的单子中编写代码切实可行，而类型类实例则允许将变换后的单子用于多态函数。
恒等单子变换器既不增加也不移除被变换单子的能力。 它的定义是适当特化后的恒等函数：
def IdT (m : Type u → Type v) : Type u → Type v := m
同样，run 函数不需要额外实参，只返回一个 m α：
def IdT.run (act : IdT m α) : m α := act
该单子实例依赖被变换单子的单子实例，并通过类型注明选择它：
instance [Monad m] : Monad (IdT m) where
pure x := (pure x : m _)
bind x f := (x >>= f : m _)
因为 IdT m 在定义上等于 m，所以 MonadLift m (IdT m) 实例无需修改被提升的动作：
instance : MonadLift m (IdT m) where
monadLift x := x
MonadControl 实例也同样简单。
instance [Monad m] : MonadControl m (IdT m) where
stM α := α
liftWith f := f (fun x => Id.run <| pure x)
restoreM v := v
Lean 标准库为许多不同的单子提供了变换器版本，包括 ReaderT、ExceptT 和 StateT，以及使用其他表示的变体，如 StateCpsT、StateRefT 和 ExceptCpsT。
此外，EStateM 单子等价于组合 ExceptT 与 StateT，但它可以使用更专门的表示来提升性能。
恒等单子 Id 完全没有任何作用。
Id 以及对应的 pure 实现都是恒等函数，而 bind 是反向函数应用。
恒等单子主要有两种用途：
它可以作为 Lean.Parser.Term.do : termdo 块的类型，用局部作用实现纯函数。
它可以放在单子变换器栈的最底层。
状态单子提供对可变值的访问。
底层实现可以使用元组模拟可变性，也可以使用 ST.Ref 之类的机制确保发生修改。
即便是使用元组的实现，由于 Lean 会在值具有唯一引用时采用修改，其运行时实际上也可能使用修改；但这要求编程风格优先使用 modify 和 modifyGet，而非 get 和 set。
状态单子提供一个给定类型的值（即_状态_），该值可以获取或替换。实例可以通过传递状态值、
使用可变引用单元（例如 ST.Ref σ）或其他方式实现这些操作。
在此类中，σ 是 outParam，这意味着它由 m 推断。MonadStateOf σ 提供相同的操作，
但允许 σ 影响实例合成。
状态单子的可变状态在多个 do 块或函数之间可见，这不同于 do 记法中的
局部可变状态。
实例构造子
MonadState.mk.{u, v}
获取单子当前的可变状态值。
MonadState.modifyGet.{u, v} {σ : outParam (Type u)} {m : Type u → Type v} [self : MonadState σ m] {α : Type u} : (σ → α × σ) → m αMonadState.modifyGet.{u, v} {σ : outParam (Type u)} {m : Type u → Type v} [self : MonadState σ m] {α : Type u} : (σ → α × σ) → m α
把一个函数应用于当前状态，该函数同时计算新状态和一个值。新状态替换当前状态，并返回该值。
它等价于 do let (a, s) := f (← get); set s; pure a。不过，使用 modifyGet 可能有更高性能，
因为它不会增加状态值的新引用；额外引用可能妨碍对数据进行原地更新。
用把 f 应用于状态所得的结果替换状态，并返回状态的旧值。
它等价于 get <* modify f，但可能更加高效。
状态单子提供一个给定类型的值（即_状态_），该值可以获取或替换。实例可以通过传递状态值、
使用可变引用单元（例如 ST.Ref σ）或其他方式实现这些操作。
在此类中，σ 是 semiOutParam，这意味着它可以影响实例的选择。MonadState σ 提供相同的
操作，但要求能从 m 推断出 σ。
状态单子的可变状态在多个 do 块或函数之间可见，这不同于 do 记法中的
局部可变状态。
实例构造子
MonadStateOf.mk.{u, v}
获取显式给定类型 σ 的当前状态。当当前单子提供多种状态类型时，此函数从中选择一种。
修改显式给定类型 σ 的当前状态，用把 f 应用于该状态所得的结果替换其值。当当前单子提供
多种状态类型时，此函数从中选择一种。
它等价于 do set (f (← get))。不过，使用 modify 可能有更高性能，因为它不会增加状态值的
新引用；额外引用可能妨碍对数据进行原地更新。
modifyGetThe.{u, v} {α : Type u} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → α × σ) : m αmodifyGetThe.{u, v} {α : Type u} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → α × σ) : m α
把一个函数应用于显式给定类型 σ 的当前状态。该函数同时计算新状态和一个值；新状态替换当前
状态，并返回该值。
它等价于 do let (a, s) := f (← getThe σ); set s; pure a。不过，使用 modifyGetThe 可能有
更高性能，因为它不会增加状态值的新引用；额外引用可能妨碍对数据进行原地更新。
基于元组的状态单子把状态类型为 σ、产生 α 类型值的计算表示为函数：它接受初始状态，并产生一个值与最终状态组成的二元组，例如 σ → α × σ。
Monad 操作会在计算中正确地传递状态。
为单子增加 σ 类型的可变状态。
所得单子中的动作是接受初始状态、并在 m 中返回一个值与状态之二元组的函数。
StateT.run.{u, v} {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ)StateT.run.{u, v} {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ)
在底层单子 m 中执行一个来自增加了状态的单子的动作。给定初始状态，它返回一个值与最终状态
组成的二元组。
获取单子当前的可变状态值。
这会增加状态的引用计数，因而可能妨碍原地更新。
用新值替换可变状态。
StateT.orElse.{u, v} {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) : StateT σ m αStateT.orElse.{u, v} {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) : StateT σ m α
从错误中恢复。错误恢复时会回滚状态。通常通过 <|> 运算符使用。
StateT.failure.{u, v} {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} : StateT σ m αStateT.failure.{u, v} {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} : StateT σ m α
以可恢复的错误失败。错误恢复时会回滚状态。
StateT.run'.{u, v} {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m αStateT.run'.{u, v} {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α
在底层单子 m 中执行一个来自增加了状态的单子的动作。给定初始状态，它返回一个值，并丢弃
最终状态。
StateT.bind.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m βStateT.bind.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β
依次执行两个动作。通常通过 >>= 运算符使用。
StateT.modifyGet.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σ → α × σ) : StateT σ m αStateT.modifyGet.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σ → α × σ) : StateT σ m α
把一个函数应用于当前状态，该函数同时计算新状态和一个值。新状态替换当前状态，并返回该值。
它等价于 do let (a, s) := f (← StateT.get); StateT.set s; pure a。不过，使用
StateT.modifyGet 可能有更高性能，因为它不会增加状态值的新引用；额外引用可能妨碍对数据
进行原地更新。
StateT.lift.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : StateT σ m αStateT.lift.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : StateT σ m α
在带状态的单子中运行底层单子的动作。状态不会被修改。
此函数通常通过 MonadLiftT 实例隐式使用，作为自动提升的一部分。
StateT.map.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : StateT σ m α) : StateT σ m βStateT.map.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : StateT σ m α) : StateT σ m β
修改计算所返回的值。通常通过 <$> 运算符使用。
延续传递风格的状态单子把有状态计算表示为函数：对于任意类型，该函数接受初始状态和一个延续（建模为函数），而延续接受一个值和更新后的状态。
这种类型的一个例子是 (δ : Type u) → σ → (α → σ → δ) → δ，不过 StateCpsT 是可应用于任意单子的变换器。
延续传递风格的状态单子与基于元组的状态单子具有不同的性能特征；对某些应用而言，值得对它们进行基准测试。
状态单子变换器的另一种实现；其内部使用延续传递风格而非二元组。
StateCpsT.runK.{u, v} {α σ : Type u} {m : Type u → Type v} {β : Type u} (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m βStateCpsT.runK.{u, v} {α σ : Type u} {m : Type u → Type v} {β : Type u} (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β
通过提供初始状态和延续，运行以延续传递风格表示的有状态计算。
StateCpsT.run'.{u, v} {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m αStateCpsT.run'.{u, v} {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m α
在底层单子 m 中执行一个来自增加了状态的单子的动作。给定初始状态，它返回一个值，并丢弃
最终状态。
单子 StateRefT σ m 是专门的状态单子变换器；当 m 是可以提升 ST 计算的单子时，便可使用它。
它使用 ST.Ref 而非纯函数来实现 MonadState 的操作。
这确保了运行时确实会使用修改。
ST 和 EST 需要一个幽灵类型参数，它与 runST 的多态函数实参共同用于封装可变性。
与其要求把它作为变换器的参数，不如使用辅助类型类 STWorld，直接从 m 传播该参数。
变换器本身被定义为语法扩展和精译器，而非普通函数。
这是因为 STWorld 没有方法：它的存在只是为了把信息从内层单子传播到变换后的单子。
尽管如此，它的实例仍是项；保留这些实例可能导致类型不必要地增大。
StateRefT
StateRefT σ m 的语法接受两个实参：
term ::= ...
|
它的精译器会合成 STWorld ω m 的实例，以确保 m 支持可变引用。
发现 ω 的值后，它会生成项 StateRefT' ω σ m，并丢弃所合成的实例。
获取单子当前的可变状态值。
这会增加状态的引用计数，因而可能妨碍原地更新。
StateRefT'.set {ω σ : Type} {m : Type → Type} [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnitStateRefT'.set {ω σ : Type} {m : Type → Type} [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit
用新值替换可变状态。
StateRefT'.modifyGet {ω σ : Type} {m : Type → Type} {α : Type} [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m αStateRefT'.modifyGet {ω σ : Type} {m : Type → Type} {α : Type} [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α
把一个函数应用于当前状态，该函数同时计算新状态和一个值。新状态替换当前状态，并返回该值。
它等价于先执行 get 再执行 set。不过，使用 modifyGet 可能有更高性能，因为它不会增加
状态值的新引用；额外引用可能妨碍对数据进行原地更新。
StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ)StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ)
在底层单子 m 中执行一个来自增加了状态的单子的动作。给定初始状态，它返回一个值与最终状态
组成的二元组。
单子 m 必须支持 ST 效应，才能创建和修改引用单元。
StateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m αStateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m α
在底层单子 m 中执行一个来自增加了状态的单子的动作。给定初始状态，它返回一个值，并丢弃
最终状态。
单子 m 必须支持 ST 效应，才能创建和修改引用单元。
读取器单子能够在计算中隐式传递一个值。该值可以读取，但不能写入。
MonadWithReader ρ 实例还允许为子计算局部覆盖此值。
在此类中，ρ 是 outParam，这意味着它由 m 推断。
MonadReaderOf ρ 提供相同的操作，但允许 ρ 影响实例合成。
实例构造子
MonadReader.mk.{u, v}
方法
read : m ρ
获取局部值。
当有多个值可用时，使用 readThe 显式指定类型。
读取器单子能够在计算中隐式传递一个值。该值可以读取，但不能写入。
MonadWithReader ρ 实例还允许为子计算局部覆盖此值。
在此类中，ρ 是 semiOutParam，这意味着它可以影响实例的选择。
MonadReader ρ 提供相同的操作，但要求能从 m 推断出 ρ。
实例构造子
MonadReaderOf.mk.{u, v}
方法
read : m ρ
获取局部值。
还允许局部覆盖值的读取器单子。
在此类中，ρ 是 outParam，这意味着它由 m 推断。
MonadWithReaderOf ρ 提供相同的操作，但允许 ρ 影响实例合成。
实例构造子
MonadWithReader.mk.{u, v}
方法
withReader : {α : Type u} → (ρ → ρ) → m α → m α
在运行动作时局部修改读取器单子的值。
在内部动作 x 执行期间，读取该值会返回把 f 应用于原值所得的结果。从 x 返回控制后，
读取器单子的值会恢复。
还允许局部覆盖值的读取器单子。
在此类中，ρ 是 semiOutParam，这意味着它可以影响实例的选择。
MonadWithReader ρ 提供相同的操作，但要求能从 m 推断出 ρ。
实例构造子
MonadWithReaderOf.mk.{u, v}
方法
withReader : {α : Type u} → (ρ → ρ) → m α → m α
在运行动作时局部修改读取器单子的值。
在内部动作 x 执行期间，读取该值会返回把 f 应用于原值所得的结果。从 x 返回控制后，
读取器单子的值会恢复。
withTheReader.{u, v} (ρ : Type u) {m : Type u → Type v} [MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) : m αwithTheReader.{u, v} (ρ : Type u) {m : Type u → Type v} [MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) : m α
在运行动作时局部修改读取器单子的值，并显式指定该局部值的类型。当单子支持读取多种类型的值时， 此函数很有用。
在内部动作 x 执行期间，读取该值会返回把 f 应用于原值所得的结果。从 x 返回控制后，
读取器单子的值会恢复。
若希望由 m 推断局部值的类型，请使用 withReader。
ReaderT.run.{u, v} {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m αReaderT.run.{u, v} {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α
在底层单子 m 中执行一个来自带只读值单子的动作。
ReaderT.adapt.{u, v} {ρ : Type u} {m : Type u → Type v} {ρ' α : Type u} (f : ρ' → ρ) : ReaderT ρ m α → ReaderT ρ' m αReaderT.adapt.{u, v} {ρ : Type u} {m : Type u → Type v} {ρ' α : Type u} (f : ρ' → ρ) : ReaderT ρ m α → ReaderT ρ' m α
使用 f 修改读取器单子的局部值。所得计算把 f 应用于传入的局部值，再将结果传给内部计算。
ReaderT.pure.{u, v} {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : ReaderT ρ m αReaderT.pure.{u, v} {ρ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : ReaderT ρ m α
返回给定值 a，忽略读取器单子的局部值。通常通过 Pure.pure 使用。
ReaderT.bind.{u, v} {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m βReaderT.bind.{u, v} {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m β
依次执行两个读取器单子计算。二者都会获得局部值，而第二个计算还会获得第一个计算的值。
通常通过 >>= 运算符使用。
ReaderT.orElse.{u_1, u_2} {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Alternative m] (x₁ : ReaderT ρ m α) (x₂ : Unit → ReaderT ρ m α) : ReaderT ρ m αReaderT.orElse.{u_1, u_2} {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Alternative m] (x₁ : ReaderT ρ m α) (x₂ : Unit → ReaderT ρ m α) : ReaderT ρ m α
从错误中恢复。两个分支都会获得同一个局部值。通常通过 <|> 运算符使用。
ReaderT.failure.{u_1, u_2} {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Alternative m] : ReaderT ρ m αReaderT.failure.{u_1, u_2} {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Alternative m] : ReaderT ρ m α
以可恢复的错误失败。
通常，Option 被视为数据，类似于可空类型。
它也可以被视为单子，从而成为一种执行计算的方式。
Option 单子及其变换器 OptionT 可以理解为描述可能提前终止并丢弃结果的计算。
调用方可以使用 OrElse.orElse 检查是否提前终止，并按需调用后备计算；也可以把它当作 MonadExcept Unit 处理。
为单子增加失败能力。与普通异常不同，它无法说明失败发生的原因。
以给定值成功。
OptionT.bind.{u, v} {m : Type u → Type v} [Monad m] {α β : Type u} (x : OptionT m α) (f : α → OptionT m β) : OptionT m βOptionT.bind.{u, v} {m : Type u → Type v} [Monad m] {α β : Type u} (x : OptionT m α) (f : α → OptionT m β) : OptionT m β
依次执行两个可能失败的动作。仅当第一个动作成功时才运行第二个动作。
可恢复的失败。
异常单子描述会提前终止（失败）的计算。
失败的计算向调用方提供一个异常值，用于说明失败的原因。
换言之，计算要么返回值，要么返回异常。
归纳类型 Except 刻画了这一模式，而它本身也是单子。
Except ε α 是这样一种类型：它表示类型为 ε 的错误，或者带有类型为 α 的值的成功结果。
Except ε : Type u → Type v 是一个表示可能抛出异常的计算的 Monad：pure 操作是 Except.ok，而 bind 操作返回遇到的第一个 Except.error。
构造子
Except.error.{u, v} {ε : Type u} {α : Type v} : ε → Except ε α
类型为 ε 的失败值。
Except.ok.{u, v} {ε : Type u} {α : Type v} : α → Except ε α
类型为 α 的成功值。
Except.bind.{u, u_1, u_2} {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : α → Except ε β) : Except ε βExcept.bind.{u, u_1, u_2} {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : α → Except ε β) : Except ε β
依次执行两个可能抛出异常的操作，并允许第二个操作依赖第一个操作返回的值。
如果第一个操作抛出异常，那么该异常就是计算结果。如果第一个操作成功、但第二个操作抛出异常，那么后一个异常就是结果。如果两者都成功，那么结果就是第二个计算的结果。
这是 Except ε 的 >>= 运算符的实现。
Except.map.{u, u_1, u_2} {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) : Except ε α → Except ε βExcept.map.{u, u_1, u_2} {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) : Except ε α → Except ε β
Except.mapError.{u, u_1, u_2} {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') : Except ε α → Except ε' αExcept.mapError.{u, u_1, u_2} {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : ε → ε') : Except ε α → Except ε' α
Except.tryCatch.{u, u_1} {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : ε → Except ε α) : Except ε αExcept.tryCatch.{u, u_1} {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α
Except.orElseLazy.{u, u_1} {ε : Type u} {α : Type u_1} (x : Except ε α) (y : Unit → Except ε α) : Except ε αExcept.orElseLazy.{u, u_1} {ε : Type u} {α : Type u_1} (x : Except ε α) (y : Unit → Except ε α) : Except ε α
从 Except ε 单子中抛出的异常恢复。通常通过 <|> 运算符使用。
Except.tryCatch 是一个相关运算符，它允许恢复过程依赖于抛出的是_哪个_异常。
异常单子提供抛出错误和处理错误的能力。
在这个类中，ε 是 outParam，这意味着它从 m 推断得出。MonadExceptOf ε 提供相同的操作，但允许 ε 影响实例合成。
当处理器没有异常类型标注时，MonadExcept.tryCatch 用于对 do 块中的 try ... catch ... 步骤进行脱糖。
实例构造子
MonadExcept.mk.{u, v, w}
方法
throw : {α : Type v} → ε → m α
向最近的外围处理器抛出类型为 ε 的异常。
tryCatch : {α : Type v} → m α → (ε → m α) → m α
捕获 body 中抛出的错误，并将它们传给 handler。不捕获 handler 中的错误。
MonadExcept.ofExcept.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {ε : Type u_3} {α : Type u_1} [Monad m] [MonadExcept ε m] : Except ε α → m αMonadExcept.ofExcept.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {ε : Type u_3} {α : Type u_1} [Monad m] [MonadExcept ε m] : Except ε α → m α
将 Except ε 动作重新解释为异常单子 m 中的动作：前者成功时后者成功，前者抛出异常时后者也抛出异常。
MonadExcept.orElse.{u, v, w} {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) : m αMonadExcept.orElse.{u, v, w} {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : Unit → m α) : m α
忽略抛出了哪个异常的无条件错误恢复。通常通过 <|> 运算符使用。
如果两个计算都抛出异常，那么结果是第二个异常。
MonadExcept.orelse'.{u, v, w} {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx : Bool := true) : m αMonadExcept.orelse'.{u, v, w} {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx : Bool := true) : m α
另一种无条件错误恢复运算符，允许调用者指定当两个操作都抛出异常时应抛出哪个异常。
默认抛出第一个异常，因为 <|> 运算符会抛出第二个。
MonadExceptOf.{u, v, w} (ε : semiOutParam (Type u)) (m : Type v → Type w) : Type (max (max u (v + 1)) w)MonadExceptOf.{u, v, w} (ε : semiOutParam (Type u)) (m : Type v → Type w) : Type (max (max u (v + 1)) w)
异常单子提供抛出错误和处理错误的能力。
在这个类中，ε 是 semiOutParam，这意味着它可以影响实例的选择。MonadExcept ε 提供相同的操作，但要求能够从 m 推断出 ε。
当处理器带有类型标注时，显式接受异常类型的 tryCatchThe 用于对 do 块中的 try ... catch ... 步骤进行脱糖。
实例构造子
MonadExceptOf.mk.{u, v, w}
方法
throw : {α : Type v} → ε → m α
向最近的外围 catch 抛出类型为 ε 的异常。
tryCatch : {α : Type v} → m α → (ε → m α) → m α
捕获 body 中抛出的错误，并将它们传给 handler。不捕获 handler 中的错误。
throwThe.{u, v, w} (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m αthrowThe.{u, v, w} (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α
抛出异常，并显式指定异常类型。当一个单子支持抛出多种类型的异常时，这很有用。
如需让程序从 m 推断异常类型的版本，请使用 throw。
tryCatchThe.{u, v, w} (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m αtryCatchThe.{u, v, w} (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α
捕获错误，并使用 handle 恢复。异常类型是显式指定的。当一个单子支持抛出或处理多种类型的异常时，这很有用。
如需让程序从 m 推断异常类型的版本，请使用 tryCatch。
提供一种能力，确保无论发生异常还是其他失败，某个动作都会执行的单子。
MonadFinally.tryFinally' 用于对 try ... finally ... 语法进行脱糖。
实例构造子
MonadFinally.mk.{u, v}
方法
tryFinally' : {α β : Type u} → m α → (Option α → m β) → m (α × β)
运行一个动作，并确保之后总会运行另一个动作。
更具体地说，tryFinally' x f 运行 x，然后运行最终处理计算 f。如果 x 成功并得到某个值 a : α，则返回 f (some a)。如果 x 按 m 对失败的定义而失败，则返回 f none。
可以认为 tryFinally' 的作用与命令式编程语言中的 finally 块相同。
向单子 m 添加类型为 ε 的异常。
ExceptT.lift.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : ExceptT ε m αExceptT.lift.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) : ExceptT ε m α
在带异常的变换后单子中运行底层单子的计算。
ExceptT.run.{u, v} {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α)ExceptT.run.{u, v} {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α)
把可能抛出异常的单子动作作为可能返回异常值的动作使用。
这是 ExceptT.mk 的逆操作。
ExceptT.pure.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : ExceptT ε m αExceptT.pure.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) : ExceptT ε m α
返回值 a，既不抛出异常，也不产生任何其他效果。
ExceptT.bind.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m βExceptT.bind.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β
依次执行两个可能抛出异常的动作。通常通过 do 记法或 >>= 运算符使用。
ExceptT.bindCont.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)ExceptT.bindCont.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
处理一个除抛出异常外不可能有_其他_效果的动作所抛出的异常。
ExceptT.tryCatch.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m αExceptT.tryCatch.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α
处理 ExceptT ε 变换器中产生的异常。
ExceptT.mk.{u, v} {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m αExceptT.mk.{u, v} {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α
把可能返回异常值的单子动作作为变换后单子中可能抛出相应异常的动作使用。
这是 ExceptT.run 的逆操作。
ExceptT.map.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m βExceptT.map.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β
使用 f 变换成功计算的值。通常通过 <$> 运算符使用。
ExceptT.adapt.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m αExceptT.adapt.{u, v} {ε : Type u} {m : Type u → Type v} [Monad m] {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α
使用函数 f 变换异常。
这是 Except.mapError 的 ExceptT 版本。
延续传递风格的异常单子把可能失败的计算表示为函数：它接受成功延续和失败延续，二者返回相同类型，而函数也返回该类型。
它们必须适用于任意返回类型。
这种类型的一个例子是 (β : Type u) → (α → β) → (ε → β) → β。
ExceptCpsT 是可应用于任意单子的变换器，因此 ExceptCpsT ε m α 实际定义为 (β : Type u) → (α → m β) → (ε → m β) → m β。
延续传递风格的异常单子与基于 Except 的异常单子具有不同的性能特征；对某些应用而言，值得对它们进行基准测试。
ExceptCpsT.runCatch.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : ExceptCpsT α m α) : m αExceptCpsT.runCatch.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : ExceptCpsT α m α) : m α
返回计算的值，不再区分它是异常还是成功结果。
这对应于提前返回。
ExceptCpsT.runK.{u, u_1} {m : Type u → Type u_1} {β ε α : Type u} (x : ExceptCpsT ε m α) (ok : α → m β) (error : ε → m β) : m βExceptCpsT.runK.{u, u_1} {m : Type u → Type u_1} {β ε α : Type u} (x : ExceptCpsT ε m α) (ok : α → m β) (error : ε → m β) : m β
通过提供显式的成功延续和失败延续来使用可能抛出异常的单子动作。
ExceptCpsT.run.{u, u_1} {m : Type u → Type u_1} {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α)ExceptCpsT.run.{u, u_1} {m : Type u → Type u_1} {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α)
把可能抛出异常的单子动作作为可能返回异常值的动作使用。
ExceptCpsT.lift.{u_1, u_2} {m : Type u_1 → Type u_2} {α ε : Type u_1} [Monad m] (x : m α) : ExceptCpsT ε m αExceptCpsT.lift.{u_1, u_2} {m : Type u_1 → Type u_2} {α ε : Type u_1} [Monad m] (x : m α) : ExceptCpsT ε m α
把底层单子中的动作提升到变换后的异常单子中运行。
EStateM 单子同时具有异常和可变状态。
EStateM ε σ α 在逻辑上等价于 ExceptT ε (StateM σ) α。
ExceptT ε (StateM σ) 求值得到类型 σ → Except ε α × σ，而类型 EStateM ε σ α 求值得到 σ → EStateM.Result ε σ α。
EStateM.Result 是一个与 Except 非常相似的归纳类型，不过它的两个构造器都多了一个状态字段。
在编译后的代码中，这种表示为每次单子绑定减少了一层间接访问。
状态与异常组合单子返回的值，其中异常不会自动回滚状态。
Result ε σ α 等价于 Except ε α × σ，但使用单个组合归纳类型可以得到效率更高的数据表示。
构造子
EStateM.Result.ok.{u} {ε σ α : Type u} : α → σ → EStateM.Result ε σ α
类型为 α 的成功值以及新状态 σ。
EStateM.Result.error.{u} {ε σ α : Type u} : ε → σ → EStateM.Result ε σ α
类型为 ε 的异常以及新状态 σ。
使用函数变换异常，而不改变成功结果。
将状态单子动作转换为带异常的状态单子动作。
所得动作不会抛出异常。
以不同顺序组合 StateT 和 ExceptT，会使异常与状态产生不同的交互。
一种顺序会在捕获异常时回滚状态变更；另一种顺序则会保留变更。
后一种选择符合大多数命令式编程语言的语义，但前一种选择对基于搜索的问题非常有用。
通常只应回滚部分而非全部状态；可以把 ExceptT“夹”在两个独立的 StateT 之间来实现这一点。
为避免使用 StateT σ (EStateM ε σ') α 再增加一层间接访问，EStateM 提供了 EStateM.Backtrackable 类型类。
该类指定状态中可以保存和恢复的部分。
EStateM 随后会在错误处理前后安排保存和恢复。
EStateM 中的异常处理器会保存由 δ 确定的部分状态，并在捕获异常时将其恢复。默认情况下，δ 是 Unit，不会保存任何信息。
实例构造子
EStateM.Backtrackable.mk.{u}
方法
save : σ → δ
提取状态中应在处理异常时回滚的信息。
restore : σ → δ → σ
使用应回滚的已保存信息来更新当前状态。处理异常时，这个更新后的状态将成为当前状态。
Backtrackable 有一个普遍适用的实例，它既不保存也不恢复任何内容。
因为实例合成会优先选择最新的实例，所以只有在未定义其他实例时才会使用这个通用实例。
一个不从状态中保存任何信息的后备 Backtrackable 实例。这样，每种类型都可以用作 EStateM 的状态，且不发生回滚。
因为这是最先声明的 Backtrackable _ σ 实例，所以只有在没有注册其他 Backtrackable _ σ 实例时才会选中它。
通常不会直接调用这些函数，而是通过相应的类型类访问它们。
返回一个值，而不修改状态或抛出异常。
EStateM.orElse.{u} {ε σ α δ : Type u} [EStateM.Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂ : Unit → EStateM ε σ α) : EStateM ε σ αEStateM.orElse.{u} {ε σ α δ : Type u} [EStateM.Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂ : Unit → EStateM ε σ α) : EStateM ε σ α
不依赖具体异常值的失败处理。
Backtrackable δ σ 实例用于在运行 x₁ 之前保存部分状态的快照。如果捕获到异常，则使用保存的快照更新状态，从而回滚部分状态。如果没有提供 Backtrackable 实例，则使用 δ 为 Unit 的后备实例，不回滚任何信息。
EStateM.orElse'.{u} {ε σ α δ : Type u} [EStateM.Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx : Bool := true) : EStateM ε σ αEStateM.orElse'.{u} {ε σ α δ : Type u} [EStateM.Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx : Bool := true) : EStateM ε σ α
另一种 orElse 运算符，允许调用者在两个操作都失败时选择应使用哪个异常。默认使用第一个异常，因为标准的 orElse 使用第二个。
EStateM.seqRight.{u} {ε σ α β : Type u} (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) : EStateM ε σ βEStateM.seqRight.{u} {ε σ α β : Type u} (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) : EStateM ε σ β
依次执行两个 EStateM ε σ 动作，先运行 x，再运行 y。忽略第一个动作的返回值。
EStateM.tryCatch.{u} {ε σ δ : Type u} [EStateM.Backtrackable δ σ] {α : Type u} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α) : EStateM ε σ αEStateM.tryCatch.{u} {ε σ δ : Type u} [EStateM.Backtrackable δ σ] {α : Type u} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α) : EStateM ε σ α
处理状态与错误组合单子中抛出的异常。
Backtrackable δ σ 实例用于在运行 x 之前保存部分状态的快照。如果捕获到异常，则使用保存的快照更新状态，从而回滚部分状态。如果没有提供 Backtrackable 实例，则使用 δ 为 Unit 的后备实例，不回滚任何信息。
向最近的外围处理器抛出类型为 ε 的异常。
取得单子可变状态的当前值。
用新值替换单子的可变状态的当前值。
对当前状态应用一个函数，该函数既计算新状态也计算一个值。新状态替换当前状态，并返回该值。
它等价于 do let (a, s) := f (← get); set s; pure a。但是，使用 modifyGet 可能具有更高的性能，因为它不会增加对状态值的新引用。额外的引用会妨碍数据的原地更新。