18.5. 单子的种类🔗

IO monad 有很多很多的效果，用于编写需要与世界交互的程序。它在它自己的部分中进行了描述。使用 IO 的程序本质上是黑匣子：它们通常不太适合验证。

许多算法最容易用更少的效果来表达。这些效果通常可以被模拟；例如，可以通过传递包含程序值和状态的元组来模拟可变状态。这些模拟效果更容易正式推理，因为它们是使用普通代码而不是新语言原语定义的。

标准库提供了处理常用效果的抽象。许多常用效果分为以下几类：

状态单子具有可变状态: 可以访问可能被计算的其他部分修改的某些数据的计算使用可变状态。状态可以通过多种方式实现，在状态 monads 部分中进行了描述，并在 MonadState 类型类中捕获。
Reader monads 是参数化计算: 大多数编程语言中都存在可以读取上下文提供的某些参数值的计算，但是许多将状态和异常作为第一类功能的语言没有用于定义新参数化计算的内置设施。通常，这些计算在调用时会提供一个参数值，有时它们可以在本地覆盖它。参数值具有动态范围：调用堆栈中最近提供的值是使用的值。可以通过一系列函数调用传递一个不变的值来模拟它们；但是，这种技术可能会使代码更难阅读，并带来可能将值错误地传递给进一步调用的风险。它们还可以使用可变状态进行模拟，并围绕状态的修改进行仔细的训练。维护参数的 Monad，可能允许它在调用堆栈的一部分中被覆盖，称为 reader monads。读取器单子在 MonadReader 类型类中捕获。此外，允许本地覆盖参数值的读取器单子在 MonadWithReader 类型类中捕获。
Exception monads 有异常: 可能因异常值而提前终止的计算使用 exceptions。它们通常使用 sum 类型进行建模，该 sum 类型具有用于普通终止的构造函数和用于提前终止错误的构造函数。异常单子在异常单子部分中进行了描述，并在 MonadExcept 类型类中捕获。

18.5.1. Monad Type 类🔗

使用 MonadState 和 MonadExcept 等类型类允许客户端代码相对于 monad 是多态的。与自动提升一起，这使得程序可以在许多不同的 monad 中重用，并使它们更适合重构。

重要的是要意识到单子中的效果可能不仅仅以一种方式相互作用。例如，具有状态和异常的 monad 在抛出异常时可能会也可能不会回滚状态更改。如果这对于函数的正确性很重要，那么它应该使用更具体的签名。

Effect Ordering

函数 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)

在一个 monad 中运行它会返回遇到 5 时的状态：

(Except.error "Five was encountered", 10)#eval
  sumNonFives (m := ExceptT String (StateM Nat))
    [1, 2, 3, 4, 5, 6] |>.run |>.run 0

(Except.error "Five was encountered", 10)

在另一个例子中，状态被丢弃：

Except.error "Five was encountered"#eval
  sumNonFives (m := StateT Nat (Except String))
    [1, 2, 3, 4, 5, 6] |>.run 0

Except.error "Five was encountered"

在第二种情况下，异常处理程序会将状态回滚到 Lean.Parser.Term.termTry : termtry 开头处的值。因此以下函数是不正确的：

/-- Computes the sum of the non-5 prefix of a list. -/
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

在一个 monad 中，答案是正确的：

Except.ok 10#eval
  sumUntilFive (m := ExceptT String (StateM Nat))
    [1, 2, 3, 4, 5, 6] |>.run |>.run' 0

Except.ok 10

另一方面，它不是：

Except.ok 0#eval
  sumUntilFive (m := StateT Nat (Except String))
    [1, 2, 3, 4, 5, 6] |>.run' 0

Except.ok 0

Live ↪

单个 monad 可以支持相同效果的多个版本。例如，可能存在可变的 Nat 和可变的 String 或两个单独的读取器参数。只要它们有不同的类型，就应该可以方便地访问两者。在典型使用中，类型类中重载的一些一元操作具有可用于实例综合的类型信息，而其他操作则没有。例如，传递给 set 的参数确定要使用的状态类型，而 get 不采用此类参数。当有多个状态可用时，set 应用程序中存在的类型信息可用于选择正确的实例，这表明可变状态的类型应该是输入参数或半输出参数，以便可用于选择实例。另一方面，get 的使用中缺乏类型信息，这表明可变状态的类型应该是 MonadState 中的输出参数，因此类型类综合从 monad 本身确定状态的类型。

这种二分法可以通过许多效果类型类的两个版本来解决。带有半输出参数的版本具有后缀-Of，其操作根据需要显式采用类型。示例包括 MonadStateOf、MonadReaderOf 和 MonadExceptOf。具有显式类型参数的操作的名称以 -The 结尾，例如 getThe、readThe 和 tryCatchThe。带有输出参数的版本名称未修饰。标准库根据典型用例中具有良好推理行为的内容，导出 -Of 和每个类型类的未修饰版本的操作组合。

操作	来自班级	注释
`get`	`MonadState`	输出参数改进了类型推断
`set`	`MonadStateOf`	半输出参数使用来自 `set` 参数的类型信息
`modify`	`MonadState`	需要输出参数来允许没有注释的函数
`modifyGet`	`MonadState`	需要输出参数来允许没有注释的函数
`read`	`MonadReader`	由于缺少参数的类型信息，因此需要输出参数
`readThe`	`MonadReaderOf`	半输出参数使用提供的类型来指导合成
`withReader`	`MonadWithReader`	输出参数避免了函数上类型注释的需要
`withTheReader`	`MonadWithReaderOf`	半输出参数使用提供的类型来指导合成
`throw`	`MonadExcept`	输出参数允许对异常使用构造函数点表示法
`throwThe`	`MonadExceptOf`	半输出参数使用提供的类型来指导合成
`tryCatch`	`MonadExcept`	输出参数允许对异常使用构造函数点表示法
`tryCatchThe`	`MonadExceptOf`	半输出参数使用提供的类型来指导合成

State Types

状态单子 M 有两个单独的状态：Nat 和 String。

abbrev M := StateT Nat (StateM String)

