6.2. 单子构建工具包🔗

ReaderT 并不是唯一有用的单子转换器。本节将介绍一些额外的转换器。每个单子转换器都由以下部分组成：

一个以单子为参数定义或数据类型 T。它的类型应类似于 (Type u → Type v) → Type u → Type v，尽管它可以接受单子之前的其他参数。
T m 的 Monad 实例依赖于 Monad m 实例。这使得转换后的单子也可以作为单子使用。
一个 MonadLift 实例，可将任意单子 m 的 m α 类型的操作转换为 T m α 类型的操作。这使得底层单子中的操作可以在转换后的单子中使用。

此外，转换器的 Monad 实例也应该遵守 Monad 的约定，至少在底层的 Monad 实例遵守的情况下。另外，monadLift (pure x : m α) 应该等价于转换后的单子中的 pure x ，而且 monadLift 应对于 bind 可分配，这样 monadLift (x >>= f : m α) 就等同于 (monadLift x : m α) >>= fun y => monadLift (f y) 。

许多单子转换器还定义了 MonadReader 风格的类型类，用于描述单子中可用的实际作用。这可以提供更大的灵活性：它允许编写只依赖接口的程序，而不限制底层单子必须由给定的转换器实现。类型类是程序表达其需求的一种方式，而单子转换器则是满足这些需求的一种便捷方式。

6.2.1. 使用 `OptionT` 失败🔗

由 Option 单子表示的失败和由 Except 单子表示的异常都有相应的转换器。对于 Option 单子，可以通过让单子包含 Option α 类型的值来为单子添加失败，否则单子将包含 α 类型的值。例如，IO (Option α) 表示并不总是返回 α 类型值的 IO 操作。这就需要定义单子转换器 OptionT：

def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
  m (Option α)

我们以一个向用户提问的程序为例来说明 OptionT 的作用。函数 getSomeInput 要求输入一行内容，并删除两端的空白。如果修剪后的输入是非空的，就会返回，但如果没有非空格字符，函数就会失败：

def getSomeInput : OptionT IO String := do
  let input ← (← IO.getStdin).getLine
  let trimmed := input.trim
  if trimmed == "" then
    failure
  else pure trimmed

这个应用软件可以追踪用户的姓名和他们最喜欢的甲虫种类：

structure UserInfo where
  name : String
  favoriteBeetle : String

询问用户输入并不比只使用 IO 的函数更冗长：

def getUserInfo : OptionT IO UserInfo := do
  IO.println "What is your name?"
  let name ← getSomeInput
  IO.println "What is your favorite species of beetle?"
  let beetle ← getSomeInput
  pure ⟨name, beetle⟩

然而，由于函数是在 OptionT IO 上下文中运行的，而不仅仅是在 IO 中，因此第一次调用 getSomeInput 失败会导致整个 getUserInfo 失败，控制权永远不会到达关于甲虫的问题。主函数 interact 在纯的 IO 上下文中调用 getUserInfo，这样就可以通过匹配内部的 Option 来检查调用成功还是失败：

def interact : IO Unit := do
  match ← getUserInfo with
  | none =>
    IO.eprintln "Missing info"
  | some ⟨name, beetle⟩ =>
    IO.println s!"Hello {name}, whose favorite beetle is {beetle}."

6.2.1.1. 单子实例🔗

在编写单子实例发现了一个难题。根据类型，pure 应该使用底层单子 m 中的 pure 和 some。正如 Option 的 bind 在第一个参数上分支，然后传播 none，OptionT 的 bind 应该运行构成第一个参数的单子操作，在结果上分支，然后传播 none。按照这个框架可以得到 Lean 不接受的如下定义：

instance [Monad m] : Monad (OptionT m) where
  pure x := failed to synthesize
  Pure (OptionT m)

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.pure Application type mismatch: The argument
  some x
has type
  Option α✝
but is expected to have type
  α✝
in the application
  pure (some x)(some x)
  bind action next := do
    failed to synthesize
  Bind (OptionT m)

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.match (← action) with
    | Type mismatch
  none
has type
  Option ?m.24
but is expected to have type
  α✝none => pure none
    | some v => next v

错误信息显示了一个隐含的类型不匹配：

Application type mismatch: The argument
  some x
has type
  Option α✝
but is expected to have type
  α✝
in the application
  pure (some x)

这里的问题是 Lean 为周围的 pure 使用选择了错误的 Monad 实例。类似的错误也发生在 bind 的定义中。一种解决方案是使用类型标注来引导 Lean 选择正确的 Monad 实例：

