Lean 函数式编程(三) | 单子

Monads

在 C# 和 Kotlin 中，?. 运算符是一种在可能为 null 的值上查找属性或调用方法的方式。如果 ?. 前的值为 null，则整个表达式为 null。否则，该非 null 值会被用于调用。多个 ?. 可以链接起来，在这种情况下，第一个 null 结果将终止查找链。像这样链接 null 检查比编写和维护深层嵌套的 if 语句方便得多。

类似地，异常机制比手动检查和传递错误码方便得多。同时，通过使用专用的日志记录框架（而不是让每个函数同时返回其日志结果和返回值）可以轻松地完成日志记录。链式的空值检查和异常通常要求语言设计者预先考虑这种用法，而日志记录框架通常利用副作用将记录日志的代码与日志的累积解耦。

所有这些功能以及更多功能都可以作为通用 API —— Monad 的实例在库代码中实现。Lean 提供了专门的语法，使此 API 易于使用，但也可能会妨碍理解幕后发生的事情。本章从手动嵌套空值检查的细节介绍开始，并由此构建到方便、通用的 API。在此期间，请暂时搁置你的怀疑。

检查none：避免重复代码

在 Lean 中，模式匹配可用于链式的空值检查。从列表中获取第一个元素可以使用可选的索引记号：

def first (xs : List α) : Option α :=
  xs[0]?

结果必须是 Option 类型，因为空列表没有第一个元素。提取第一个和第三个元素需要检查每个元素都不为 none：