由于 get 是 MonadState.get 的别名，因此状态类型是输出参数。这意味着 Lean 自动选择一种状态类型，在本例中是来自最外层 monad 转换器的状态类型：

get : M Nat#check (get : M _)

get : M Nat

只能使用最外层，因为状态的类型是输出参数。

#check (failed to synthesize instance of type class
  MonadState String M

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.get : M String)

failed to synthesize instance of type class
  MonadState String M

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

使用 MonadStateOf 中的 getThe 显式提供状态类型允许读取两种状态。

(getThe String, getThe Nat) : M String × M Nat#check ((getThe String, getThe Nat) : M String × M Nat)

(getThe String, getThe Nat) : M String × M Nat

设置状态适用于任一类型，因为状态类型是 MonadStateOf 上的半输出参数。

set 4 : M PUnit#check (set 4 : M Unit)

set 4 : M PUnit

set "Four" : M PUnit#check (set "Four" : M Unit)

set "Four" : M PUnit

Live ↪

18.5.2. 莫纳德变形金刚🔗

monad Transformer 是一个函数，当提供一个 monad 时，它会返回一个新的 monad。通常，这个新的 monad 具有原始 monad 的所有效果以及一些附加效果。

一个 Monad 转换器由以下部分组成：

从现有 monad 构造新 monad 类型的函数 T
run 函数，将 T m α 改编为 m 的某些变体，通常需要附加参数并在 m 下返回更具体的类型
[Monad m] → Monad (T m) 的实例，允许将转换后的 monad 用作 monad
MonadLift 的实例，允许在转换后的 monad 中使用原始 monad 的代码
如果可能，MonadControl m (T m) 的实例允许在原始 monad 中使用转换后的 monad 中的操作

通常，monad 转换器还提供一个或多个类型类的实例来描述它引入的效果。转换器的 Monad 和 MonadLift 实例使得在转换后的 monad 中编写代码变得实用，而类型类实例允许将转换后的 monad 与多态函数一起使用。

The Identity Monad Transformer

身份 monad 转换器既不会添加也不会删除转换后的 monad 的功能。它的定义是恒等函数，经过适当专门化：

def IdT (m : Type u → Type v) : Type u → Type v := m

同样，run 函数不需要额外的参数，只返回 m α：

def IdT.run (act : IdT m α) : m α := act

monad 实例依赖于转换后的 monad 的 monad 实例，通过 type ascriptions 选择它：

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

Live ↪

Lean 标准库提供许多不同 monad 的转换器版本，包括 ReaderT、ExceptT 和 StateT，以及使用其他表示形式的变体，例如 StateCpsT、StateRefT 和 ExceptCpsT。此外，EStateM monad 相当于 ExceptT 和 StateT 的组合，但它可以使用更专门的表示来提高性能。

18.5.3. 身份🔗

身份单子 Id 没有任何效果。 Id和pure的相应实现都是恒等函数，bind是逆函数应用。身份单子有两个主要用例：

它可以是实现具有局部效果的纯函数的 Lean.Parser.Term.do : termdo 块的类型。
它可以放置在一堆 monad 变压器的底部。

def

Id.{u} (type : Type u) : Type u
Id.{u} (type : Type u) : Type u

The identity function on types, used primarily for its Monad instance.

The identity monad is useful together with monad transformers to construct monads for particular purposes. Additionally, it can be used with do-notation in order to use control structures such as local mutability, for-loops, and early returns in code that does not otherwise use monads.

Examples:

def containsFive (xs : List Nat) : Bool := Id.run do
  for x in xs do
    if x == 5 then return true
  return false

#eval containsFive [1, 3, 5, 7]

true

def

Id.run.{u_1} {α : Type u_1} (x : Id α) : α
Id.run.{u_1} {α : Type u_1} (x : Id α) : α

Runs a computation in the identity monad.

This function is the identity function. Because its parameter has type Id α, it causes do-notation in its arguments to use the Monad Id instance.

Local Effects with the Identity Monad

此代码块通过使用身份单子中的模拟本地可变性来实现倒计时过程。

[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]#eval Id.run do
  let mut xs := []
  for x in [0:10] do
    xs := x :: xs
  pure xs

[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]

Live ↪

18.5.4. 状态🔗

状态单子提供对可变值的访问。底层实现可以使用元组来模拟可变性，或者可以使用 ST.Ref 之类的东西来确保突变。即使那些使用元组的实现实际上也可能在运行时使用突变，因为当存在对值的唯一引用时 Lean 使用突变，但这需要一种更喜欢 modify 和 modifyGet 而不是 get 和 set 的编程风格。

18.5.4.1. 一般状态 API🔗

type class

MonadState.{u, v} (σ : outParam (Type u)) (m : Type u → Type v) :
  Type (max (u + 1) v)
MonadState.{u, v} (σ : outParam (Type u))
  (m : Type u → Type v) :
  Type (max (u + 1) v)

State monads provide a value of a given type (the state) that can be retrieved or replaced. Instances may implement these operations by passing state values around, by using a mutable reference cell (e.g. ST.Ref σ), or in other ways.

In this class, σ is an outParam, which means that it is inferred from m. MonadStateOf σ provides the same operations, but allows σ to influence instance synthesis.

The mutable state of a state monad is visible between multiple do-blocks or functions, unlike local mutable state in do-notation.

Instance Constructor

MonadState.mk.{u, v}

Methods

get : m σ

Retrieves the current value of the monad's mutable state.

set : σ → m PUnit

Replaces the current value of the mutable state with a new one.

modifyGet : {α : Type u} → (σ → α × σ) → m α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to do let (a, s) := f (← get); set s; pure a. However, using modifyGet may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

def

MonadState.get.{u, v} {σ : outParam (Type u)} {m : Type u → Type v}
  [self : MonadState σ m] : m σ
MonadState.get.{u, v}
  {σ : outParam (Type u)}
  {m : Type u → Type v}
  [self : MonadState σ m] : m σ

Retrieves the current value of the monad's mutable state.

def

modify.{u, v} {σ : Type u} {m : Type u → Type v} [MonadState σ m]
  (f : σ → σ) : m PUnit