instance [Monad m] : Monad (OptionT m) where
  pure x := (pure (some x) : m (Option _))
  bind action next := (do
    match (← action) with
    | none => pure none
    | some v => next v : m (Option _))

虽然这种解决方案可行，但它不够优雅，代码也变得有点啰嗦。

另一种解决方案是定义函数，由函数的类型签名引导 Lean 找到正确的实例。事实上，OptionT 自身可以定义为一个结构：

structure OptionT (m : Type u → Type v) (α : Type u) : Type v where
  run : m (Option α)

这可以解决这个问题，因为构造函数 OptionT.mk 和字段访问函数 OptionT.run 将引导类型类推理到正确的实例。但这样做的缺点是，生成的代码会更复杂，而且这些结构会使阅读证明更加困难。我们可以通过定义与构造函数 OptionT.mk 和字段 OptionT.run 具有相同作用的函数来实现两全其美的效果，但这些函数要与直接定义一起使用：

def OptionT.mk (x : m (Option α)) : OptionT m α := x

def OptionT.run (x : OptionT m α) : m (Option α) := x

这两个函数直接返回的其原输入，但它们指明了旨在呈现 OptionT 接口的代码与旨在呈现底层单子 m 接口的代码之间的边界。使用这些辅助函数，Monad 实例变得更加可读：

instance [Monad m] : Monad (OptionT m) where
  pure x := OptionT.mk (pure (some x))
  bind action next := OptionT.mk do
    match ← action with
    | none => pure none
    | some v => next v

在这里，使用 OptionT.mk 表示其参数应被视为使用 m 接口的代码，它允许 Lean 选择正确的 Monad 实例。

定义完单子实例后，最好检查一下单子约定是否满足。第一步是证明 bind (pure v) f 与 f v 相同。步骤如下：

bind (pure v) f

Unfolding the definitions of bind and pure

OptionT.mk do
  match ← pure (some v) with
  | none => pure none
  | some x => f x

Desugaring nested action syntax

OptionT.mk do
  let y ← pure (some v)
  match y with
  | none => pure none
  | some x => f x

Desugaring do-notation

OptionT.mk
  (pure (some v) >>= fun y =>
    match y with
    | none => pure none
    | some x => f x)

Using the first monad rule for m

OptionT.mk
  (match some v with
   | none => pure none
   | some x => f x)

Reduce match

OptionT.mk (f v)

Definition of OptionT.mk

f v

第二条规则指出，bind w pure 与 w 相同。为了证明这一点，展开 bind 和 pure 的定义，得出：

OptionT.mk do
    match ← w with
    | none => pure none
    | some v => pure (some v)

在这个模式匹配中，两种情况的结果都与被匹配的模式相同，只是在其周围加上了 pure。换句话说，它等同于 w >>= fun y => pure y，这是 m 的第二个单子规则的一个实例。

最后一条规则指出 bind (bind v f) g 与 bind v (fun x => bind (f x) g) 相同。通过扩展 bind 和 pure 的定义，然后将其委托给底层单子 m，可以用同样的方法对其进行检查。

6.2.1.2. 一个 `Alternative` 实例🔗

一种使用 OptionT 的便捷方法是通过 Alternative 类型类。成功返回已经由 pure 表示，而 Alternative 的 failure 和 orElse 方法提供了一种编写程序的方式，可以从多个子程序中返回第一个成功的结果：

instance [Monad m] : Alternative (OptionT m) where
  failure := OptionT.mk (pure none)
  orElse x y := OptionT.mk do
    match ← x with
    | some result => pure (some result)
    | none => y ()

6.2.1.3. 提升🔗

将一个操作从 m 移植到 OptionT m 只需要用 some 包装计算结果：

instance [Monad m] : MonadLift m (OptionT m) where
  monadLift action := OptionT.mk do
    pure (some (← action))

6.2.2. 异常🔗

单子转换器版本的 Except 与单子转换器版本的 Option 非常相似。向 m α 类型的单子动作添加 ε 类型的异常，可以通过向 α 添加异常来实现，从而产生 m (Except ε α)：

def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
  m (Except ε α)

OptionT 提供了 OptionT.mk 和 OptionT.run 函数来引导类型检查器找到正确的 Monad 实例。这个技巧对 ExceptT 也很有用：