def firstThird (xs : List α) : Option (α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      some (first, third)

类似地，提取第一个、第三个和第五个元素需要更多检查，以确保这些值不是 none：

def firstThirdFifth (xs : List α) : Option (α × α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      match xs[4]? with
      | none => none
      | some fifth =>
        some (first, third, fifth)

而将第七个元素添加到此序列中则开始变得相当难以管理：

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      match xs[4]? with
      | none => none
      | some fifth =>
        match xs[6]? with
        | none => none
        | some seventh =>
          some (first, third, fifth, seventh)

这段代码的根本问题在于它处理了两个关注点：提取数字和检查它们是否全部存在，但第二个关注点是通过复制粘贴处理 none 情况的代码来解决的。通常良好的编程风格是将重复的片段提取到辅助函数中：

def andThen (opt : Option α) (next : α → Option β) : Option β :=
  -- if opt 不存在，直接返回 none，else 返回 next x
  match opt with
  | none => none
  | some x => next x

该辅助函数类似于 C# 和 Kotlin 中的 ?.，用于传播 none 值。它接受两个参数：一个可选值和一个在该值非 none 时应用的函数。如果第一个参数是 none，则辅助函数返回 none。如果第一个参数不是 none，则该函数将应用于 some 构造器的内容。

现在，firstThird 可以使用 andThen 重写：

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? fun first =>
  andThen xs[2]? fun third =>
  some (first, third)

在 Lean 中，作为参数传递时，函数不需要用括号括起来。以下等价定义使用了更多括号并缩进了函数体：

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? (fun first =>
    andThen xs[2]? (fun third =>
      some (first, third)))

andThen辅助函数提供了一种让值流过的“管道”，具有特殊缩进的版本更能说明这一事实。改进 andThen的语法可以使其更容易阅读和理解。

中缀运算符

在 Lean 中，可以使用 infix、infixl 和 infixr 命令声明中缀运算符，分别用于非结合、左结合和右结合的情况。当连续多次使用时，左结合运算符会将（开）括号堆叠在表达式的左侧。加法运算符 + 是左结合的，因此 w + x + y + z 等价于 (((w + x) + y) + z)。指数运算符 ^ 是右结合的，因此 w ^ x ^ y ^ z 等价于 (w ^ (x ^ (y ^ z)))。比较运算符（如 <）是非结合的，因此 x < y < z 是一个语法错误，需要手动添加括号。

以下声明将 andThen 声明为中缀运算符：

infixl:55 " ~~> " => andThen

冒号后面的数字声明了新中缀运算符的优先级。在一般的数学记号中，x + y * z 等价于 x + (y * z)，即使 + 和 * 都是左结合的。在 Lean 中，+ 的优先级为 65，* 的优先级为 70。优先级更高的运算符应用于优先级较低的运算符之前。根据 ~~> 的声明，+ 和 * 都具有更高的优先级，因此会被首先计算。通常来说，找出最适合一组运算符的优先级需要一些实验和大量的示例。

在新的中缀运算符后面是一个双箭头 =>，指定中缀运算符使用的命名函数。Lean 的标准库使用此功能将 + 和 * 定义为指向 HAdd.hAdd 和 HMul.hMul 的中缀运算符，从而允许将类型类用于重载中缀运算符。不过这里的 andThen 只是一个普通函数。

通过为 andThen 定义一个中缀运算符，firstThird 可以被改写成一种，显化 none 检查的“管道”风格的方式：

def firstThirdInfix (xs : List α) : Option (α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  some (first, third)

这种风格在编写较长的函数时更加精炼：

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  xs[4]? ~~> fun fifth =>
  xs[6]? ~~> fun seventh =>
  some (first, third, fifth, seventh)

错误消息的传递

像 Lean 这样的纯函数式语言并没有用于错误处理的内置异常机制，因为抛出或捕获异常超出了表达式逐步求值模型考虑的范围。然而函数式程序肯定需要处理错误。在 firstThirdFifthSeventh 的情况下，用户很可能需要知道列表有多长以及查找失败发生的位置。

这通常通过定义一个可以表示错误或结果的数据类型，并让带有异常的函数返回此类型来实现：

-- 和类型，两个构造子，error 存储 ε 类型的报错信息，ok 存储 α 数据类型
inductive Except (ε : Type) (α : Type) where
  | error : ε → Except ε α
  | ok : α → Except ε α
deriving BEq, Hashable, Repr

类型变量 ε 表示函数可能产生的错误类型。调用者需要处理错误和成功两种情况，因此类型变量 ε 的作用有点类似 Java 中需要检查的异常列表。

类似于 Option，Except 可用于指示在列表中找不到项的情况。此时，错误类型为 String：

def get (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

查找未越界的值会返回 Except.ok：

def ediblePlants : List String :=
  ["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]

#eval get ediblePlants 2

Except.ok "sea buckthorn"

查找越界的值会返回 Except.error：

#eval get ediblePlants 4

Except.error "Index 4 not found (maximum is 3)"

单个列表查找可以方便地返回值或错误：

def first (xs : List α) : Except String α :=
  get xs 0

连续进行两次列表查找需要处理可能发生的失败情况：

def firstThird (xs : List α) : Except String (α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  -- 拿到正确的 first 后，继续查找 third
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      Except.ok (first, third)

向函数中添加另一个列表查找操作需要处理更多的错误：

def firstThirdFifth (xs : List α) : Except String (α × α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      match get xs 4 with
      | Except.error msg => Except.error msg
      | Except.ok fifth =>
        Except.ok (first, third, fifth)

再添加一个列表查找操作则开始变得相当难以管理：

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      match get xs 4 with
      | Except.error msg => Except.error msg
      | Except.ok fifth =>
        match get xs 6 with
        | Except.error msg => Except.error msg
        | Except.ok seventh =>
          Except.ok (first, third, fifth, seventh)

同样，可以将通用模式提取为一个辅助函数。函数中的每一步都会检查错误，只有在成功的情况下才进行后续计算。可以为 Except 定义新版本的 andThen：

def andThen (attempt : Except e α) (next : α → Except e β) : Except e β :=
  match attempt with
  | Except.error msg => Except.error msg
  | Except.ok x => next x

与 Option 一样，这个版本的 andThen 允许更简洁地定义 firstThird：

def firstThird' (xs : List α) : Except String (α × α) :=
  andThen (get xs 0) fun first  =>
  andThen (get xs 2) fun third =>
  Except.ok (first, third)

在 Option 和 Except 的情况下，都有两个重复的模式：每一步都有对中间结果的检查，已提取为 andThen；还有最终的成功结果，分别是 some 或 Except.ok。为了方便起见，可以将成功的情况提取为辅助函数 ok：

-- 将 x 记录到 ok 中
def ok (x : α) : Except ε α := Except.ok x

类似地，可以将失败的情况提取为辅助函数 fail：

-- 将 err 记录到 error 中
def fail (err : ε) : Except ε α := Except.error err

使用 ok 和 fail 使得 get 的可读性更好：

def get (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => fail s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => ok x

在为 andThen 添加中缀运算符后，firstThird 可以和返回 Option 的版本一样简洁：

infixl:55 " ~~> " => andThen

def firstThird (xs : List α) : Except String (α × α) :=
  get xs 0 ~~> fun first =>
  get xs 2 ~~> fun third =>
  ok (first, third)

这种技术同样适用于更复杂的函数：

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
  get xs 0 ~~> fun first =>
  get xs 2 ~~> fun third =>
  get xs 4 ~~> fun fifth =>
  get xs 6 ~~> fun seventh =>
  ok (first, third, fifth, seventh)

Q：同样模式反复出现后，怎么归纳统一？

日志记录

当一个数字除以 2 时没有余数则称它为偶数：

def isEven (i : Int) : Bool :=
  i % 2 == 0

函数 sumAndFindEvens 计算列表所有元素的和，同时记录沿途遇到的偶数：

def sumAndFindEvens : List Int → List Int × Int
  | [] => ([], 0)
  | i :: is =>
    let (moreEven, sum) := sumAndFindEvens is
    (if isEven i then i :: moreEven else moreEven, sum + i)

此函数是一个常见模式的简化示例。许多程序需要遍历一次数据结构，在计算一个主要结果的同时累积某种额外的结果。一个例子是日志记录：一个类型为 IO 的程序会将日志输出到磁盘上的文件中，但是由于磁盘在 Lean 函数的数学世界之外，因此对基于 IO 的日志相关的证明变得十分困难。另一个例子是同时计算树的中序遍历和所有节点的和的函数，它必须记录每个访问的节点：

def inorderSum : BinTree Int → List Int × Int
  | BinTree.leaf => ([], 0)
  | BinTree.branch l x r =>
    let (leftVisited, leftSum) := inorderSum l
    let (hereVisited, hereSum) := ([x], x)
    let (rightVisited, rightSum) := inorderSum r
    (leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)

sumAndFindEvens 和 inorderSum 都具有共同的重复结构。计算的每一步都返回一个对（pair），由数据列表和主要结果组成。在下一步中列表会被附加新的元素，计算新的主要结果并与附加的列表再次配对。通过对 sumAndFindEvens 稍微改写，二者共同的结构变得更加明显：

def sumAndFindEvens : List Int → List Int × Int
  | [] => ([], 0)
  | i :: is =>
    let (moreEven, sum) := sumAndFindEvens is
    let (evenHere, ()) := (if isEven i then [i] else [], ())
    (evenHere ++ moreEven, sum + i)

为了清晰起见，可以给由累积结果和值组成的对（pair）起一个专有的名字：

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

同样，保存累积结果列表的同时传递一个值到下一步计算的过程，可以提取为一个辅助函数，再次命名为 andThen：

def andThen (result : WithLog α β) (next : β → WithLog α γ) : WithLog α γ :=
  let {log := thisOut, val := thisRes} := result
  let {log := nextOut, val := nextRes} := next thisRes
  {log := thisOut ++ nextOut, val := nextRes} 

在 Except 的语境下，ok 表示一个总是成功的操作。然而在这里，它仅简单地返回一个值而不产生任何日志：

def ok (x : β) : WithLog α β := {log := [], val := x}

正如 Except 提供 fail 作为一种可能性，WithLog 应该允许将项添加到日志中。它不需要返回任何有意义的结果，所以返回类型为 Unit：

def save (data : α) : WithLog α Unit :=
  {log := [data], val := ()}

WithLog、andThen、ok 和 save 可以将两个程序中的日志记录与求和关注点分开：

-- 计算列表元素的和，同时记录遇到的偶数
def sumAndFindEvens : List Int → WithLog Int Int
  | [] => ok 0  -- 空列表：返回和为0，无日志
  | i :: is =>
    -- 第一步：如果当前元素是偶数，则记录它；否则不记录任何内容
    andThen (if isEven i then save i else ok ()) fun () =>
    -- 第二步：递归处理剩余列表，获取它们的和
    andThen (sumAndFindEvens is) fun sum =>
    -- 第三步：返回当前元素与剩余元素和的总和
    ok (i + sum)

-- 计算二叉树所有节点的和，同时记录中序遍历的节点序列
def inorderSum : BinTree Int → WithLog Int Int
  | BinTree.leaf => ok 0  -- 叶子节点：返回和为0，无日志
  | BinTree.branch l x r =>
    -- 第一步：递归计算左子树的和
    andThen (inorderSum l) fun leftSum =>
    -- 第二步：记录当前节点的值（中序遍历的核心）
    andThen (save x) fun () =>
    -- 第三步：递归计算右子树的和
    andThen (inorderSum r) fun rightSum =>
    -- 第四步：返回左子树、当前节点和右子树的总和
    ok (leftSum + x + rightSum)

关键设计模式：

• andThen 函数将计算步骤串联起来，自动处理日志的合并
• ok 函数用于返回纯值，不产生任何日志
• save 函数用于向日志中添加数据，返回 Unit 类型

同样地，中缀运算符有助于专注于正确的步骤：

infixl:55 " ~~> " => andThen

def sumAndFindEvens : List Int → WithLog Int Int
  | [] => ok 0
  | i :: is =>
    (if isEven i then save i else ok ()) ~~> fun () =>
    sumAndFindEvens is ~~> fun sum =>
    ok (i + sum)

def inorderSum : BinTree Int → WithLog Int Int
  | BinTree.leaf => ok 0
  | BinTree.branch l x r =>
    inorderSum l ~~> fun leftSum =>
    save x ~~> fun () =>
    inorderSum r ~~> fun rightSum =>
    ok (leftSum + x + rightSum)

对树节点编号

树的每个节点的中序编号指的是在中序遍历中被访问的次序。例如，考虑如下的 aTree：

open BinTree in
def aTree :=
  branch
    (branch
       (branch leaf "a" (branch leaf "b" leaf))
       "c"
       leaf)
    "d"
    (branch leaf "e" leaf)

它的中序编号结果为：

BinTree.branch
  (BinTree.branch
    (BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
    (2, "c")
    (BinTree.leaf))
  (3, "d")
  (BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))

虽然树用递归函数来处理最为自然，但树的常见递归模式并不适合计算中序编号。这是因为左子树中分配的最大编号将决定当前节点的编号，进而决定右子树编号的起点。在命令式语言中，可以使用一个保存下一个待分配编号的可变变量来解决此问题。以下 Python 程序使用可变变量计算中序编号：

class Branch:
    def __init__(self, value, left=None, right=None):
        self.left = left
        self.value = value
        self.right = right
    def __repr__(self):
        return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'

def number(tree):
    num = 0
    def helper(t):
        nonlocal num
        if t is None:
            return None
        else:
            new_left = helper(t.left)
            new_value = (num, t.value)
            num += 1
            new_right = helper(t.right)
            return Branch(left=new_left, value=new_value, right=new_right)

    return helper(tree)

aTree 在 Python 中的等价定义是：

a_tree = Branch("d",
                left=Branch("c",
                            left=Branch("a", left=None, right=Branch("b")),
                            right=None),
                right=Branch("e"))

它的编号结果是：

>>> number(a_tree)
Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))

尽管 Lean 没有可变变量，但存在一种解决方法。从外部观察者的角度来看，可变变量可以认为具有两个相关方面：函数调用时的值和函数返回时的值。换句话说，使用可变变量的函数可以看作是：将变量的起始值作为参数，返回变量的最终值和计算结果构成的元组的函数。然后可以将此最终值作为参数传递给下一步计算。

正如 Python 示例中使用定义可变变量的外部函数和更改变量的内部辅助函数一样，Lean 版本使用：提供变量初值并明确返回结果的外部函数，以及在计算编号树的同时传递变量值的内部辅助函数：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α))
    | BinTree.leaf => (n, BinTree.leaf)
    | BinTree.branch left x right =>
      let (k, numberedLeft) := helper n left
      let (i, numberedRight) := helper (k + 1) right
      (i, BinTree.branch numberedLeft (k, x) numberedRight)
  (helper 0 t).snd

此代码与传递 none 的 Option 代码、传递 error 的 Except 代码以及累积日志的 WithLog 代码一样，混合了两个关注点：传递计数器的值和实际遍历树以查找结果。与那些情况一样，可以定义一个 andThen 辅助函数，在计算的各个步骤之间传递状态。第一步是为以下模式命名：将输入状态作为参数并返回输出状态和值的模式：

def State (σ : Type) (α : Type) : Type :=
  σ → (σ × α)

在 State 的情况下，ok 函数保持输入状态不变，并返回提供的值：

def ok (x : α) : State σ α :=
  fun s => (s, x)

在使用可变变量时，有两个基本操作：读取值和用新值替换它。读取当前值是通过一个函数实现的，该函数将输入状态原样放入输出状态，同时将其作为返回值：

def get : State σ σ :=
  fun s => (s, s)

写入新值是指忽略输入状态，并将提供的新值放入输出状态：

def set (s : σ) : State σ Unit :=
  fun _ => (s, ())

最后，可以通过将第一个函数的输出状态和返回值传递给下一个函数来实现两个使用状态的计算的顺序执行：

def andThen (first : State σ α) (next : α → State σ β) : State σ β :=
  fun s =>
    let (s', x) := first s
    next x s'

infixl:55 " ~~> " => andThen

使用 State 和它的辅助函数，可以模拟局部可变状态：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => ok BinTree.leaf
    | BinTree.branch left x right =>
      helper left ~~> fun numberedLeft =>
      get ~~> fun n =>
      set (n + 1) ~~> fun () =>
      helper right ~~> fun numberedRight =>
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

由于 State 只模拟单个局部变量，因此 get 和 set 不需要引用任何特定的变量名。

单子：一种函数式设计模式

以上每个示例都包含以下结构：

• 一个多态类型，例如 Option、Except ε、WithLog logged 或 State σ
• 一个运算符 andThen，用于处理具有此类型的程序的顺序组合和重复模式
• 一个运算符 ok，它（在某种意义上）是使用该类型最基本的方式
• 一系列其他操作，例如 none、fail、save 和 get，它们提供了使用相应类型的具体方式

这种风格的 API 称为单子（Monad）。虽然单子的思想源自数学分支范畴论，但在编程中使用它们并不需要理解范畴论。单子的核心思想是：每个单子都使用纯函数式语言 Lean 提供的工具来编码特定类型的副作用。例如，Option 表示可能通过返回 none 而失败的程序，Except 表示可能抛出异常的程序，WithLog 表示在运行时累积日志的程序，State 表示具有单个可变变量的程序。

Monad 类型类

无需为每个单子都实现 ok 或 andThen 这样的运算符，Lean 标准库包含一个类型类，允许它们被重载，以便相同的运算符可用于 任何 单子。单子有两个操作，分别相当于 ok 和 andThen：

class Monad (m : Type → Type) where
  pure : α → m α
  bind : m α → (α → m β) → m β

这个定义略有简化。Lean 标准库中的实际定义更复杂一些，稍后会介绍。

Option 和 Except 的 Monad 实例可以通过调整它们各自的 andThen 操作的定义来创建：

instance : Monad Option where
  pure x := some x
  bind opt next :=
    match opt with
    | none => none
    | some x => next x

instance : Monad (Except ε) where
  pure x := Except.ok x
  bind attempt next :=
    match attempt with
    | Except.error e => Except.error e
    | Except.ok x => next x

例如 firstThirdFifthSeventh 原本对 Option α 和 Except String α 类型分别定义。现在，它可以被定义为对 任何 单子都有效的多态函数。但是，它需要接受一个参数作为查找函数，因为不同的单子可能以不同的方式找不到结果。bind 的中缀运算符是 >>=，它扮演与示例中 ~~> 相同的角色。

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

给定作为示例的 slowMammals 和 fastBirds 列表，该 firstThirdFifthSeventh 实现可与 Option 一起使用：

def slowMammals : List String :=
  ["Three-toed sloth", "Slow loris"]

def fastBirds : List String := [
  "Peregrine falcon",
  "Saker falcon",
  "Golden eagle",
  "Gray-headed albatross",
  "Spur-winged goose",
  "Swift",
  "Anna's hummingbird"
]

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) slowMammals

none

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds

some ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

在将 Except 的查找函数 get 重命名为更具体的形式后，完全相同的 firstThirdFifthSeventh 实现也可以与 Except 一起使用：

def getOrExcept (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

#eval firstThirdFifthSeventh getOrExcept slowMammals

Except.error "Index 2 not found (maximum is 1)"

#eval firstThirdFifthSeventh getOrExcept fastBirds

Except.ok ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

m 必须有 Monad 实例，这一事实意味着可以使用 >>= 和 pure 运算符。

通用的单子运算符

由于许多不同类型都是单子，因此对 任何 单子多态的函数非常强大。例如，函数 mapM 是 map 的另一个版本，它使用 Monad 将函数调用的结果按顺序连接起来：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)

函数参数 f 的返回类型决定了将使用哪个 Monad 实例。换句话说，mapM 可用于生成日志的函数、可能失败的函数、或使用可变状态的函数。由于 f 的类型直接决定了可用的效应 (Effects)，因此 API 设计人员可以对其进行严格控制。译者注：效应 (Effects) 是函数式编程中与 Monad 密切相关的主题，实际上对效应的控制比此处原文所述更复杂一些，但超出了本文的内容。另外副作用 (Side Effects) 也是一种效应。

As described in this chapter’s introduction, State σ α represents programs that make use of a mutable variable of type σ and return a value of type α. These programs are actually functions from a starting state to a pair of a value and a final state. The Monad class requires that its parameter expect a single type argument—that is, it should be a Type → Type. This means that the instance for State should mention the state type σ, which becomes a parameter to the instance:

如本章简介所介绍的，State σ α 表示使用类型为 σ 的可变变量，并返回类型为 α 的值的程序。这些程序实际上是从起始状态到值和最终状态构成的对 (pair) 的函数。Monad 类型类要求：类型参数期望另一个类型参数，即它应该是 Type → Type。这意味着 State 的实例应提及状态类型 σ，使它成为实例的参数：

instance : Monad (State σ) where
  pure x := fun s => (s, x)
  bind first next :=
    fun s =>
      let (s', x) := first s
      next x s'

这意味着在使用 bind 对 get 和 set 排序时，状态的类型不能更改，这是具有状态的计算的合理规则。运算符 increment 将保存的状态增加一定量，并返回原值：

def increment (howMuch : Int) : State Int Int :=
  get >>= fun i =>
  set (i + howMuch) >>= fun () =>
  pure i

将 mapM 和 increment 一起使用会得到一个计算列表元素累加和的程序。更具体地说，可变变量包含到目前为止的和，而作为结果的列表包含各个步骤前状态变量的值。换句话说，mapM increment 的类型为 List Int → State Int (List Int)，展开 State 的定义得到 List Int → Int → (Int × List Int)。它将初始值作为参数，应为 0：

#eval mapM increment [1, 2, 3, 4, 5] 0

(15, [0, 1, 3, 6, 10])

A logging effect can be represented using WithLog. Just like State, its Monad instance is polymorphic with respect to the type of the logged data:

可以使用 WithLog 表示日志记录效应。就和 State 一样，它的 Monad 实例对于被记录数据的类型也是多态的：

instance : Monad (WithLog logged) where
  pure x := {log := [], val := x}
  bind result next :=
    let {log := thisOut, val := thisRes} := result
    let {log := nextOut, val := nextRes} := next thisRes
    {log := thisOut ++ nextOut, val := nextRes}

saveIfEven is a function that logs even numbers but returns its argument unchanged:

saveIfEven函数记录偶数，但将参数原封不动返回：

def saveIfEven (i : Int) : WithLog Int Int :=
  (if isEven i then
    save i
   else pure ()) >>= fun () =>
  pure i

Using this function with mapM results in a log containing even numbers paired with an unchanged input list:

将 mapM 和该函数一起使用，会生成一个记录偶数的日志、和未更改的输入列表：

#eval mapM saveIfEven [1, 2, 3, 4, 5]



{ log := [2, 4], val := [1, 2, 3, 4, 5] }

The Identity Monad

恒等单子

Monads encode programs with effects, such as failure, exceptions, or logging, into explicit representations as data and functions. Sometimes, however, an API will be written to use a monad for flexibility, but the API’s client may not require any encoded effects. The identity monad is a monad that has no effects, and allows pure code to be used with monadic APIs:

单子将具有效应(Effects)的程序（例如失败、异常或日志记录）编码为数据和函数的显式表示。 有时API会使用单子来提高灵活性，但API的使用方可能不需要任何效应。 恒等单子 (Identity Monad)是一个没有任何效应的单子，允许将纯(pure)代码与monadic API一起使用：

def Id (t : Type) : Type := t

instance : Monad Id where
  pure x := x
  bind x f := f x

The type of pure should be α → Id α, but Id α reduces to just α. Similarly, the type of bind should be α → (α → Id β) → Id β. Because this reduces to α → (α → β) → β, the second argument can be applied to the first to find the result.

pure的类型应为 α → Id α，但Id α 归约 为 α。类似地，bind 的类型应为α → (α → Id β) → Id β。 由于这 归约 为 α → (α → β) → β，因此可以将第二个参数应用于第一个参数得到结果。 译者注：此处归约 一词原文为reduces to，实际含义为beta-reduction，请见类型论相关资料。

With the identity monad, mapM becomes equivalent to map. To call it this way, however, Lean requires a hint that the intended monad is Id:

"使用恒等单子时，mapM等同于map。但是要以这种方式调用它，Lean需要额外的提示来表明目标单子是Id：

#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5]



[2, 3, 4, 5, 6]

Omitting the hint results in an error:

省略提示则会导致错误：

#eval mapM (· + 1) [1, 2, 3, 4, 5]

failed to synthesize instance
  HAdd Nat Nat (?m.9063 ?m.9065)

In this error, the application of one metavariable to another indicates that Lean doesn’t run the type-level computation backwards. The return type of the function is expected to be the monad applied to some other type. Similarly, using mapM with a function whose type doesn’t provide any specific hints about which monad is to be used results in an “instance problem stuck” message:

导致错误的原因是：一个元变量应用于另一个元变量，使得Lean不会反向运行类型计算。 函数的返回类型应该是应用于其他类型参数的单子。 类似地，将 mapM 和未提供任何特定单子类型信息的函数一起使用，会导致"instance problem stuck"错误：

#eval mapM (fun x => x) [1, 2, 3, 4, 5]



typeclass instance problem is stuck, it is often due to metavariables
  Monad ?m.9063

The Monad Contract

单子约定

Just as every pair of instances of BEq and Hashable should ensure that any two equal values have the same hash, there is a contract that each instance of Monad should obey. First, pure should be a left identity of bind. That is, bind (pure v) f should be the same as f v. Secondly, pure should be a right identity of bind, so bind v pure is the same as v. Finally, bind should be associative, so bind (bind v f) g is the same as bind v (fun x => bind (f x) g).

正如 BEq 和 Hashable 的每一对实例都应该确保任何两个相等的值具有相同的哈希值，有一些是固有的约定是每个 Monad 的实例都应遵守的。 首先，pure应为 bind 的左单位元，即 bind (pure v) f 应与 f v 等价。 其次，pure应为 bind 的右单位元，即 bind v pure 应与 v 等价。 最后，bind应满足结合律，即 bind (bind v f) g 应与 bind v (fun x => bind (f x) g) 等价。

This contract specifies the expected properties of programs with effects more generally. Because pure has no effects, sequencing its effects with bind shouldn’t change the result. The associative property of bind basically says that the sequencing bookkeeping itself doesn’t matter, so long as the order in which things are happening is preserved.

这些约定保证了具有效应的程序的预期属性。 由于 pure 不导致效应，因此用 bind 将其与其他效应接连执行不应改变结果。 bind满足的结合律则意味着先计算哪一部分无关紧要，只要保证效应的顺序不变即可。

Exercises

练习

Mapping on a Tree

映射一棵树

Define a function BinTree.mapM. By analogy to mapM for lists, this function should apply a monadic function to each data entry in a tree, as a preorder traversal. The type signature should be:

定义函数BinTree.mapM。 通过类比列表的mapM，此函数应将单子函数应用于树中的每个节点，作为前序遍历。 类型签名应为：

def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β)

The Option Monad Contract

Option单子的约定

First, write a convincing argument that the Monad instance for Option satisfies the monad contract. Then, consider the following instance:

首先充分论证 Option 的 Monad 实例满足单子约定。 然后，考虑以下实例：

instance : Monad Option where
  pure x := some x
  bind opt next := none

Both methods have the correct type. Why does this instance violate the monad contract?

这两个方法都有正确的类型。 但这个实例却违反了单子约定，为什么？

Example: Arithmetic in Monads

例子：利用单子实现算术表达式求值

Monads are a way of encoding programs with side effects into a language that does not have them. It would be easy to read this as a sort of admission that pure functional programs are missing something important, requiring programmers to jump through hoops just to write a normal program. However, while using the Monad API does impose a syntactic cost on a program, it brings two important benefits: 1. Programs must be honest about which effects they use in their types. A quick glance at a type signature describes everything that the program can do, rather than just what it accepts and what it returns. 2. Not every language provides the same effects. For example, only some language have exceptions. Other languages have unique, exotic effects, such as Icon’s searching over multiple values and Scheme or Ruby’s continuations. Because monads can encode any effect, programmers can choose which ones are the best fit for a given application, rather than being stuck with what the language developers provided.

单子是一种将具有副作用的程序编入没有副作用的语言中的范式。 但很容易将此误解为：承认纯函数式编程缺少一些重要的东西，程序员要越过这些障碍才能编写一个普通的程序。 虽然使用 Monad 确实给程序带来了语法上的成本，但它带来了两个重要的优点：

1. 程序必须在类型中诚实地告知它们使用的作用（Effects）。因此看一眼类型签名就可以知道程序能做的所有事情，而不只是知道它接受什么和返回什么。
2. 并非每种语言都提供相同的作用。例如只有某些语言有异常。其他语言具有独特的新奇作用，例如 Icon’s searching over multiple values以及Scheme 或Ruby的continuations。由于单子可以编码 任何 作用，因此程序员可以选择最适合给定程序的作用，而不是局限于语言开发者提供的作用。

One example of a program that can make sense in a variety of monads is an evaluator for arithmetic expressions.

对许多单子都有意义的一个例子是算术表达式的求值器。

Arithmetic Expressions

算术表达式

An arithmetic expression is either a literal integer or a primitive binary operator applied to two expressions. The operators are addition, subtraction, multiplication, and division:

一条算术表达式要么是一个字面量(Literal)，要么是应用于两个算术表达式的二元运算。运算符包括加法、减法、乘法和除法：

inductive Expr (op : Type) where
  | const : Int → Expr op
  | prim : op → Expr op → Expr op → Expr op


inductive Arith where
  | plus
  | minus
  | times
  | div

The expression 2 + 3 is represented:

表达式 2 + 3 表示为：

open Expr in
open Arith in
def twoPlusThree : Expr Arith :=
  prim plus (const 2) (const 3)

and 14 / (45 - 5 * 9) is represented:

而 14 / (45 - 5 * 9) 表示为：

open Expr in
open Arith in
def fourteenDivided : Expr Arith :=
  prim div (const 14) (prim minus (const 45) (prim times (const 5) (const 9)))

Evaluating Expressions

对表达式求值

Because expressions include division, and division by zero is undefined, evaluation might fail. One way to represent failure is to use Option:

由于表达式包含除法，而除以零是未定义的，因此求值可能会失败。 表示失败的一种方法是使用 Option：

def evaluateOption : Expr Arith → Option Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateOption e1 >>= fun v1 =>
    evaluateOption e2 >>= fun v2 =>
    match p with
    | Arith.plus => pure (v1 + v2)
    | Arith.minus => pure (v1 - v2)
    | Arith.times => pure (v1 * v2)
    | Arith.div => if v2 == 0 then none else pure (v1 / v2)

This definition uses the Monad Option instance to propagate failures from evaluating both branches of a binary operator. However, the function mixes two concerns: evaluating subexpressions and applying a binary operator to the results. It can be improved by splitting it into two functions:

此定义使用 Monad Option 实例，来传播从二元运算符的两个分支求值产生的失败。 然而该函数混合了两个问题：对子表达式的求值和对运算符的计算。 可以将其拆分为两个函数：

def applyPrim : Arith → Int → Int → Option Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y => if y == 0 then none else pure (x / y)

def evaluateOption : Expr Arith → Option Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateOption e1 >>= fun v1 =>
    evaluateOption e2 >>= fun v2 =>
    applyPrim p v1 v2

Running #eval evaluateOption fourteenDivided yields none, as expected, but this is not a very useful error message. Because the code was written using >>= rather than by explicitly handling the none constructor, only a small modification is required for it to provide an error message on failure:

运行 #eval evaluateOption fourteenDivided 产生 none, 与预期一样, 但这个报错信息却并不十分有用. 由于代码使用 >>= 而非显式处理none，所以只需少量修改即可在失败时提供错误消息：

def applyPrim : Arith → Int → Int → Except String Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)


def evaluateExcept : Expr Arith → Except String Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateExcept e1 >>= fun v1 =>
    evaluateExcept e2 >>= fun v2 =>
    applyPrim p v1 v2

The only difference is that the type signature mentions Except String instead of Option, and the failing case uses Except.error instead of none. By making evaluate polymorphic over its monad and passing it applyPrim as an argument, a single evaluator becomes capable of both forms of error reporting:

唯一区别是：类型签名提到的是 Except String 而非 Option，并且失败时使用 Except.error 而不是 none。通过让 evaluate 对单子多态，并将对应的求值函数作为参数 applyPrim 传递，单个求值器就足够以两种形式报告错误：

def applyPrimOption : Arith → Int → Int → Option Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then
      none
    else pure (x / y)

def applyPrimExcept : Arith → Int → Int → Except String Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def evaluateM [Monad m] (applyPrim : Arith → Int → Int → m Int): Expr Arith → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applyPrim e1 >>= fun v1 =>
    evaluateM applyPrim e2 >>= fun v2 =>
    applyPrim p v1 v2

Using it with applyPrimOption works just like the first version of evaluate:

将其与 applyPrimOption 一起使用作用就和最初的 evaluate 一样：

#eval evaluateM applyPrimOption fourteenDivided



none

Similarly, using it with applyPrimExcept works just like the version with error messages:

类似地，和 applyPrimExcept 函数一起使用时作用与带有错误消息的版本相同：

#eval evaluateM applyPrimExcept fourteenDivided



Except.error "Tried to divide 14 by zero"

The code can still be improved. The functions applyPrimOption and applyPrimExcept differ only in their treatment of division, which can be extracted into another parameter to the evaluator:

代码仍有改进空间。 applyPrimOption和 applyPrimExcept 函数仅在除法处理上有所不同，因此可以将它提取到另一个参数中：

def applyDivOption (x : Int) (y : Int) : Option Int :=
    if y == 0 then
      none
    else pure (x / y)

def applyDivExcept (x : Int) (y : Int) : Except String Int :=
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def applyPrim [Monad m] (applyDiv : Int → Int → m Int) : Arith → Int → Int → m Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y => applyDiv x y

def evaluateM [Monad m] (applyDiv : Int → Int → m Int): Expr Arith → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applyDiv e1 >>= fun v1 =>
    evaluateM applyDiv e2 >>= fun v2 =>
    applyPrim applyDiv p v1 v2

In this refactored code, the fact that the two code paths differ only in their treatment of failure has been made fully apparent.

在重构后的代码中，两条路径仅在对失败情况的处理上有所不同，这一事实显而易见。

Further Effects

额外的作用

Failure and exceptions are not the only kinds of effects that can be interesting when working with an evaluator. While division’s only side effect is failure, adding other primitive operators to the expressions make it possible to express other effects.

在考虑求值器时，失败和异常并不是唯一值得在意的作用。虽然除法的唯一副作用是失败，但若要增加其他运算符的支持，则可能需要表达对应的作用。

The first step is an additional refactoring, extracting division from the datatype of primitives:

第一步是重构，从原始数据类型中提取除法：

inductive Prim (special : Type) where
  | plus
  | minus
  | times
  | other : special → Prim special

inductive CanFail where
  | div

The name CanFail suggests that the effect introduced by division is potential failure.

名称 CanFail 表明被除法引入的作用是可能发生的失败。

The second step is to broaden the scope of the division handler argument to evaluateM so that it can process any special operator:

第二步是将 evaluateM 的作为除法计算的参数扩展，以便它可以处理任何特殊运算符：

def divOption : CanFail → Int → Int → Option Int
  | CanFail.div, x, y => if y == 0 then none else pure (x / y)

def divExcept : CanFail → Int → Int → Except String Int
  | CanFail.div, x, y =>
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def applyPrim [Monad m] (applySpecial : special → Int → Int → m Int) : Prim special → Int → Int → m Int
  | Prim.plus, x, y => pure (x + y)
  | Prim.minus, x, y => pure (x - y)
  | Prim.times, x, y => pure (x * y)
  | Prim.other op, x, y => applySpecial op x y

def evaluateM [Monad m] (applySpecial : special → Int → Int → m Int): Expr (Prim special) → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applySpecial e1 >>= fun v1 =>
    evaluateM applySpecial e2 >>= fun v2 =>
    applyPrim applySpecial p v1 v2

No Effects

无作用

The type Empty has no constructors, and thus no values, like the Nothing type in Scala or Kotlin. In Scala and Kotlin, Nothing can represent computations that never return a result, such as functions that crash the program, throw exceptions, or always fall into infinite loops. An argument to a function or method of type Nothing indicates dead code, as there will never be a suitable argument value. Lean doesn’t support infinite loops and exceptions, but Empty is still useful as an indication to the type system that a function cannot be called. Using the syntax nomatch E when E is an expression whose type has no constructors indicates to Lean that the current expression need not return a result, because it could never have been called.

Empty类型没有构造子，因此没有任何取值，就像Scala或Kotlin中的 Nothing 类型。 在Scala和Kotlin中，返回类型为 Nothing 表示永不返回结果的计算，例如导致程序崩溃、或引发异常、或陷入无限循环的函数。 参数类型为 Nothing 表示函数是死代码，因为我们永远无法构造出合适的参数值来调用它。 Lean 不支持无限循环和异常，但 Empty 仍然可作为向类型系统说明函数不可被调用的标志。 当 E 是一条表达式，但它的类型没有任何取值时，使用 nomatch E 向Lean说明当前表达式不返回结果，因为它永远不会被调用。

Using Empty as the parameter to Prim indicates that there are no additional cases beyond Prim.plus, Prim.minus, and Prim.times, because it is impossible to come up with a value of type Empty to place in the Prim.other constructor. Because a function to apply an operator of type Empty to two integers can never be called, it doesn’t need to return a result. Thus, it can be used in any monad:

将 Empty 用作 Prim 的参数，表示除了 Prim.plus、Prim.minus 和 Prim.times 之外没有其他情况，因为不可能找到一个 Empty 类型的值来放在 Prim.other 构造子中。 由于类型为 Empty 的运算符应用于两个整数的函数永远不会被调用，所以它不需要返回结果。 因此，它可以在 任何 单子中使用：

def applyEmpty [Monad m] (op : Empty) (_ : Int) (_ : Int) : m Int :=
  nomatch op

This can be used together with Id, the identity monad, to evaluate expressions that have no effects whatsoever:

这可以与恒等单子 Id 一起使用，用来计算没有任何副作用的表达式：

open Expr Prim in
#eval evaluateM (m := Id) applyEmpty (prim plus (const 5) (const (-14)))



-9

Nondeterministic Search

非确定性搜索

Instead of simply failing when encountering division by zero, it would also be sensible to backtrack and try a different input. Given the right monad, the very same evaluateM can perform a nondeterministic search for a set of answers that do not result in failure. This requires, in addition to division, some means of specifying a choice of results. One way to do this is to add a function choose to the language of expressions that instructs the evaluator to pick either of its arguments while searching for non-failing results.

遇到除以零时，除了直接失败并结束之外，还可以回溯并尝试不同的输入。 给定适当的单子，同一个 evaluateM 可以对不致失败的答案 集合 执行非确定性搜索。 这要求除了除法之外，还需要指定选择结果的方式。 一种方法是在表达式的语言中添加一个函数choose，告诉求值器在搜索非失败结果时选择其中一个参数。

The result of the evaluator is now a multiset of values, rather than a single value. The rules for evaluation into a multiset are: * Constants \( n \) evaluate to singleton sets \( \{n\} \). * Arithmetic operators other than division are called on each pair from the Cartesian product of the operators, so \( X + Y \) evaluates to \( \\{ x + y \\mid x ∈ X, y ∈ Y \\} \). * Division \( X / Y \) evaluates to \( \\{ x / y \\mid x ∈ X, y ∈ Y, y ≠ 0\\} \). In other words, all \( 0 \) values in \( Y \) are thrown out. * A choice \( \\mathrm{choose}(x, y) \) evaluates to \( \\{ x, y \\} \).

求值结果现在变成一个多重集合(multiset)，而不是一个单一值 求值到多重集合的规则如下：

• 常量 ( n ) 求值为单元素集合 ( {n} )。
• 除法以外的算术运算符作用于两个参数的笛卡尔积中的每一对，所以 ( X + Y ) 求值为 ( \{ x + y \mid x ∈ X, y ∈ Y \} )。
• 除法 ( X / Y ) 求值为 ( \{ x / y \mid x ∈ X, y ∈ Y, y ≠ 0\} ). 换句话说，所有 ( Y ) 中的 ( 0 ) 都被丢弃。
• 选择 ( \mathrm{choose}(x, y) ) 求值为 ( \{ x, y \} )。

For example, \( 1 + \\mathrm{choose}(2, 5) \) evaluates to \( \\{ 3, 6 \\} \), \(1 + 2 / 0 \) evaluates to \( \\{\\} \), and \( 90 / (\\mathrm{choose}(-5, 5) + 5) \) evaluates to \( \\{ 9 \\} \). Using multisets instead of true sets simplifies the code by removing the need to check for uniqueness of elements.

例如， ( 1 + \mathrm{choose}(2, 5) ) 求值为 ( \{ 3, 6 \} )， (1 + 2 / 0 ) 求值为 ( \{\} )，并且 ( 90 / (\mathrm{choose}(-5, 5) + 5) ) 求值为 ( \{ 9 \} )。 使用多重集合而非集合，是为了避免处理元素重复的情况而使代码过于复杂。

A monad that represents this non-deterministic effect must be able to represent a situation in which there are no answers, and a situation in which there is at least one answer together with any remaining answers:

表示这种非确定性作用的单子必须能够处理没有答案的情况，以及至少有一个答案和其他答案的情况：

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

This datatype looks very much like List. The difference is that where cons stores the rest of the list, more stores a function that should compute the next value on demand. This means that a consumer of Many can stop the search when some number of results have been found.

该数据类型看起来非常像List。 不同之处在于，cons存储列表的其余部分，而 more 存储一个函数，该函数仅在需要时才会被调用来计算下一个值。 这意味着 Many 的使用者可以在找到一定数量的结果后停止搜索。

A single result is represented by a more constructor that returns no further results:

单个结果由 more 构造子表示，该构造子不返回任何进一步的结果：

def Many.one (x : α) : Many α := Many.more x (fun () => Many.none)

The union of two multisets of results can be computed by checking whether the first multiset is empty. If so, the second multiset is the union. If not, the union consists of the first element of the first multiset followed by the union of the rest of the first multiset with the second multiset:

两个作为结果的多重集合的并集，可以通过检查第一个是否为空来计算。 如果第一个为空则第二个多重集合就是并集。 如果非空，则并集由第一个多重集合的第一个元素，紧跟着其余部分与第二个多重集的并集：

def Many.union : Many α → Many α → Many α
  | Many.none, ys => ys
  | Many.more x xs, ys => Many.more x (fun () => union (xs ()) ys)

It can be convenient to start a search process with a list of values. Many.fromList converts a list into a multiset of results:

对值列表搜索会比手动构造多重集合更方便。 函数 Many.fromList 将列表转换为结果的多重集合：

def Many.fromList : List α → Many α
  | [] => Many.none
  | x :: xs => Many.more x (fun () => fromList xs)

Similarly, once a search has been specified, it can be convenient to extract either a number of values, or all the values:

类似地，一旦搜索已经确定，就可以方便地提取固定数量的值或所有值：

def Many.take : Nat → Many α → List α
  | 0, _ => []
  | _ + 1, Many.none => []
  | n + 1, Many.more x xs => x :: (xs ()).take n

def Many.takeAll : Many α → List α
  | Many.none => []
  | Many.more x xs => x :: (xs ()).takeAll

A Monad Many instance requires a bind operator. In a nondeterministic search, sequencing two operations consists of taking all possibilities from the first step and running the rest of the program on each of them, taking the union of the results. In other words, if the first step returns three possible answers, the second step needs to be tried for all three. Because the second step can return any number of answers for each input, taking their union represents the entire search space.

Monad Many实例需要一个 bind 运算符。 在非确定性搜索中，对两个操作进行排序包括：从第一步中获取所有可能性，并对每种可能性都运行程序的其余部分，取结果的并集。 换句话说，如果第一步返回三个可能的答案，则需要对这三个答案分别尝试第二步。 由于第二步为每个输入都可以返回任意数量的答案，因此取它们的并集表示整个搜索空间。

def Many.bind : Many α → (α → Many β) → Many β
  | Many.none, _ =>
    Many.none
  | Many.more x xs, f =>
    (f x).union (bind (xs ()) f)

Many.one and Many.bind obey the monad contract. To check that Many.bind (Many.one v) f is the same as f v, start by evaluating the expression as far as possible:

Many.one和 Many.bind 遵循单子约定。 要检查 Many.bind (Many.one v) f 是否与 f v 相同，首先应最大限度地计算表达式：

Many.bind (Many.one v) f
===>
Many.bind (Many.more v (fun () => Many.none)) f
===>
(f v).union (Many.bind Many.none f)
===>
(f v).union Many.none

The empty multiset is a right identity of union, so the answer is equivalent to f v. To check that Many.bind v Many.one is the same as v, consider that bind takes the union of applying Many.one to each element of v. In other words, if v has the form {v1, v2, v3, ..., vn}, then Many.bind v Many.one is {v1} ∪ {v2} ∪ {v3} ∪ ... ∪ {vn}, which is {v1, v2, v3, ..., vn}.

空集是 union 的右单位元，因此答案等同于f v。 要检查 Many.bind v Many.one 是否与 v 相同，需要考虑 Many.one 应用于 v 的各元素结果的并集。 换句话说，如果 v 的形式为 {v1, v2, v3, ..., vn}，则Many.bind v Many.one 为{v1} ∪ {v2} ∪ {v3} ∪ ... ∪ {vn}，即{v1, v2, v3, ..., vn}。

Finally, to check that Many.bind is associative, check that Many.bind (Many.bind bind v f) g is the same as Many.bind v (fun x => Many.bind (f x) g). If v has the form {v1, v2, v3, ..., vn}, then:

最后，要检查 Many.bind 是否满足结合律，需要检查 Many.bind (Many.bind bind v f) g 是否与 Many.bind v (fun x => Many.bind (f x) g) 相同。 如果 v 的形式为{v1, v2, v3, ..., vn}，则：

Many.bind v f
===>
f v1 ∪ f v2 ∪ f v3 ∪ ... ∪ f vn

which means that

Many.bind (Many.bind bind v f) g
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g

Similarly,

与此类似，

Many.bind v (fun x => Many.bind (f x) g)
===>
(fun x => Many.bind (f x) g) v1 ∪
(fun x => Many.bind (f x) g) v2 ∪
(fun x => Many.bind (f x) g) v3 ∪
... ∪
(fun x => Many.bind (f x) g) vn
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g

Thus, both sides are equal, so Many.bind is associative.

因此两边相等，所以 Many.bind 满足结合律。

由此得到的单子实例为：

instance : Monad Many where
  pure := Many.one
  bind := Many.bind

An example search using this monad finds all the combinations of numbers in a list that add to 15:

利用此单子，下例可找到列表中所有加起来等于15的数字组合：

def addsTo (goal : Nat) : List Nat → Many (List Nat)
  | [] =>
    if goal == 0 then
      pure []
    else
      Many.none
  | x :: xs =>
    if x > goal then
      addsTo goal xs
    else
      (addsTo goal xs).union
        (addsTo (goal - x) xs >>= fun answer =>
         pure (x :: answer))

The search process is recursive over the list. The empty list is a successful search when the goal is 0; otherwise, it fails. When the list is non-empty, there are two possibilities: either the head of the list is greater than the goal, in which case it cannot participate in any successful searches, or it is not, in which case it can. If the head of the list is not a candidate, then the search proceeds to the tail of the list. If the head is a candidate, then there are two possibilities to be combined with Many.union: either the solutions found contain the head, or they do not. The solutions that do not contain the head are found with a recursive call on the tail, while the solutions that do contain it result from subtracting the head from the goal, and then attaching the head to the solutions that result from the recursive call.

(译者注：这是一个动态规划算法)对列表进行递归搜索。 当输入列表为空且目标为 0 时，返回空列表表示成功；否则返回 Many.none 表示失败，因为空输入不可能得到非0加和。 当列表非空时，有两种可能性：若输入列表的第一个元素大于goal，此时它的任何加和都大于 0 因此不可能是候选者；若第一个元素不大于goal，可以参与后续的搜索。 如果列表的头部x 不是 候选者，对列表的尾部xs递归搜索。 如果头部是候选者，则有两种用 Many.union 合并起来的可能性：找到的解含有当前的x，或者不含有。 不含x的解通过xs递归搜索找到；而含有x的解则通过从goal中减去x，然后将x附加到递归的解中得到。

Returning to the arithmetic evaluator that produces multisets of results, the both and neither operators can be written as follows:

让我们回到产生多重集合的算术求值器，both和 neither 运算符可以写成如下形式：

inductive NeedsSearch
  | div
  | choose

def applySearch : NeedsSearch → Int → Int → Many Int
  | NeedsSearch.choose, x, y =>
    Many.fromList [x, y]
  | NeedsSearch.div, x, y =>
    if y == 0 then
      Many.none
    else Many.one (x / y)

Using these operators, the earlier examples can be evaluated:

可以用这些运算符对前面的示例求值：

open Expr Prim NeedsSearch

#eval (evaluateM applySearch (prim plus (const 1) (prim (other choose) (const 2) (const 5)))).takeAll



[3, 6]



#eval (evaluateM applySearch (prim plus (const 1) (prim (other div) (const 2) (const 0)))).takeAll



[]



#eval (evaluateM applySearch (prim (other div) (const 90) (prim plus (prim (other choose) (const (-5)) (const 5)) (const 5)))).takeAll



[9]

Custom Environments

自定义环境

The evaluator can be made user-extensible by allowing strings to be used as operators, and then providing a mapping from strings to a function that implements them. For example, users could extend the evaluator with a remainder operator or with one that returns the maximum of its two arguments. The mapping from function names to function implementations is called an environment.

可以通过允许将字符串当作运算符，然后提供从字符串到它们的实现函数之间的映射，使求值器可由用户扩展。 例如，用户可以用余数运算或最大值运算来扩展求值器。 从函数名称到函数实现的映射称为 环境 。

The environments needs to be passed in each recursive call. Initially, it might seem that evaluateM needs an extra argument to hold the environment, and that this argument should be passed to each recursive invocation. However, passing an argument like this is another form of monad, so an appropriate Monad instance allows the evaluator to be used unchanged.

环境需要在每层递归调用之间传递。 因此一开始 evaluateM 看起来需要一个额外的参数来保存环境，并且该参数需要在每次递归调用时传递。 然而，像这样传递参数是单子的另一种形式，因此一个适当的 Monad 实例允许求值器本身保持不变。

Using functions as a monad is typically called a reader monad. When evaluating expressions in the reader monad, the following rules are used: * Constants \( n \) evaluate to constant functions \( λ e . n \), * Arithmetic operators evaluate to functions that pass their arguments on, so \( f + g \) evaluates to \( λ e . f(e) + g(e) \), and * Custom operators evaluate to the result of applying the custom operator to the arguments, so \( f \\ \\mathrm{OP}\\ g \) evaluates to \[ λ e . \\begin{cases} h(f(e), g(e)) & \\mathrm{if}\\ e\\ \\mathrm{contains}\\ (\\mathrm{OP}, h) \\\\ 0 & \\mathrm{otherwise} \\end{cases} \] with \( 0 \) serving as a fallback in case an unknown operator is applied.

将函数当作单子，这通常称为 reader 单子。 在reader单子中对表达式求值使用以下规则：

• 常量 ( n ) 映射为常量函数 ( λ e . n )，
• 算术运算符映射为将参数各自传递然后计算的函数，因此 ( f + g ) 映射为 ( λ e . f(e) + g(e) )，并且
• 自定义运算符求值为将自定义运算符应用于参数的结果，因此 ( f \ \mathrm{OP}\ g ) 映射为 [ λ e . \begin{cases} h(f(e), g(e)) & \mathrm{if}\ e\ \mathrm{contains}\ (\mathrm{OP}, h) \\ 0 & \mathrm{otherwise} \end{cases} ] 其中 ( 0 ) 用于运算符未知的情况。

To define the reader monad in Lean, the first step is to define the Reader type and the effect that allows users to get ahold of the environment:

要在Lean中定义reader单子，第一步是定义 Reader 类型，和用户获取环境的作用：

def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

By convention, the Greek letter ρ, which is pronounced “rho”, is used for environments.

按照惯例，希腊字母ρ（发音为“rho”）用于表示环境。

The fact that constants in arithmetic expressions evaluate to constant functions suggests that the appropriate definition of pure for Reader is a a constant function:

算术表达式中的常量映射为常量函数这一事实表明，Reader的 pure 的适当定义是一个常量函数：

def Reader.pure (x : α) : Reader ρ α := fun _ => x

On the other hand, bind is a bit tricker. Its type is Reader ρ α → (α → Reader ρ β) → Reader ρ β. This type can be easier to understand by expanding the definitions of Reader, which yields (ρ → α) → (α → ρ → β) → ρ → β. It should take an environment-accepting function as its first argument, while the second argument should transform the result of the environment-accepting function into yet another environment-accepting function. The result of combining these is itself a function, waiting for an environment.

另一方面 bind 则有点棘手。 它的类型是Reader ρ α → (α → Reader ρ β) → Reader ρ β。 通过展开 Reader 的定义，可以更容易地理解此类型，从而产生(ρ → α) → (α → ρ → β) → ρ → β。 它将读取环境的函数作为第一个参数，而第二个参数将第一个参数的结果转换为另一个读取环境的函数。 组合这些结果本身就是一个读取环境的函数。

It’s possible to use Lean interactively to get help writing this function. The first step is to write down the arguments and return type, being very explicit in order to get as much help as possible, with an underscore for the definition’s body:

可以交互式地使用Lean，获得编写该函数的帮助。 为了获得尽可能多的帮助，第一步是非常明确地写下参数的类型和返回的类型，用下划线表示定义的主体：

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  _

Lean provides a message that describes which variables are available in scope, and the type that’s expected for the result. The ⊢ symbol, called a turnstile due to its resemblance to subway entrances, separates the local variables from the desired type, which is ρ → β in this message:

Lean提供的消息描述了哪些变量在作用域内可用，以及结果的预期类型。 ⊢符号，由于它类似于地铁入口而被称为 turnstile ，将局部变量与所需类型分开，在此消息中为ρ → β：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β

⊢ ρ → β

Because the return type is a function, a good first step is to wrap a fun around the underscore:

因为返回类型是一个函数，所以第一步最好在下划线外套一层fun：

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => _

The resulting message now shows the function’s argument as a local variable:

产生的消息说明现在函数的参数已经成为一个局部变量：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ

⊢ β

The only thing in the context that can produce a β is next, and it will require two arguments to do so. Each argument can itself be an underscore:

上下文中唯一可以产生 β 的是 next， 并且它需要两个参数。 每个参数都可以用下划线表示：

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next _ _

The two underscores have the following respective messages associated with them:

这两个下划线分别有如下的消息：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ

⊢ α



don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ ρ

Attacking the first underscore, only one thing in the context can produce an α, namely result:

先处理第一条下划线，注意到上下文中只有一个东西可以产生α，即result：

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result _) _

Now, both underscores have the same error:

现在两条下划线都有一样的报错了：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ

⊢ ρ

Happily, both underscores can be replaced by env, yielding:

值得高兴的是，两条下划线都可以被 env 替换，得到：

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

The final version can be obtained by undoing the expansion of Reader and cleaning up the explicit details:

要得到最后的版本，只需要把我们前面对 Reader 的展开撤销，并且去掉过于明确的细节：

def Reader.bind (result : Reader ρ α) (next : α → Reader ρ β) : Reader ρ β :=
  fun env => next (result env) env

It’s not always possible to write correct functions by simply “following the types”, and it carries the risk of not understanding the resulting program. However, it can also be easier to understand a program that has been written than one that has not, and the process of filling in the underscores can bring insights. In this case, Reader.bind works just like bind for Id, except it accepts an additional argument that it then passes down to its arguments, and this intuition can help in understanding how it works.

仅仅跟着类型信息走并不总是能写出正确的函数，并且有未能完全理解产生的程序的风险。 然而理解一个已经写出的程序比理解还没写出的要简单，而且逐步填充下划线的内容也可以提供思路。 这张情况下，Reader.bind和 Id 的 bind 很像，唯一区别在于它接受一个额外的参数并传递到其他参数中。这个直觉可以帮助理解它的原理。

Reader.pure, which generates constant functions, and Reader.bind obey the monad contract. To check that Reader.bind (Reader.pure v) f is the same as f v, it’s enough to replace definitions until the last step:

Reader.pure和 Reader.bind 遵循单子约定。 要检查 Reader.bind (Reader.pure v) f 与 f v 等价, 只需要不断地展开定义即可：

Reader.bind (Reader.pure v) f
===>
fun env => f ((Reader.pure v) env) env
===>
fun env => f ((fun _ => v) env) env
===>
fun env => f v env
===>
f v

For every function f, fun x => f x is the same as f, so the first part of the contract is satisfied. To check that Reader.bind r Reader.pure is the same as r, a similar technique works:

对任意函数 f 来说，fun x => f x和 f 是等价的，所以约定的第一部分已经满足。 要检查 Reader.bind r Reader.pure 与 r 等价，只需要相似的技巧：

Reader.bind r Reader.pure
===>
fun env => Reader.pure (r env) env
===>
fun env => (fun _ => (r env)) env
===>
fun env => r env

Because reader actions r are themselves functions, this is the same as r. To check associativity, the same thing can be done for both Reader.bind (Reader.bind r f) g and Reader.bind r (fun x => Reader.bind (f x) g):

因为 r 本身是函数，所以这和 r 也是等价的。 要检查结合律，只需要对 Reader.bind (Reader.bind r f) g 和 Reader.bind r (fun x => Reader.bind (f x) g) 重复同样的步骤：

Reader.bind (Reader.bind r f) g
===>
fun env => g ((Reader.bind r f) env) env
===>
fun env => g ((fun env' => f (r env') env') env) env
===>
fun env => g (f (r env) env) env



Reader.bind r (fun x => Reader.bind (f x) g)
===>
Reader.bind r (fun x => fun env => g (f x env) env)
===>
fun env => (fun x => fun env' => g (f x env') env') (r env) env
===>
fun env => (fun env' => g (f (r env) env') env') env
===>
fun env => g (f (r env) env) env

Thus, a Monad (Reader ρ) instance is justified:

至此，Monad (Reader ρ)实例已经得到了充分验证：

instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

The custom environments that will be passed to the expression evaluator can be represented as lists of pairs:

要被传递给表达式求值器的环境可以用键值对的列表来表示：

abbrev Env : Type := List (String × (Int → Int → Int))

For instance, exampleEnv contains maximum and modulus functions:

例如，exampleEnv包含最大值和模函数：

def exampleEnv : Env := [("max", max), ("mod", (· % ·))]

Lean already has a function List.lookup that finds the value associated with a key in a list of pairs, so applyPrimReader needs only check whether the custom function is present in the environment. It returns 0 if the function is unknown:

Lean已提供函数 List.lookup 用来在键值对的列表中根据键寻找对应的值，所以 applyPrimReader 只需要确认自定义函数是否存在于环境中即可。如果不存在则返回0：

def applyPrimReader (op : String) (x : Int) (y : Int) : Reader Env Int :=
  read >>= fun env =>
  match env.lookup op with
  | none => pure 0
  | some f => pure (f x y)

Using evaluateM with applyPrimReader and an expression results in a function that expects an environment. Luckily, exampleEnv is available:

将evaluateM、applyPrimReader、和一条表达式一起使用，即得到一个接受环境的函数。 而我们前面已经准备好了exampleEnv：

open Expr Prim in
#eval evaluateM applyPrimReader (prim (other "max") (prim plus (const 5) (const 4)) (prim times (const 3) (const 2))) exampleEnv



9

Like Many, Reader is an example of an effect that is difficult to encode in most languages, but type classes and monads make it just as convenient as any other effect. The dynamic or special variables found in Common Lisp, Clojure, and Emacs Lisp can be used like Reader. Similarly, Scheme and Racket’s parameter objects are an effect that exactly correspond to Reader. The Kotlin idiom of context objects can solve a similar problem, but they are fundamentally a means of passing function arguments automatically, so this idiom is more like the encoding as a reader monad than it is an effect in the language.

与 Many 一样，Reader是难以在大多数语言中编码的作用，但类型类和单子使其与任何其他作用一样方便。 Common Lisp、Clojure和Emacs Lisp中的动态或特殊变量可以用作Reader。 类似地，Scheme和Racket的参数对象是一个与 Reader 完全对应的作用。 Kotlin的上下文对象可以解决类似的问题，但根本上是一种自动传递函数参数的方式，因此更像是作为reader单子的编码，而不是语言中实现的作用。

Exercises

练习

Checking Contracts

检查约定

Check the monad contract for State σ and Except ε.

检查 State σ 和 Except ε 满足单子约定。

Readers with Failure

允许Reader失败

Adapt the reader monad example so that it can also indicate failure when the custom operator is not defined, rather than just returning zero. In other words, given these definitions:

调整例子中的reader单子，使得它可以在自定义的运算符不存在时提供错误信息而不是直接返回0。 换句话说，给定这些定义：

def ReaderOption (ρ : Type) (α : Type) : Type := ρ → Option α

def ReaderExcept (ε : Type) (ρ : Type) (α : Type) : Type := ρ → Except ε α

do the following: 1. Write suitable pure and bind functions 2. Check that these functions satisfy the Monad contract 3. Write Monad instances for ReaderOption and ReaderExcept 4. Define suitable applyPrim operators and test them with evaluateM on some example expressions

要做的是：

1. 实现恰当的 pure 和 bind 函数
2. 验证这些函数满足 Monad 约定
3. 为 ReaderOption 和 ReaderExcept 实现 Monad 实例
4. 为它们定义恰当的 applyPrim 运算符，并且将它们和 evaluateM 一起测试一些例子

A Tracing Evaluator

带有跟踪信息的求值器

The WithLog type can be used with the evaluator to add optional tracing of some operations. In particular, the type ToTrace can serve as a signal to trace a given operator:

WithLog类型可以和求值器一起使用，来实现对某些运算的跟踪。 特别地，可以使用 ToTrace 类型来追踪某个给定的运算符：

inductive ToTrace (α : Type) : Type where
  | trace : α → ToTrace α

For the tracing evaluator, expressions should have type Expr (Prim (ToTrace (Prim Empty))). This says that the operators in the expression consist of addition, subtraction, and multiplication, augmented with traced versions of each. The innermost argument is Empty to signal that there are no further special operators inside of trace, only the three basic ones.

对于带有跟踪信息的求值器，表达式应该具有类型Expr (Prim (ToTrace (Prim Empty))). 这说明表达式中的运算符由附加参数的加、减、乘运算组成。最内层的参数是 Empty，说明在trace 内部没有特殊运算符，只有三种基本运算。

Do the following: 1. Implement a Monad (WithLog logged) instance 2. Write an applyTraced function to apply traced operators to their arguments, logging both the operator and the arguments, with type ToTrace (Prim Empty) → Int → Int → WithLog (Prim Empty × Int × Int) Int

要做的是：

1. 实现 Monad (WithLog logged) 实例
2. 写一个 applyTraced 来将被追踪的运算符应用到参数，将运算符和参数记录到日志，类型为：ToTrace (Prim Empty) → Int → Int → WithLog (Prim Empty × Int × Int) Int

If the exercise has been completed correctly, then

如果练习已经正确实现，那么

open Expr Prim ToTrace in
#eval evaluateM applyTraced (prim (other (trace times)) (prim (other (trace plus)) (const 1) (const 2)) (prim (other (trace minus)) (const 3) (const 4)))

should result in

将有如下结果

{ log := [(Prim.plus, 1, 2), (Prim.minus, 3, 4), (Prim.times, 3, -1)], val := -3 }

Hint: values of type Prim Empty will appear in the resulting log. In order to display them as a result of #eval, the following instances are required:

提示：Prim Empty会出现在日志中。为了让它们能被 #eval 输出，需要下面几个实例：

 deriving instance Repr for WithLog
deriving instance Repr for Empty
deriving instance Repr for Prim

do-Notation for Monads

单子的 do-记法

While APIs based on monads are very powerful, the explicit use of >>= with anonymous functions is still somewhat noisy. Just as infix operators are used instead of explicit calls to HAdd.hAdd, Lean provides a syntax for monads called do-notation that can make programs that use monads easier to read and write. This is the very same do-notation that is used to write programs in IO, and IO is also a monad.

基于单子的 API 非常强大，但显式使用 >>= 和匿名函数仍然有些繁琐。 正如使用中缀运算符代替显式调用 HAdd.hAdd 一样，Lean 提供了一种称为 do-记法 的单子语法，它可以使使用单子的程序更易于阅读和编写。 这与用于编写 IO 程序的 do-记法完全相同，而 IO 也是一个单子。

In Hello, World!, the do syntax is used to combine IO actions, but the meaning of these programs is explained directly. Understanding how to program with monads means that do can now be explained in terms of how it translates into uses of the underlying monad operators.

在 Hello, World! 中，do 语法用于组合 IO 活动， 但这些程序的含义是直接解释的。理解如何运用单子进行编程意味着现在可以用 do 来解释它如何转换为对底层单子运算符的使用。

The first translation of do is used when the only statement in the do is a single expression E. In this case, the do is removed, so

当 do 中的唯一语句是单个表达式 E 时，会使用 do 的第一种翻译。 在这种情况下，do 被删除，因此

do E

会被翻译为

E

The second translation is used when the first statement of the do is a let with an arrow, binding a local variable. This translates to a use of >>= together with a function that binds that very same variable, so

当 do 的第一个语句是带有箭头的 let 绑定一个局部变量时，则使用第二种翻译。 它会翻译为使用 >>= 以及绑定同一变量的函数，因此

do let x ← E1
   Stmt
   ...
   En

translates to

会被翻译为

E1 >>= fun x =>
do Stmt
   ...
   En

When the first statement of the do block is an expression, then it is considered to be a monadic action that returns Unit, so the function matches the Unit constructor and

当 do 块的第一个语句是一个表达式时，它会被认为是一个返回 Unit 的单子操作， 因此该函数匹配 Unit 构造子，而

do E1
   Stmt
   ...
   En

translates to

会被翻译为

E1 >>= fun () =>
do Stmt
   ...
   En

Finally, when the first statement of the do block is a let that uses :=, the translated form is an ordinary let expression, so

最后，当 do 块的第一个语句是使用 := 的 let 时，翻译后的形式是一个普通的 let 表达式，因此

do let x := E1
   Stmt
   ...
   En

translates to

会被翻译为

let x := E1
do Stmt
   ...
   En

The definition of firstThirdFifthSeventh that uses the Monad class looks like this:

使用 Monad 类的 firstThirdFifthSeventh 的定义如下：

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

Using do-notation, it becomes significantly more readable:

使用 do-记法，它会变得更加易读：

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) := do
  let first ← lookup xs 0
  let third ← lookup xs 2
  let fifth ← lookup xs 4
  let seventh ← lookup xs 6
  pure (first, third, fifth, seventh)

Without the Monad type class, the function number that numbers the nodes of a tree was written:

若没有 Monad 类型，则对树的节点进行编号的函数 number 写作如下形式：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => ok BinTree.leaf
    | BinTree.branch left x right =>
      helper left ~~> fun numberedLeft =>
      get ~~> fun n =>
      set (n + 1) ~~> fun () =>
      helper right ~~> fun numberedRight =>
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

有了 Monad 和 do，其定义就简洁多了：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => pure BinTree.leaf
    | BinTree.branch left x right => do
      let numberedLeft ← helper left
      let n ← get
      set (n + 1)
      let numberedRight ← helper right
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

使用 do 与 IO 的所有便利性在使用其他单子时也可用。 例如，嵌套操作也适用于任何单子。mapM 的原始定义为：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)

With do-notation, it can be written:

使用 do-记法，可以写成：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs => do
    let hd ← f x
    let tl ← mapM f xs
    pure (hd :: tl)

Using nested actions makes it almost as short as the original non-monadic map:

使用嵌套活动会让它与原始非单子 map 一样简洁：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs => do
    pure ((← f x) :: (← mapM f xs))

Using nested actions, number can be made much more concise:

使用嵌套活动，number 可以变得更加简洁：

def increment : State Nat Nat := do
  let n ← get
  set (n + 1)
  pure n

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => pure BinTree.leaf
    | BinTree.branch left x right => do
      pure (BinTree.branch (← helper left) ((← increment), x) (← helper right))
  (helper t 0).snd

Exercises

练习

• Rewrite evaluateM, its helpers, and the different specific use cases using do-notation instead of explicit calls to >>=. * Rewrite firstThirdFifthSeventh using nested actions.

  • 使用 do-记法而非显式调用 >>= 重写 evaluateM、辅助函数以及不同的特定用例。
  • 使用嵌套操作重写 firstThirdFifthSeventh。

The IO Monad

IO 单子

IO as a monad can be understood from two perspectives, which were described in the section on running programs. Each can help to understand the meanings of pure and bind for IO.

IO 作为单子可以从两个角度理解，这在 运行程序 一节中进行了描述。每个角度都可以帮助理解 IO 的 pure 和 bind 的含义。

From the first perspective, an IO action is an instruction to Lean’s run-time system. For example, the instruction might be “read a string from this file descriptor, then re-invoke the pure Lean code with the string”. This perspective is an exterior one, viewing the program from the perspective of the operating system. In this case, pure is an IO action that does not request any effects from the RTS, and bind instructs the RTS to first carry out one potentially-effectful operation and then invoke the rest of the program with the resulting value.

从第一个视角看，IO 活动是 Lean 运行时系统的指令。 例如，指令可能是「从该文件描述符读取字符串，然后使用该字符串重新调用纯 Lean 代码」。 这是一种 外部 的视角，即从操作系统的视角看待程序。 在这种情况下，pure 是一个不请求 RTS 产生任何作用的 IO 活动， 而 bind 指示 RTS 首先执行一个产生潜在作用的操作，然后使用结果值调用程序的其余部分。

From the second perspective, an IO action transforms the whole world. IO actions are actually pure, because they receive a unique world as an argument and then return the changed world. This perspective is an interior one that matches how IO is represented inside of Lean. The world is represented in Lean as a token, and the IO monad is structured to make sure that each token is used exactly once.

从第二个视角看，IO 活动会变换整个世界。IO 活动实际上是纯（Pure）的， 因为它接受一个唯一的世界作为参数，然后返回改变后的世界。 这是一种 内部 的视角，它对应了 IO 在 Lean 中的表示方式。 世界在 Lean 中表示为一个标记，而 IO 单子的结构化可以确保标记刚好使用一次。

To see how this works, it can be helpful to peel back one definition at a time. The #print command reveals the internals of Lean datatypes and definitions. For example,

为了了解其工作原理，逐层解析它的定义会很有帮助。 #print 命令揭示了 Lean 数据类型和定义的内部结构。例如，

#print Nat

results in

的结果为

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

and

而

#print Char.isAlpha

results in

的结果为

def Char.isAlpha : Char → Bool :=
fun c => Char.isUpper c || Char.isLower c

Sometimes, the output of #print includes Lean features that have not yet been presented in this book. For example,

有时，#print 的输出包含了本书中尚未展示的 Lean 特性。例如，

#print List.isEmpty

produces

会产生

def List.isEmpty.{u} : {α : Type u} → List α → Bool :=
fun {α} x =>
  match x with
  | [] => true
  | head :: tail => false

which includes a .{u} after the definition’s name, and annotates types as Type u rather than just Type. This can be safely ignored for now.

它在定义名的后面包含了一个 .{u} ，并将类型标注为 Type u 而非只是 Type。 目前可以安全地忽略它。

Printing the definition of IO shows that it’s defined in terms of simpler structures:

打印 IO 的定义表明它是根据更简单的结构定义的：

#print IO



@[reducible] def IO : Type → Type :=
EIO IO.Error

IO.Error represents all the errors that could be thrown by an IO action:

IO.Error 表示 IO 活动可能抛出的所有错误：

#print IO.Error



inductive IO.Error : Type
number of parameters: 0
constructors:
IO.Error.alreadyExists : Option String → UInt32 → String → IO.Error
IO.Error.otherError : UInt32 → String → IO.Error
IO.Error.resourceBusy : UInt32 → String → IO.Error
IO.Error.resourceVanished : UInt32 → String → IO.Error
IO.Error.unsupportedOperation : UInt32 → String → IO.Error
IO.Error.hardwareFault : UInt32 → String → IO.Error
IO.Error.unsatisfiedConstraints : UInt32 → String → IO.Error
IO.Error.illegalOperation : UInt32 → String → IO.Error
IO.Error.protocolError : UInt32 → String → IO.Error
IO.Error.timeExpired : UInt32 → String → IO.Error
IO.Error.interrupted : String → UInt32 → String → IO.Error
IO.Error.noFileOrDirectory : String → UInt32 → String → IO.Error
IO.Error.invalidArgument : Option String → UInt32 → String → IO.Error
IO.Error.permissionDenied : Option String → UInt32 → String → IO.Error
IO.Error.resourceExhausted : Option String → UInt32 → String → IO.Error
IO.Error.inappropriateType : Option String → UInt32 → String → IO.Error
IO.Error.noSuchThing : Option String → UInt32 → String → IO.Error
IO.Error.unexpectedEof : IO.Error
IO.Error.userError : String → IO.Error

EIO ε α represents IO actions that will either terminate with an error of type ε or succeed with a value of type α. This means that, like the Except ε monad, the IO monad includes the ability to define error handling and exceptions.

EIO ε α 表示一个 IO 活动，它将以类型为 ε 的错误表示终止，或者以类型为 α 的值表示成功。 这意味着，与 Except ε 单子一样，IO 单子也包括定义错误处理和异常的能力。

Peeling back another layer, EIO is itself defined in terms of a simpler structure: Peeling back another layer, EIO is itself defined in terms of a simpler structure:

剥离另一层，EIO 本身又是根据更简单的结构定义的：

#print EIO



def EIO : Type → Type → Type :=
fun ε => EStateM ε IO.RealWorld

The EStateM monad includes both errors and state—it’s a combination of Except and State. It is defined using another type, EStateM.Result:

EStateM 单子同时包括错误和状态——它是 Except 和 State 的组合。 它使用另一个类型 EStateM.Result 定义：

#print EStateM



def EStateM.{u} : Type u → Type u → Type u → Type u :=
fun ε σ α => σ → EStateM.Result ε σ α

In other words, a program with type EStateM ε σ α is a function that accepts an initial state of type σ and returns an EStateM.Result ε σ α.

换句话说，类型为 EStateM ε σ α 的程序是一个函数， 它接受类型为 σ 的初始状态并返回一个 EStateM.Result ε σ α。

EStateM.Result is very much like the definition of Except, with one constructor that indicates a successful termination and one constructor that indicates an error:

EStateM.Result 与 Except 的定义非常相似，一个构造子表示成功终止， 令一个构造子表示错误：

#print EStateM.Result



inductive EStateM.Result.{u} : Type u → Type u → Type u → Type u
number of parameters: 3
constructors:
EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α

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

Just like Except ε α, the ok constructor includes a result of type α, and the error constructor includes an exception of type ε. Unlike Except, both constructors have an additional state field that includes the final state of the computation.

就像 Except ε α 一样，ok 构造子包含类型为 α 的结果， error 构造子包含类型为 ε 的异常。与 Except 不同， 这两个构造子都有一个附加的状态字段，其中包含计算的最终状态。

The Monad instance for EStateM ε σ requires pure and bind. Just as with State, the implementation of pure for EStateM accepts an initial state and returns it unchanged, and just as with Except, it returns its argument in the ok constructor:

EStateM ε σ 的 Monad 实例需要 pure 和 bind。 与 State 一样，EStateM 的 pure 实现接受一个初始状态并将其返回而不改变， 并且与 Except 一样，它在 ok 构造子中返回其参数：

#print EStateM.pure



protected def EStateM.pure.{u} : {ε σ α : Type u} → α → EStateM ε σ α :=
fun {ε σ α} a s => EStateM.Result.ok a s

protected means that the full name EStateM.pure is needed even if the EStateM namespace has been opened.

protected 意味着即使打开了 EStateM 命名空间，也需要完整的名称 EStateM.pure。

Similarly, bind for EStateM takes an initial state as an argument. It passes this initial state to its first action. Like bind for Except, it then checks whether the result is an error. If so, the error is returned unchanged and the second argument to bind remains unused. If the result was a success, then the second argument is applied to both the returned value and to the resulting state.

类似地，EStateM 的 bind 将初始状态作为参数。它将此初始状态传递给其第一个操作。 与 Except 的 bind 一样，它然后检查结果是否为错误。如果是，则错误将保持不变， 并且 bind 的第二个参数保持未使用。如果结果成功，则将第二个参数应用于返回值和结果状态。

#print EStateM.bind



protected def EStateM.bind.{u} : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β :=
fun {ε σ α β} x f s =>
  match x s with
  | EStateM.Result.ok a s => f a s

| EStateM.Result.error e s => EStateM.Result.error e s

Putting all of this together, IO is a monad that tracks state and errors at the same time. The collection of available errors is that given by the datatype IO.Error, which has constructors that describe many things that can go wrong in a program. The state is a type that represents the real world, called IO.RealWorld. Each basic IO action receives this real world and returns another one, paired either with an error or a result. In IO, pure returns the world unchanged, while bind passes the modified world from one action into the next action.

综上所述，IO 是同时跟踪状态和错误的单子。可用错误的集合由数据类型 IO.Error 给出， 该数据类型具有描述程序中可能出错的许多情况的构造子。状态是一种表示现实世界的类型， 称为 IO.RealWorld。每个基本的 IO 活动都会接收这个现实世界并返回另一个，与错误或结果配对。 在 IO 中，pure 返回未更改的世界，而 bind 将修改后的世界从一个活动传递到下一个活动。

Because the entire universe doesn’t fit in a computer’s memory, the world being passed around is just a representation. So long as world tokens are not re-used, the representation is safe. This means that world tokens do not need to contain any data at all: Because the entire universe doesn’t fit in a computer’s memory, the world being passed around is just a representation. So long as world tokens are not re-used, the representation is safe. This means that world tokens do not need to contain any data at all:

由于计算机内存无法容纳整个宇宙，因此传递的世界仅仅是一种表示。 只要不重复使用世界标记，该表示就是安全的。这意味着世界标记根本不需要包含任何数据：

#print IO.RealWorld



def IO.RealWorld : Type :=
Unit

Additional Conveniences

其他便利功能

Shared Argument Types

共享参数类型

When defining a function that takes multiple arguments that have the same type, both can be written before the same colon. For example,

定义具有相同类型的多个参数时，可以把它们写在同一个冒号之前。 例如：

def equal? [BEq α] (x : α) (y : α) : Option α :=
  if x == y then
    some x
  else
    none

can be written

可以写成

def equal? [BEq α] (x y : α) : Option α :=
  if x == y then
    some x
  else
    none

This is especially useful when the type signature is large.

这在类型签名很长的时候特别有用。

Leading Dot Notation

开头的点号

The constructors of an inductive type are in a namespace. This allows multiple related inductive types to use the same constructor names, but it can lead to programs becoming verbose. In contexts where the inductive type in question is known, the namespace can be omitted by preceding the constructor’s name with a dot, and Lean uses the expected type to resolve the constructor names. For example, a function that mirrors a binary tree can be written:

一个归纳类型的所有构造子都存在于一个命名空间中。 因此允许不同的归纳类型有同名构造子，但是这也会导致程序变得啰嗦。 当问题中的归纳类型已知时，可以命名空间可以省略，只需要在构造子前保留点号，Lean可以根据该处期望的类型来决定如何选择构造子。 例如将二叉树镜像的函数：

def BinTree.mirror : BinTree α → BinTree α
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)