modify.{u, v} {σ : Type u}
  {m : Type u → Type v} [MonadState σ m]
  (f : σ → σ) : m PUnit

Mutates the current state, replacing its value with the result of applying f to it.

Use modifyThe to explicitly select a state type to modify.

It is equivalent to do set (f (← get)). However, using modify may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

def

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 α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

def

getModify.{u, v} {σ : Type u} {m : Type u → Type v} [MonadState σ m]
  (f : σ → σ) : m σ
getModify.{u, v} {σ : Type u}
  {m : Type u → Type v} [MonadState σ m]
  (f : σ → σ) : m σ

Replaces the state with the result of applying f to it. Returns the old value of the state.

It is equivalent to get <* modify f but may be more efficient.

type class

MonadStateOf.{u, v} (σ : semiOutParam (Type u)) (m : Type u → Type v) :
  Type (max (u + 1) v)
MonadStateOf.{u, v}
  (σ : semiOutParam (Type u))
  (m : Type u → Type v) :
  Type (max (u + 1) v)

In this class, σ is a semiOutParam, which means that it can influence the choice of instance. MonadState σ provides the same operations, but requires that σ be inferable from m.

The mutable state of a state monad is visible between multiple do-blocks or functions, unlike local mutable state in do-notation.

Instance Constructor

MonadStateOf.mk.{u, v}

Methods

get : m σ

Retrieves the current value of the monad's mutable state.

set : σ → m PUnit

Replaces the current value of the mutable state with a new one.

modifyGet : {α : Type u} → (σ → α × σ) → m α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

def

getThe.{u, v} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] :
  m σ
getThe.{u, v} (σ : Type u)
  {m : Type u → Type v}
  [MonadStateOf σ m] : m σ

Gets the current state that has the explicitly-provided type σ. When the current monad has multiple state types available, this function selects one of them.

def

modifyThe.{u, v} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m]
  (f : σ → σ) : m PUnit
modifyThe.{u, v} (σ : Type u)
  {m : Type u → Type v} [MonadStateOf σ m]
  (f : σ → σ) : m PUnit

Mutates the current state that has the explicitly-provided type σ, replacing its value with the result of applying f to it. When the current monad has multiple state types available, this function selects one of them.

def

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 α

Applies a function to the current state that has the explicitly-provided type σ. The function both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to do let (a, s) := f (← getThe σ); set s; pure a. However, using modifyGetThe may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

18.5.4.2. 基于元组的状态 Monad🔗

基于元组的状态单子表示具有 σ 类型的状态的计算，生成 α 类型的值，作为采用起始状态并生成与最终状态配对的值的函数，例如σ → α × σ。 Monad 操作通过计算正确地对状态进行线程化。

def

StateM.{u} (σ α : Type u) : Type u
StateM.{u} (σ α : Type u) : Type u

A tuple-based state monad.

Actions in StateM σ are functions that take an initial state and return a value paired with a final state.

def

StateT.{u, v} (σ : Type u) (m : Type u → Type v) (α : Type u) :
  Type (max u v)
StateT.{u, v} (σ : Type u)
  (m : Type u → Type v) (α : Type u) :
  Type (max u v)

Adds a mutable state of type σ to a monad.

Actions in the resulting monad are functions that take an initial state and return, in m, a tuple of a value and a state.

def

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 (α × σ)

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value paired with the final state.

def

StateT.get.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] :
  StateT σ m σ
StateT.get.{u, v} {σ : Type u}
  {m : Type u → Type v} [Monad m] :
  StateT σ m σ

Retrieves the current value of the monad's mutable state.

This increments the reference count of the state, which may inhibit in-place updates.

def

StateT.set.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m] :
  σ → StateT σ m PUnit
StateT.set.{u, v} {σ : Type u}
  {m : Type u → Type v} [Monad m] :
  σ → StateT σ m PUnit

Replaces the mutable state with a new value.

def

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 α

Recovers from errors. The state is rolled back on error recovery. Typically used via the <|> operator.

def

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 α

Fails with a recoverable error. The state is rolled back on error recovery.

def

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 α

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value, discarding the final state.

def

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 β

Sequences two actions. Typically used via the >>= operator.

def

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 α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to do let (a, s) := f (← StateT.get); StateT.set s; pure a. However, using StateT.modifyGet may lead to better performance because it doesn't add a new reference to the state value, and additional references can inhibit in-place updates of data.

def

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 α

Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a MonadLiftT instance as part of automatic lifting.

def

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 β

Modifies the value returned by a computation. Typically used via the <$> operator.

def

StateT.pure.{u, v} {σ : Type u} {m : Type u → Type v} [Monad m]
  {α : Type u} (a : α) : StateT σ m α
StateT.pure.{u, v} {σ : Type u}
  {m : Type u → Type v} [Monad m]
  {α : Type u} (a : α) : StateT σ m α

Returns the given value without modifying the state. Typically used via Pure.pure.

18.5.4.3. 连续传递风格的状态单子🔗

延续传递风格的状态单子将状态计算表示为函数，对于任何类型，该函数都采用初始状态和接受值和更新状态的延续（建模为函数）。这种类型的一个例子是 (δ : Type u) → σ → (α → σ → δ) → δ，尽管 StateCpsT 是一个可以应用于任何 monad 的转换器。连续传递风格的状态单子与基于元组的状态单子具有不同的性能特征；对于某些应用程序，可能值得对它们进行基准测试。

def

StateCpsT.{u, v} (σ : Type u) (m : Type u → Type v) (α : Type u) :
  Type (max (u + 1) v)
StateCpsT.{u, v} (σ : Type u)
  (m : Type u → Type v) (α : Type u) :
  Type (max (u + 1) v)

An alternative implementation of a state monad transformer that internally uses continuation passing style instead of tuples.

def

StateCpsT.lift.{u, v} {α σ : Type u} {m : Type u → Type v} [Monad m]
  (x : m α) : StateCpsT σ m α
StateCpsT.lift.{u, v} {α σ : Type u}
  {m : Type u → Type v} [Monad m]
  (x : m α) : StateCpsT σ m α

Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a MonadLiftT instance as part of automatic lifting.