def ExceptT.mk {ε α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x

def ExceptT.run {ε α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x

用于 ExceptT 的 Monad 实例与用于 OptionT 的实例也非常相似。唯一不同的是，它传播的是一个特定的错误值，而不是 none：

instance {ε : Type u} {m : Type u → Type v} [Monad m] :
    Monad (ExceptT ε m) where
  pure x := ExceptT.mk (pure (Except.ok x))
  bind result next := ExceptT.mk do
    match ← result with
    | .error e => pure (.error e)
    | .ok x => next x

ExceptT.mk 和 ExceptT.run 的类型签名包含一个微妙的细节：它们明确地注释了 α 和 ε 的宇宙层级。如果它们没有被明确注释，那么 Lean 会生成一个更通用的类型签名，其中它们拥有不同的多态宇宙变量。然而， ExceptT 的定义希望它们在同一个宇宙中，因为它们都可以作为参数提供给 m。这会导致 Monad 实例出现问题，即宇宙层级求解器无法找到有效的解决方案：

def ExceptT.mk (x : m (Except ε α)) : ExceptT ε m α := x

instance {ε : Type u} {m : Type u → Type v} [Monad m] :
    Monad (ExceptT ε m) stuck at solving universe constraint
  max ?u.18963 ?u.18964 =?= u
while trying to unify
  ExceptT ε m β✝ : Type v
with
  ExceptT.{max ?u.18964 ?u.18963, v} ε m β✝ : Type vstuck at solving universe constraint
  max ?u.18795 ?u.18796 =?= u
while trying to unify
  ExceptT ε m α✝ : Type v
with
  ExceptT.{max ?u.18796 ?u.18795, v} ε m α✝ : Type vwhere
  pure x := ExceptT.mk (pure (Except.ok x))
  bind result next := ExceptT.mk do
    match (← result) with
    | stuck at solving universe constraint
  max ?u.18795 ?u.18796 =?= u
while trying to unify
  ExceptT ε m α✝ : Type v
with
  ExceptT.{max ?u.18796 ?u.18795, v} ε m α✝ : Type v.error e => pure (.error e)
    | .ok x => next x

stuck at solving universe constraint
  max ?u.18963 ?u.18964 =?= u
while trying to unify
  ExceptT ε m β✝ : Type v
with
  ExceptT.{max ?u.18964 ?u.18963, v} ε m β✝ : Type v

这种错误信息通常是由欠约束的宇宙变量引起的。诊断起来可能很棘手，但第一步可以查找某些定义中重复使用的宇宙变量，而其他定义中没有重复使用的宇宙变量。

与 Option 不同，Except 数据类型通常不作为数据结构使用。它总是作为控制结构与其 Monad 实例一起使用。这意味着将 Except ε 操作提升到 ExceptT ε m 以及对底层单子 m 的操作都是合理的。通过用 m 的 pure 对 Except 操作进行包装，可以将其提升为 ExceptT 操作，因为一个只有异常作用的动作不可能有来自单子 m 的任何作用：

instance [Monad m] : MonadLift (Except ε) (ExceptT ε m) where
  monadLift action := ExceptT.mk (pure action)

由于 m 中的操作不包含任何异常，因此它们的值应该用 Except.ok 封装。这可以利用 Functor 是 Monad 的超类这一事实来实现，因此可以使用 Functor.map，将函数应用于任何单子计算的结果：

instance [Monad m] : MonadLift m (ExceptT ε m) where
  monadLift action := ExceptT.mk (.ok <$> action)

6.2.2.1. 异常的类型类🔗

异常处理从根本上说包括两种操作：抛出异常的能力和恢复异常的能力。到目前为止，我们分别使用 Except 的构造函数和模式匹配来实现这一点。然而，这将使用异常的程序与异常处理作用的特定编码联系在一起。使用类型类来捕获这些操作，可以让使用异常的程序在任何支持抛出和捕获的单子中使用。

抛出异常应该以异常作为参数，而且应该允许在任何要求执行单子动作的上下文中抛出异常。规范中 “任何上下文” 的部分可以写成一种类型，即 m α ——— 因为没有办法产生任意类型的值，所以 throw 操作必须能使控制权离开程序的这一部分。捕获异常应该接受任何单子操作和处理程序，处理程序应该解释如何从异常返回到操作的类型：

class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where
  throw : ε → m α
  tryCatch : m α → (ε → m α) → m α

MonadExcept 的宇宙层级与 ExceptT 不同。在 ExceptT 中，ε 和 α 具有相同的层级，而 MonadExcept 则没有这种限制。这是因为 MonadExcept 从不将异常值置于 m 内。在这个定义中，最通用的宇宙签名承认 ε 和 α 是完全独立的。更通用意味着类型类可以为更多类型实例化。

下面是一个简单的除法服务，作为使用 MonadExcept 的一个示例程序。程序分为两部分：前端提供基于字符串的用户界面，用于处理错误；后端实际执行除法操作。前后端都可以抛出异常，前者用于处理格式错误的输入，后者用于处理除数为零的错误。定义异常为一种归纳类型：

inductive Err where
  | divByZero
  | notANumber : String → Err

后端检查是否为零，如果为零，则进行除法：

def divBackend [Monad m] [MonadExcept Err m] (n k : Int) : m Int :=
  if k == 0 then
    throw .divByZero
  else pure (n / k)

如果传入的字符串不是数字，前端的辅助函数 asNumber 会抛出异常。整个前端会将输入转换为 Int 并调用后端，通过返回友好的错误字符串来处理异常：

def asNumber [Monad m] [MonadExcept Err m] (s : String) : m Int :=
  match s.toInt? with
  | none => throw (.notANumber s)
  | some i => pure i

def divFrontend [Monad m] [MonadExcept Err m] (n k : String) : m String :=
  tryCatch (do pure (toString (← divBackend (← asNumber n) (← asNumber k))))
    fun
      | .divByZero => pure "Division by zero!"
      | .notANumber s => pure s!"Not a number: \"{s}\""

抛出和捕获异常非常常见，因此 Lean 提供了使用 MonadExcept 的特殊语法。正如 + 是 HAdd.hAdd 的缩写，try 和 catch 可以作为 tryCatch 方法的缩写：

def divFrontend [Monad m] [MonadExcept Err m] (n k : String) : m String :=
  try
    pure (toString (← divBackend (← asNumber n) (← asNumber k)))
  catch
    | .divByZero => pure "Division by zero!"
    | .notANumber s => pure s!"Not a number: \"{s}\""

除了 Except 和 ExceptT 之外，还有一些有用的 MonadExcept 实例，用于处理其他类型的异常，这些异常乍看起来可能不像是异常。例如，Option 导致的失败可以被看作是抛出了一个不包含任何数据的异常，因此有一个实例 MonadExcept Unit Option 允许将 try ...catch ... 语法与 Option 一起使用。

6.2.3. 状态🔗

通过让单子动作接受一个起始状态作为参数，并返回一个最终状态及其结果，就可以在单子中加入对可变状态的模拟。状态单子的绑定操作符将一个动作的最终状态作为下一个动作的参数，从而将状态贯穿整个程序。这种模式也可以用单子转换器来表示：

def StateT (σ : Type u)
    (m : Type u → Type v) (α : Type u) : Type (max u v) :=
  σ → m (α × σ)

同样，该单子实例与 State 非常相似。唯一不同的是，输入和输出状态是在底层单子中传递和返回的，而不是纯代码：

instance [Monad m] : Monad (StateT σ m) where
  pure x := fun s => pure (x, s)
  bind result next := fun s => do
    let (v, s') ← result s
    next v s'

相应的类型类有 get 和 set 方法。 get 和 set 的一个缺点是，在更新状态时很容易 set 错误的状态。这是因为检索状态、更新状态并保存更新后的状态是编写某些程序的一种很自然的方式。例如，下面的程序会计算一串字母中不含音素的英语元音和辅音的数量：

structure LetterCounts where
  vowels : Nat
  consonants : Nat
deriving Repr

inductive Err where
  | notALetter : Char → Err
deriving Repr

def vowels :=
  let lowerVowels := "aeiuoy"
  lowerVowels ++ lowerVowels.map (·.toUpper)

def consonants :=
  let lowerConsonants := "bcdfghjklmnpqrstvwxz"
  lowerConsonants ++ lowerConsonants.map (·.toUpper )

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  let rec loop (chars : List Char) := do
    match chars with
    | [] => pure ()
    | c :: cs =>
      let st ← get
      let st' ←
        if c.isAlpha then
          if vowels.contains c then
            pure {st with vowels := st.vowels + 1}
          else if consonants.contains c then
            pure {st with consonants := st.consonants + 1}
          else -- modified or non-English letter
            pure st
        else throw (.notALetter c)
      set st'
      loop cs
  loop str.toList

非常容易将 set st 误写成 set st' 。在大型程序中，这种错误会导致难以诊断的 bug。

虽然使用嵌套操作来调用 get 可以解决这个问题，但它不能解决所有此类问题。例如，一个函数可能会根据另外两个字段的值来更新结构体上的一个字段。这就需要对 get 进行两次单独的嵌套操作调用。由于 Lean 编译器包含的优化功能只有在对值进行单个引用时才有效，因此重复引用状态可能会导致代码速度大大降低。使用 modify（即使用函数转换状态）可以解决潜在的性能问题和 bug：

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  let rec loop (chars : List Char) := do
    match chars with
    | [] => pure ()
    | c :: cs =>
      if c.isAlpha then
        if vowels.contains c then
          modify fun st => {st with vowels := st.vowels + 1}
        else if consonants.contains c then
          modify fun st => {st with consonants := st.consonants + 1}
        else -- modified or non-English letter
          pure ()
      else throw (.notALetter c)
      loop cs
  loop str.toList

类型类包含一个类似于 modify 的函数，称为 modifyGet，它允许函数在一个步骤中同时计算返回值和转换旧状态。该函数返回一个二元组，其中第一个元素是返回值，第二个元素是新状态；modify 只是将 Unit 的构造函数添加到 modifyGet 中使用的二元组中：

def modify [MonadState σ m] (f : σ → σ) : m Unit :=
  modifyGet fun s => ((), f s)

MonadState 的定义如下：

class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :
    Type (max (u+1) v) where
  get : m σ
  set : σ → m PUnit
  modifyGet : (σ → α × σ) → m α

PUnit 是 Unit 类型的一个版本，它具有宇宙多态性，允许以 Type u 代替 Type。虽然可以用 get 和 set 来提供 modifyGet 的默认实现，但这样就无法进行使 modifyGet 有用的优化，从而使该方法变得无用。

6.2.4. `Of` 类和 `The` 函数🔗

到目前为止，每个需要额外信息的单子类型类，如 MonadExcept 的异常类型或 MonadState 的状态类型，都有这类额外信息作为输出参数。对于简单的程序来说，这通常很方便，因为结合使用了 StateT、ReaderT 和 ExceptT 的单子只有单一的状态类型、环境类型和异常类型。然而，随着单子的复杂性增加，它们可能会涉及多个状态或错误类型。在这种情况下，输出参数的使用使得无法在同一个 do 块中同时针对两种状态。

应对这些情况，还有一些额外的类型类，其中的额外信息不是输出参数。这些版本的类型类在名称中使用了 Of 字样。例如，MonadStateOf 与 MonadState 类似，但没有 outParam 修饰符。

这些类使用 semiOutParam 来表示各自的状态、环境或异常类型，而不是 outParam。与 outParam 一样，semiOutParam 也不需要在 Lean 开始搜索实例之前就知道。但是，有一个重要的区别：outParam 在搜索实例时会被忽略，因此它们是真正的输出。如果在搜索之前就知道了一个 outParam，那么 Lean 只会检查搜索结果是否与已知结果相同。另一方面，如果在搜索开始前就知道了一个 semiOutParam，那么它就可以像输入参数一样用来缩小候选范围。

当状态单子的状态类型是 outParam 时，每个单子最多只能有一种状态类型。这很方便，因为它改进了类型推断：可以在更多情况下推断出状态类型。但这也很不方便，因为由多次使用 StateT 构建的单子无法提供有用的 MonadState 实例。然而，使用 MonadStateOf 会让 Lean 在选择使用哪个实例时考虑状态类型，因此一个单子可以提供多种类型的状态。这样做的缺点是，如果状态类型没有被明确指定，得到的实例可能不是预期的实例，从而导致令人困惑的错误信息。

同样，也有一些版本的类型类方法接受额外信息的类型作为显式参数，而不是隐式参数。对于 MonadStateOf，有 getThe，类型为

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

以及 modifyThe，类型为

(σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → (σ → σ) → m PUnit

没有 setThe 函数，因为新状态的类型足以决定使用哪个状态单子转换器。

在 Lean 标准库中，有非 Of 版本的类型类实例是根据带 Of 版本的类型类实例定义的。换句话说，实现 Of 版本可以同时实现这两个版本。一般来说，实现 Of 版本是个好主意，然后开始使用类的非 Of 版本编写程序，如果输出参数变得不方便，就过渡到 Of 版本。

6.2.5. 转换器和 `Id`🔗

恒等单子 Id 是没有任何作用的单子，可用于上下文因某种原因需要单子，但实际上不需要的情况。 Id 的另一个用途是作为单子转换器栈的底层。例如，StateT σ Id 的作用与 State σ 相同。

6.2.6. 练习🔗

6.2.6.1. 单子约定🔗

用纸笔检查本节中每个单子转换器是否符合单子转换器的规则。

6.2.6.2. 日志转换器🔗

定义 WithLog 的单子转换器版本。同时定义相应的类型类 MonadWithLog，并编写一个结合日志和异常的程序。

6.2.6.3. 文件计数🔗

用 StateT 来修改 doug 的单子，使它能统计所看到的目录和文件的数量。在执行结束时，它应该显示如下报告：

  Viewed 38 files in 5 directories.