Omitting the namespaces makes it significantly shorter, at the cost of making the program harder to read in contexts like code review tools that don’t include the Lean compiler:

省略命名空间使代码显著变短，但代价是在没有Lean编译器，例如code review时，代码会变得难以阅读：

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

Using the expected type of an expression to disambiguate a namespace is also applicable to names other than constructors. If BinTree.empty is defined as an alternative way of creating BinTrees, then it can also be used with dot notation:

通过期望的类型来消除命名空间的歧义，同样可以应用于构造子之外的名称。 例如BinTree.empty定义为一种创建BinTree的方式，那么它也可以和点号一起使用：

def BinTree.empty : BinTree α := .leaf

#check (.empty : BinTree Nat)



BinTree.empty : BinTree Nat

Or-Patterns

或-模式

In contexts that allow multiple patterns, such as match-expressions, multiple patterns may share their result expressions. The datatype Weekday that represents days of the week:

当有多个模式匹配的分支时，例如match表达式，那么不同的模式可以共享同一个结果表达式。 表示一周的每一天的类型Weekday：

inductive Weekday where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
  deriving Repr

Pattern matching can be used to check whether a day is a weekend:

可以用模式匹配检查某一天是否是周末：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | Weekday.saturday => true
  | Weekday.sunday => true
  | _ => false