def

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 β

Runs a stateful computation that's represented using continuation passing style by providing it with an initial state and a continuation.

def

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 α

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value, discarding the final state.

def

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 (α × σ)

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value paired with the final state.

While the state is internally represented in continuation passing style, the resulting value is the same as for a non-CPS state monad.

18.5.4.4. 来自可变引用的状态 Monad🔗

monad StateRefT σ m 是一种专用状态 monad 转换器，当 m 是可以将 ST 计算提升到的 monad 时，可以使用它。它使用 ST.Ref 而不是纯函数来实现 MonadState 的操作。这确保了突变在运行时实际使用。

ST 和 EST 需要一个幻像类型参数，该参数与 runST 的多态函数参数一起使用以封装可变性。不需要将此作为变压器的参数，而是使用辅助类型类 STWorld 直接从 m 传播它。

变压器本身被定义为语法扩展和精化器，而不是普通函数。这是因为 STWorld 没有方法：它的存在只是为了将信息从内部 monad 传播到转换后的 monad。然而，它的实例是术语；保留它们可能会导致不必要的大型类型。

type class

STWorld (σ : outParam Type) (m : Type → Type) : Type
STWorld (σ : outParam Type)
  (m : Type → Type) : Type

An auxiliary class used to infer the “state” of EST and ST monads.

Instance Constructor

STWorld.mk

syntaxStateRefT

StateRefT σ m 的语法接受两个参数：

term ::= ...
    | A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref`).

This is syntax, rather than a function, to make it easier to use. Its elaborator synthesizes an
appropriate parameter for the underlying monad's `ST` effects, then passes it to `StateRefT'`.
StateRefT term (macroDollarArg
       | term)

其精化器合成 STWorld ω m 的实例，以确保 m 支持可变引用。发现 ω 的值后，它会生成项 StateRefT' ω σ m，并丢弃合成的实例。

def

StateRefT' (ω σ : Type) (m : Type → Type) (α : Type) : Type
StateRefT' (ω σ : Type) (m : Type → Type)
  (α : Type) : Type

A state monad that uses an actual mutable reference cell (i.e. an ST.Ref ω σ).

The macro StateRefT σ m α infers ω from m. It should normally be used instead.

def

StateRefT'.get {ω σ : Type} {m : Type → Type} [MonadLiftT (ST ω) m] :
  StateRefT' ω σ m σ
StateRefT'.get {ω σ : Type}
  {m : Type → Type}
  [MonadLiftT (ST ω) m] :
  StateRefT' ω σ m σ

Retrieves the current value of the monad's mutable state.

This increments the reference count of the state, which may inhibit in-place updates.

def

StateRefT'.set {ω σ : Type} {m : Type → Type} [MonadLiftT (ST ω) m]
  (s : σ) : StateRefT' ω σ m PUnit
StateRefT'.set {ω σ : Type}
  {m : Type → Type} [MonadLiftT (ST ω) m]
  (s : σ) : StateRefT' ω σ m PUnit

Replaces the mutable state with a new value.

def

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 α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

It is equivalent to a get followed by a set. However, using modifyGet may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.

def

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 (α × σ)

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value paired with the final state.

The monad m must support ST effects in order to create and mutate reference cells.

def

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 α

Executes an action from a monad with added state in the underlying monad m. Given an initial state, it returns a value, discarding the final state.

The monad m must support ST effects in order to create and mutate reference cells.

def

StateRefT'.lift {ω σ : Type} {m : Type → Type} {α : Type} (x : m α) :
  StateRefT' ω σ m α
StateRefT'.lift {ω σ : Type}
  {m : Type → Type} {α : Type} (x : m α) :
  StateRefT' ω σ m α

Runs an action from the underlying monad in the monad with state. The state is not modified.

This function is typically implicitly accessed via a MonadLiftT instance as part of automatic lifting.

18.5.5. 读者🔗

type class

MonadReader.{u, v} (ρ : outParam (Type u)) (m : Type u → Type v) :
  Type v
MonadReader.{u, v} (ρ : outParam (Type u))
  (m : Type u → Type v) : Type v

Reader monads provide the ability to implicitly thread a value through a computation. The value can be read, but not written. A MonadWithReader ρ instance additionally allows the value to be locally overridden for a sub-computation.

In this class, ρ is an outParam, which means that it is inferred from m. MonadReaderOf ρ provides the same operations, but allows ρ to influence instance synthesis.

Instance Constructor

MonadReader.mk.{u, v}

Methods

read : m ρ

Retrieves the local value.

Use readThe to explicitly specify a type when more than one value is available.

type class

MonadReaderOf.{u, v} (ρ : semiOutParam (Type u)) (m : Type u → Type v) :
  Type v
MonadReaderOf.{u, v}
  (ρ : semiOutParam (Type u))
  (m : Type u → Type v) : Type v

In this class, ρ is a semiOutParam, which means that it can influence the choice of instance. MonadReader ρ provides the same operations, but requires that ρ be inferable from m.

Instance Constructor

MonadReaderOf.mk.{u, v}

Methods

read : m ρ

Retrieves the local value.

def

readThe.{u, v} (ρ : Type u) {m : Type u → Type v} [MonadReaderOf ρ m] :
  m ρ
readThe.{u, v} (ρ : Type u)
  {m : Type u → Type v}
  [MonadReaderOf ρ m] : m ρ

Retrieves the local value whose type is ρ. This is useful when a monad supports reading more than one type of value.

Use read for a version that expects the type ρ to be inferred from m.

type class

MonadWithReader.{u, v} (ρ : outParam (Type u)) (m : Type u → Type v) :
  Type (max (u + 1) v)
MonadWithReader.{u, v}
  (ρ : outParam (Type u))
  (m : Type u → Type v) :
  Type (max (u + 1) v)

A reader monad that additionally allows the value to be locally overridden.

In this class, ρ is an outParam, which means that it is inferred from m. MonadWithReaderOf ρ provides the same operations, but allows ρ to influence instance synthesis.

Instance Constructor

MonadWithReader.mk.{u, v}

Methods

withReader : {α : Type u} → (ρ → ρ) → m α → m α

Locally modifies the reader monad's value while running an action.

During the inner action x, reading the value returns f applied to the original value. After control returns from x, the reader monad's value is restored.

type class

MonadWithReaderOf.{u, v} (ρ : semiOutParam (Type u))
  (m : Type u → Type v) : Type (max (u + 1) v)
MonadWithReaderOf.{u, v}
  (ρ : semiOutParam (Type u))
  (m : Type u → Type v) :
  Type (max (u + 1) v)

A reader monad that additionally allows the value to be locally overridden.

In this class, ρ is a semiOutParam, which means that it can influence the choice of instance. MonadWithReader ρ provides the same operations, but requires that ρ be inferable from m.

Instance Constructor

MonadWithReaderOf.mk.{u, v}

Methods

withReader : {α : Type u} → (ρ → ρ) → m α → m α

Locally modifies the reader monad's value while running an action.

During the inner action x, reading the value returns f applied to the original value. After control returns from x, the reader monad's value is restored.

def

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 α

Locally modifies the reader monad's value while running an action, with the reader monad's local value type specified explicitly. This is useful when a monad supports reading more than one type of value.

During the inner action x, reading the value returns f applied to the original value. After control returns from x, the reader monad's value is restored.

Use withReader for a version that expects the local value's type to be inferred from m.

def

ReaderT.{u, v} (ρ : Type u) (m : Type u → Type v) (α : Type u) :
  Type (max u v)
ReaderT.{u, v} (ρ : Type u)
  (m : Type u → Type v) (α : Type u) :
  Type (max u v)

Adds the ability to access a read-only value of type ρ to a monad. The value can be locally overridden by withReader, but it cannot be mutated.

Actions in the resulting monad are functions that take the local value as a parameter, returning ordinary actions in m.

def

ReaderM.{u} (ρ α : Type u) : Type u
ReaderM.{u} (ρ α : Type u) : Type u

A monad with access to a read-only value of type ρ. The value can be locally overridden by withReader, but it cannot be mutated.

def

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 α

Executes an action from a monad with a read-only value in the underlying monad m.

def

ReaderT.read.{u, v} {ρ : Type u} {m : Type u → Type v} [Monad m] :
  ReaderT ρ m ρ
ReaderT.read.{u, v} {ρ : Type u}
  {m : Type u → Type v} [Monad m] :
  ReaderT ρ m ρ

Retrieves the reader monad's local value. Typically accessed via read, or via readThe when more than one local value is available.

def

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 α

Modifies a reader monad's local value with f. The resulting computation applies f to the incoming local value and passes the result to the inner computation.

def

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 α

Returns the provided value a, ignoring the reader monad's local value. Typically used via Pure.pure.

def

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 β

Sequences two reader monad computations. Both are provided with the local value, and the second is passed the value of the first. Typically used via the >>= operator.

def

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 α

Recovers from errors. The same local value is provided to both branches. Typically used via the <|> operator.

def

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 α

Fails with a recoverable error.

18.5.6. 选项🔗

通常，Option 被视为数据，类似于可为 null 的类型。它也可以被视为一个单子，因此是一种执行计算的方式。 Option monad 及其转换器 OptionT 可以理解为描述可能提前终止并丢弃结果的计算。调用者可以使用 OrElse.orElse 或将其视为 MonadExcept Unit 来检查是否提前终止并调用回退（如果需要）。

def

OptionT.{u, v} (m : Type u → Type v) (α : Type u) : Type v
OptionT.{u, v} (m : Type u → Type v)
  (α : Type u) : Type v

Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a failure occurred.

def

OptionT.run.{u, v} {m : Type u → Type v} {α : Type u}
  (x : OptionT m α) : m (Option α)
OptionT.run.{u, v} {m : Type u → Type v}
  {α : Type u} (x : OptionT m α) :
  m (Option α)

Executes an action that might fail in the underlying monad m, returning none in case of failure.

def

OptionT.lift.{u, v} {m : Type u → Type v} [Monad m] {α : Type u}
  (x : m α) : OptionT m α
OptionT.lift.{u, v} {m : Type u → Type v}
  [Monad m] {α : Type u} (x : m α) :
  OptionT m α

Converts a computation from the underlying monad into one that could fail, even though it does not.

This function is typically implicitly accessed via a MonadLiftT instance as part of automatic lifting.

def

OptionT.mk.{u, v} {m : Type u → Type v} {α : Type u}
  (x : m (Option α)) : OptionT m α
OptionT.mk.{u, v} {m : Type u → Type v}
  {α : Type u} (x : m (Option α)) :
  OptionT m α

Converts an action that returns an Option into one that might fail, with none indicating failure.

def

OptionT.pure.{u, v} {m : Type u → Type v} [Monad m] {α : Type u}
  (a : α) : OptionT m α
OptionT.pure.{u, v} {m : Type u → Type v}
  [Monad m] {α : Type u} (a : α) :
  OptionT m α

Succeeds with the provided value.

def

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 β

Sequences two potentially-failing actions. The second action is run only if the first succeeds.

def

OptionT.fail.{u, v} {m : Type u → Type v} [Monad m] {α : Type u} :
  OptionT m α
OptionT.fail.{u, v} {m : Type u → Type v}
  [Monad m] {α : Type u} : OptionT m α

A recoverable failure.

def