This can already be simplified by using constructor dot notation:

首先可以用点号来简化：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday => true
  | .sunday => true
  | _ => false

Because both weekend patterns have the same result expression (true), they can be condensed into one:

因为周末的两天都有相同的结果true，所以可以精简成：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday | .sunday => true
  | _ => false

This can be further simplified into a version in which the argument is not named:

进一步可以简化成没有参数名称的函数：

def Weekday.isWeekend : Weekday → Bool
  | .saturday | .sunday => true
  | _ => false

Behind the scenes, the result expression is simply duplicated across each pattern. This means that patterns can bind variables, as in this example that removes the inl and inr constructors from a sum type in which both contain the same type of value:

实际上结果表达式只是简单地被复制。所以模式也可以绑定变量，这个例子在和类型(Sum Type)两边具有相同类型时，将inl和inr构造子去除：

def condense : α ⊕ α → α
  | .inl x | .inr x => x

Because the result expression is duplicated, the variables bound by the patterns are not required to have the same types. Overloaded functions that work for multiple types may be used to write a single result expression that works for patterns that bind variables of different types:

但是因为结果表达式只是被复制，所以模式绑定的变量也可以具有不同类型。 重载的函数可以让同一个结果表达式用于多个绑定不同类型的变量的模式：

def stringy : Nat ⊕ Weekday → String
  | .inl x | .inr x => s!"It is {repr x}"