OptionT.orElse.{u, v} {m : Type u → Type v} [Monad m] {α : Type u}
  (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α
OptionT.orElse.{u, v}
  {m : Type u → Type v} [Monad m]
  {α : Type u} (x : OptionT m α)
  (y : Unit → OptionT m α) : OptionT m α

Recovers from failures. Typically used via the <|> operator.

def

OptionT.tryCatch.{u, v, u_1} {m : Type u → Type v} [Monad m]
  {α : Type u} (x : OptionT m α) (handle : PUnit → OptionT m α) :
  OptionT m α
OptionT.tryCatch.{u, v, u_1}
  {m : Type u → Type v} [Monad m]
  {α : Type u} (x : OptionT m α)
  (handle : PUnit → OptionT m α) :
  OptionT m α

Handles failures by treating them as exceptions of type Unit.

18.5.7. 例外情况🔗

异常单子描述提前终止（失败）的计算。失败的计算为其调用者提供一个异常值，该值描述了为什么失败。换句话说，计算要么返回一个值，要么返回一个异常。归纳类型Except 捕获了这种模式，并且它本身就是一个 monad。

18.5.7.1. 例外情况🔗

inductive type

Except.{u, v} (ε : Type u) (α : Type v) : Type (max u v)
Except.{u, v} (ε : Type u) (α : Type v) :
  Type (max u v)

Except ε α is a type which represents either an error of type ε or a successful result with a value of type α.

Except ε : Type u → Type v is a Monad that represents computations that may throw exceptions: the pure operation is Except.ok and the bind operation returns the first encountered Except.error.

Constructors

Except.error.{u, v} {ε : Type u} {α : Type v} :
  ε → Except ε α

A failure value of type ε

Except.ok.{u, v} {ε : Type u} {α : Type v} : α → Except ε α

A success value of type α

def

Except.pure.{u, u_1} {ε : Type u} {α : Type u_1} (a : α) : Except ε α
Except.pure.{u, u_1} {ε : Type u}
  {α : Type u_1} (a : α) : Except ε α

A successful computation in the Except ε monad: a is returned, and no exception is thrown.

def

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 ε β

Sequences two operations that may throw exceptions, allowing the second to depend on the value returned by the first.

If the first operation throws an exception, then it is the result of the computation. If the first succeeds but the second throws an exception, then that exception is the result. If both succeed, then the result is the result of the second computation.

This is the implementation of the >>= operator for Except ε.

def

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 ε β

Transforms a successful result with a function, doing nothing when an exception is thrown.

Examples:

(pure 2 : Except String Nat).map toString = pure 2
(throw "Error" : Except String Nat).map toString = throw "Error"

def

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 ε' α

Transforms exceptions with a function, doing nothing on successful results.

Examples:

(pure 2 : Except String Nat).mapError (·.length) = pure 2
(throw "Error" : Except String Nat).mapError (·.length) = throw 5

def

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 ε α

Handles exceptions thrown in the Except ε monad.

If ma is successful, its result is returned. If it throws an exception, then handle is invoked on the exception's value.

Examples:

(pure 2 : Except String Nat).tryCatch (pure ·.length) = pure 2
(throw "Error" : Except String Nat).tryCatch (pure ·.length) = pure 5
(throw "Error" : Except String Nat).tryCatch (fun x => throw ("E: " ++ x)) = throw "E: Error"

def

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 ε α

Recovers from exceptions thrown in the Except ε monad. Typically used via the <|> operator.

Except.tryCatch is a related operator that allows the recovery procedure to depend on which exception was thrown.

def

Except.isOk.{u, u_1} {ε : Type u} {α : Type u_1} : Except ε α → Bool
Except.isOk.{u, u_1} {ε : Type u}
  {α : Type u_1} : Except ε α → Bool

Returns true if the value is Except.ok, false otherwise.

def

Except.toOption.{u, u_1} {ε : Type u} {α : Type u_1} :
  Except ε α → Option α
Except.toOption.{u, u_1} {ε : Type u}
  {α : Type u_1} : Except ε α → Option α

Returns none if an exception was thrown, or some around the value on success.

Examples:

(pure 10 : Except String Nat).toOption = some 10
(throw "Failure" : Except String Nat).toOption = none

def

Except.toBool.{u, u_1} {ε : Type u} {α : Type u_1} : Except ε α → Bool
Except.toBool.{u, u_1} {ε : Type u}
  {α : Type u_1} : Except ε α → Bool

Returns true if the value is Except.ok, false otherwise.

18.5.7.2. Type级🔗

type class

MonadExcept.{u, v, w} (ε : outParam (Type u)) (m : Type v → Type w) :
  Type (max (max u (v + 1)) w)
MonadExcept.{u, v, w}
  (ε : outParam (Type u))
  (m : Type v → Type w) :
  Type (max (max u (v + 1)) w)

Exception monads provide the ability to throw errors and handle errors.

In this class, ε is an outParam, which means that it is inferred from m. MonadExceptOf ε provides the same operations, but allows ε to influence instance synthesis.

MonadExcept.tryCatch is used to desugar try ... catch ... steps inside do-blocks when the handlers do not have exception type annotations.

Instance Constructor

MonadExcept.mk.{u, v, w}

Methods

throw : {α : Type v} → ε → m α

Throws an exception of type ε to the nearest enclosing handler.

tryCatch : {α : Type v} → m α → (ε → m α) → m α

Catches errors thrown in body, passing them to handler. Errors in handler are not caught.

def

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 α

Re-interprets an Except ε action in an exception monad m, succeeding if it succeeds and throwing an exception if it throws an exception.

def

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 α

Unconditional error recovery that ignores which exception was thrown. Usually used via the <|> operator.

If both computations throw exceptions, then the result is the second exception.

def

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 α

An alternative unconditional error recovery operator that allows callers to specify which exception to throw in cases where both operations throw exceptions.

By default, the first is thrown, because the <|> operator throws the second.

type class

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)

Exception monads provide the ability to throw errors and handle errors.

In this class, ε is a semiOutParam, which means that it can influence the choice of instance. MonadExcept ε provides the same operations, but requires that ε be inferable from m.

tryCatchThe, which takes an explicit exception type, is used to desugar try ... catch ... steps inside do-blocks when the handlers have type annotations.

Instance Constructor

MonadExceptOf.mk.{u, v, w}

Methods

throw : {α : Type v} → ε → m α

Throws an exception of type ε to the nearest enclosing catch.

tryCatch : {α : Type v} → m α → (ε → m α) → m α

Catches errors thrown in body, passing them to handler. Errors in handler are not caught.

def

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 α

Throws an exception, with the exception type specified explicitly. This is useful when a monad supports throwing more than one type of exception.

Use throw for a version that expects the exception type to be inferred from m.

def

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 α

Catches errors, recovering using handle. The exception type is specified explicitly. This is useful when a monad supports throwing or handling more than one type of exception.