In practice, only variables shared in all patterns can be referred to in the result expression, because the result must make sense for each pattern. In getTheNat, only n can be accessed, and attempts to use either x or y lead to errors.

实践中，只有在所有模式都存在的变量才可以在结果表达式中引用，因为这条表达式必须对所有分支都有意义。 getTheNat中只有n可以被访问，使用x或y将会导致错误。

def getTheNat : (Nat × α) ⊕ (Nat × β) → Nat
  | .inl (n, x) | .inr (n, y) => n

Attempting to access x in a similar definition causes an error because there is no x available in the second pattern:

这种类似的情况中访问x同样会导致错误，因为x在第二个模式中不存在：

def getTheAlpha : (Nat × α) ⊕ (Nat × α) → α
  | .inl (n, x) | .inr (n, y) => x



unknown identifier 'x'

The fact that the result expression is essentially copy-pasted to each branch of the pattern match can lead to some surprising behavior. For example, the following definitions are acceptable because the inr version of the result expression refers to the global definition of str:

简单地对结果表达式进行复制，会导致某些令人惊讶的行为。 例如，下列定义是合法的，因为inr分支实际上引用的是全局定义str：

def str := "Some string"

def getTheString : (Nat × String) ⊕ (Nat × β) → String
  | .inl (n, str) | .inr (n, y) => str

Calling this function on both constructors reveals the confusing behavior. In the first case, a type annotation is needed to tell Lean which type β should be:

在不同分支上调用该函数会让人困惑。 第一种情况中，需要提供类型标记告诉Lean类型β是什么：

#eval getTheString (.inl (20, "twenty") : (Nat × String) ⊕ (Nat × String))



"twenty"

In the second case, the global definition is used:

第二种情况被使用的是全局定义：

#eval getTheString (.inr (20, "twenty"))



"Some string"

Using or-patterns can vastly simplify some definitions and increase their clarity, as in Weekday.isWeekend. Because there is a potential for confusing behavior, it’s a good idea to be careful when using them, especially when variables of multiple types or disjoint sets of variables are involved.

使用或-模式可以极大简化某些定义，让它们更加清晰，例如Weekday.isWeekend. 但因为存在可能导致困惑的行为，需要十分小心地使用，特别是涉及不同类型的变量，或不相交的变量集合时。

Summary

总结

Encoding Side Effects

编码副作用

Lean is a pure functional language. This means that it does not include side effects such as mutable variables, logging, or exceptions. However, most side effects can be encoded using a combination of functions and inductive types or structures. For example, mutable state can be encoded as a function from an initial state to a pair of a final state and a result, and exceptions can be encoded as an inductive type with constructors for successful termination and errors.