Use tryCatch, for a version that expects the exception type to be inferred from m.

18.5.7.3. “最后”计算🔗

type class

MonadFinally.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
MonadFinally.{u, v}
  (m : Type u → Type v) :
  Type (max (u + 1) v)

Monads that provide the ability to ensure an action happens, regardless of exceptions or other failures.

MonadFinally.tryFinally' is used to desugar try ... finally ... syntax.

Instance Constructor

MonadFinally.mk.{u, v}

Methods

tryFinally' : {α β : Type u} → m α → (Option α → m β) → m (α × β)

Runs an action, ensuring that some other action always happens afterward.

More specifically, tryFinally' x f runs x and then the “finally” computation f. If x succeeds with some value a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned.

tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

18.5.7.4. 变压器🔗

def

ExceptT.{u, v} (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v
ExceptT.{u, v} (ε : Type u)
  (m : Type u → Type v) (α : Type u) :
  Type v

Adds exceptions of type ε to a monad m.

def

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 α

Runs a computation from an underlying monad in the transformed monad with exceptions.

def

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 ε α)

Use a monadic action that may throw an exception as an action that may return an exception's value.

This is the inverse of ExceptT.mk.

def

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 α

Returns the value a without throwing exceptions or having any other effect.

def

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 β

Sequences two actions that may throw exceptions. Typically used via do-notation or the >>= operator.

def

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 ε β)

Handles exceptions thrown by an action that can have no effects other than throwing exceptions.

def

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 α

Handles exceptions produced in the ExceptT ε transformer.

def

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 α

Use a monadic action that may return an exception's value as an action in the transformed monad that may throw the corresponding exception.

This is the inverse of ExceptT.run.

def

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 β

Transforms a successful computation's value using f. Typically used via the <$> operator.

def

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 α

Transforms exceptions using the function f.

This is the ExceptT version of Except.mapError.

18.5.7.5. 连续传递风格中的异常 Monad🔗

连续传递式异常 monad 将可能失败的计算表示为采用成功和失败连续的函数，这两个连续都返回相同的类型，返回该类型。它们必须适用于 any 返回类型。此类类型的一个示例是 (β : Type u) → (α → β) → (ε → β) → β。 ExceptCpsT是一个可以应用于任何monad的变压器，因此ExceptCpsT ε m α实际上被定义为(β : Type u) → (α → m β) → (ε → m β) → m β。连续传递风格的异常 monad 与基于 Except 的状态 monad 相比具有不同的性能特征；对于某些应用程序，可能值得对它们进行基准测试。

def

ExceptCpsT.{u, v} (ε : Type u) (m : Type u → Type v) (α : Type u) :
  Type (max (u + 1) v)
ExceptCpsT.{u, v} (ε : Type u)
  (m : Type u → Type v) (α : Type u) :
  Type (max (u + 1) v)

Adds exceptions of type ε to a monad m.

Instead of using Except ε to model exceptions, this implementation uses continuation passing style. This has different performance characteristics from ExceptT ε.

def

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 α

Returns the value of a computation, forgetting whether it was an exception or a success.

This corresponds to early return.

def

ExceptCpsT.runK.{u, u_1} {m : Type u → Type u_1} {β ε α : Type u}
  (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β
ExceptCpsT.runK.{u, u_1}
  {m : Type u → Type u_1} {β ε α : Type u}
  (x : ExceptCpsT ε m α) (s : ε)
  (ok : α → m β) (error : ε → m β) : m β

Use a monadic action that may throw an exception by providing explicit success and failure continuations.

def

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 ε α)

Use a monadic action that may throw an exception as an action that may return an exception's value.

def

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 α

Run an action from the transformed monad in the exception monad.

18.5.8. 组合错误和状态 Monad🔗

EStateM monad 具有异常和可变状态。 EStateM ε σ α 在逻辑上等同于 ExceptT ε (StateM σ) α。 ExceptT ε (StateM σ) 计算结果为 σ → Except ε α × σ 类型，而 EStateM ε σ α 计算结果为 σ → EStateM.Result ε σ α。 EStateM.Result 是一个归纳类型，它与 Except 非常相似，只是两个构造函数都有一个附加的状态字段。在编译的代码中，这种表示形式从每个单子绑定中删除了一层间接。

def

EStateM.{u} (ε σ α : Type u) : Type u
EStateM.{u} (ε σ α : Type u) : Type u

A combined state and exception monad in which exceptions do not automatically roll back the state.

Instances of EStateM.Backtrackable provide a way to roll back some part of the state if needed.

EStateM ε σ is equivalent to ExceptT ε (StateM σ), but it is more efficient.

inductive type

EStateM.Result.{u} (ε σ α : Type u) : Type u
EStateM.Result.{u} (ε σ α : Type u) :
  Type u

The value returned from a combined state and exception monad in which exceptions do not automatically roll back the state.

Result ε σ α is equivalent to Except ε α × σ, but using a single combined inductive type yields a more efficient data representation.

Constructors

EStateM.Result.ok.{u} {ε σ α : Type u} :
  α → σ → EStateM.Result ε σ α

A success value of type α and a new state σ.

EStateM.Result.error.{u} {ε σ α : Type u} :
  ε → σ → EStateM.Result ε σ α

An exception of type ε and a new state σ.

def

EStateM.run.{u} {ε σ α : Type u} (x : EStateM ε σ α) (s : σ) :
  EStateM.Result ε σ α
EStateM.run.{u} {ε σ α : Type u}
  (x : EStateM ε σ α) (s : σ) :
  EStateM.Result ε σ α

Executes an EStateM action with the initial state s. The returned value includes the final state and indicates whether an exception was thrown or a value was returned.

def

EStateM.run'.{u} {ε σ α : Type u} (x : EStateM ε σ α) (s : σ) : Option α
EStateM.run'.{u} {ε σ α : Type u}
  (x : EStateM ε σ α) (s : σ) : Option α

Executes an EStateM with the initial state s for the returned value α, discarding the final state. Returns none if an unhandled exception was thrown.

def

EStateM.adaptExcept.{u} {ε σ α ε' : Type u} (f : ε → ε')
  (x : EStateM ε σ α) : EStateM ε' σ α
EStateM.adaptExcept.{u}
  {ε σ α ε' : Type u} (f : ε → ε')
  (x : EStateM ε σ α) : EStateM ε' σ α

Transforms exceptions with a function, doing nothing on successful results.

def

EStateM.fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α
EStateM.fromStateM {ε σ α : Type}
  (x : StateM σ α) : EStateM ε σ α

Converts a state monad action into a state monad action with exceptions.

The resulting action does not throw an exception.

18.5.8.1. 状态回滚🔗

以不同顺序组合 StateT 和 ExceptT 会导致异常与状态的交互方式不同。在一种顺序中，当捕获异常时，状态更改会回滚；另一方面，他们坚持不懈。后一个选项与大多数命令式编程语言的语义相匹配，但前者对于基于搜索的问题非常有用。通常，一些但不是全部状态应该回滚；这可以通过将 ExceptT“夹在”StateT 的两个单独用途之间来实现。

为了避免通过使用 StateT σ (EStateM ε σ') α 产生另一层间接，EStateM 提供了 EStateM.Backtrackable 类型类别。此类指定可以保存和恢复的状态的某些部分。然后，EStateM 安排围绕错误处理进行保存和恢复。

type class

EStateM.Backtrackable.{u} (δ : outParam (Type u)) (σ : Type u) : Type u
EStateM.Backtrackable.{u}
  (δ : outParam (Type u)) (σ : Type u) :
  Type u

Exception handlers in EStateM save some part of the state, determined by δ, and restore it if an exception is caught. By default, δ is Unit, and no information is saved.

Instance Constructor

EStateM.Backtrackable.mk.{u}

Methods

save : σ → δ

Extracts the information in the state that should be rolled back if an exception is handled.

restore : σ → δ → σ

Updates the current state with the saved information that should be rolled back. This updated state becomes the current state when an exception is handled.

有一个普遍适用的 Backtrackable 实例，既不保存也不恢复任何内容。由于实例合成首先选择最近的实例，因此只有在没有定义其他实例的情况下才会使用通用实例。

def

EStateM.nonBacktrackable.{u} {σ : Type u} :
  EStateM.Backtrackable PUnit σ
EStateM.nonBacktrackable.{u}
  {σ : Type u} :
  EStateM.Backtrackable PUnit σ

A fallback Backtrackable instance that saves no information from a state. This allows every type to be used as a state in EStateM, with no rollback.

Because this is the first declared instance of Backtrackable _ σ, it will be picked only if there are no other Backtrackable _ σ instances registered.

18.5.8.2. 实施🔗

这些函数通常不直接调用，而是通过其相应的类型类访问。

def

EStateM.map.{u} {ε σ α β : Type u} (f : α → β) (x : EStateM ε σ α) :
  EStateM ε σ β
EStateM.map.{u} {ε σ α β : Type u}
  (f : α → β) (x : EStateM ε σ α) :
  EStateM ε σ β

Transforms the value returned from an EStateM ε σ action using a function.

def

EStateM.pure.{u} {ε σ α : Type u} (a : α) : EStateM ε σ α
EStateM.pure.{u} {ε σ α : Type u}
  (a : α) : EStateM ε σ α

Returns a value without modifying the state or throwing an exception.

def

EStateM.bind.{u} {ε σ α β : Type u} (x : EStateM ε σ α)
  (f : α → EStateM ε σ β) : EStateM ε σ β
EStateM.bind.{u} {ε σ α β : Type u}
  (x : EStateM ε σ α)
  (f : α → EStateM ε σ β) : EStateM ε σ β

Sequences two EStateM ε σ actions, passing the returned value from the first into the second.

def

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 ε σ α

Failure handling that does not depend on specific exception values.

The Backtrackable δ σ instance is used to save a snapshot of part of the state prior to running x₁. If an exception is caught, the state is updated with the saved snapshot, rolling back part of the state. If no instance of Backtrackable is provided, a fallback instance in which δ is Unit is used, and no information is rolled back.

def

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 ε σ α

Alternative orElse operator that allows callers to select which exception should be used when both operations fail. The default is to use the first exception since the standard orElse uses the second.

def

EStateM.seqRight.{u} {ε σ α β : Type u} (x : EStateM ε σ α)
  (y : Unit → EStateM ε σ β) : EStateM ε σ β
EStateM.seqRight.{u} {ε σ α β : Type u}
  (x : EStateM ε σ α)
  (y : Unit → EStateM ε σ β) :
  EStateM ε σ β

Sequences two EStateM ε σ actions, running x before y. The first action's return value is ignored.

def

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 ε σ α

Handles exceptions thrown in the combined error and state monad.

The Backtrackable δ σ instance is used to save a snapshot of part of the state prior to running x. If an exception is caught, the state is updated with the saved snapshot, rolling back part of the state. If no instance of Backtrackable is provided, a fallback instance in which δ is Unit is used, and no information is rolled back.

def

EStateM.throw.{u} {ε σ α : Type u} (e : ε) : EStateM ε σ α
EStateM.throw.{u} {ε σ α : Type u}
  (e : ε) : EStateM ε σ α

Throws an exception of type ε to the nearest enclosing handler.

def

EStateM.get.{u} {ε σ : Type u} : EStateM ε σ σ
EStateM.get.{u} {ε σ : Type u} :
  EStateM ε σ σ

Retrieves the current value of the monad's mutable state.

def

EStateM.set.{u} {ε σ : Type u} (s : σ) : EStateM ε σ PUnit
EStateM.set.{u} {ε σ : Type u} (s : σ) :
  EStateM ε σ PUnit

Replaces the current value of the mutable state with a new one.

def

EStateM.modifyGet.{u} {ε σ α : Type u} (f : σ → α × σ) : EStateM ε σ α
EStateM.modifyGet.{u} {ε σ α : Type u}
  (f : σ → α × σ) : EStateM ε σ α

Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.

18.1.	法律
18.2.	提升单子
18.3.	句法
18.4.	API 参考
18.5.	单子的种类