是一种纯函数式语言。这意味着它不包含副作用，例如可变变量、日志记录或异常。 但是，大多数副作用都可以使用函数和归纳类型或结构体的组合进行编码 。 例如，可变状态可以编码为从初始状态到一对最终状态和结果的函数， 异常可以编码为具有成功终止构造子和错误构造子的归纳类型。

Each set of encoded effects is a type. As a result, if a program uses these encoded effects, then this is apparent in its type. Functional programming does not mean that programs can’t use effects, it simply requires that they be honest about which effects they use. A Lean type signature describes not only the types of arguments that a function expects and the type of result that it returns, but also which effects it may use.

每组编码的作用都是一种类型。因此，如果程序使用这些编码作用，那么这在它的类型中是显而易见的。 函数式编程并不意味着程序不能使用作用，它只是要求它们 诚实地 说明它们使用的作用。 Lean 类型签名不仅描述了函数期望的参数类型和它返回的结果类型，还描述了它可能使用的作用。

The Monad Type Class

单子类型类

It’s possible to write purely functional programs in languages that allow effects anywhere. For example, 2 + 3 is a valid Python program that has no effects at all. Similarly, combining programs that have effects requires a way to state the order in which the effects must occur. It matters whether an exception is thrown before or after modifying a variable, after all.

在允许在任何地方使用作用的语言中编写纯函数式程序是可能的。 例如，2 + 3 是一个有效的 Python 程序，它没有任何作用。 类似地，组合具有作用的程序需要一种方法来说明作用必须发生的顺序。 毕竟，异常是在修改变量之前还是之后抛出是有区别的。

The type class Monad captures these two important properties. It has two methods: pure represents programs that have no effects, and bind sequences effectful programs. The contract for Monad instances ensures that bind and pure actually capture pure computation and sequencing.

类型类 Monad 刻画了这两个重要属性。它有两个方法：pure 表示没有副作用的程序， bind 顺序执行有副作用的程序。Monad 实例的约束确保了 bind 和 pure 实际上刻画了纯计算和顺序执行。

do-Notation for Monads

单子的 do-记法

Rather than being limited to IO, do-notation works for any monad. It allows programs that use monads to be written in a style that is reminiscent of statement-oriented languages, with statements sequenced after one another. Additionally, do-notation enables a number of additional convenient shorthands, such as nested actions. A program written with do is translated to applications of >>= behind the scenes.

do 符号不仅限于 IO，它也适用于任何单子。 它允许使用单子的程序以类似于面向语句的语言的风格编写，语句一个接一个地顺序执行。 此外，do-记法还支持许多其他方便的简写，例如嵌套动作。 使用 do 编写的程序在幕后会被翻译为 >>= 的应用。

Custom Monads

定制单子

Different languages provide different sets of side effects. While most languages feature mutable variables and file I/O, not all have features like exceptions. Other languages offer effects that are rare or unique, like Icon’s search-based program execution, Scheme and Ruby’s continuations, and Common Lisp’s resumable exceptions. An advantage to encoding effects with monads is that programs are not limited to the set of effects that are provided by the language. Because Lean is designed to make programming with any monad convenient, programmers are free to choose exactly the set of side effects that make sense for any given application.

不同的语言提供不同的副作用集。虽然大多数语言都具有可变变量和文件 I/O， 但并非所有语言都具有异常等特性。其他语言提供罕见或独特的副作用， 例如 Icon 基于搜索的程序执行、Scheme 和 Ruby 的续体以及 Common Lisp 的可恢复异常。 用单子对副作用进行编码的一个优点是，程序不受语言提供的副作用集的限制。 由于 Lean 被设计为能方便地使用任何单子进行编程， 因此程序员可以自由选择最适合任何给定应用的副作用集。

The IO Monad

IO 单子

Programs that can affect the real world are written as IO actions in Lean. IO is one monad among many. The IO monad encodes state and exceptions, with the state being used to keep track of the state of the world and the exceptions modeling failure and recovery.

可以在现实世界中产生影响的程序在 Lean 中被写作 IO 活动。 IO 是众多单子中的一个。IO 单子对状态和异常进行编码，其中状态用于跟踪世界的状态， 异常则对失败和恢复进行建模。