4.4. 单子的 `do`-记法🔗

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

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

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

do E

会被翻译为

E

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

do let x ← E₁
   Stmt
   …
   Eₙ

会被翻译为

E₁ >>= fun x =>
  do Stmt
     …
     Eₙ

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

do E₁
   Stmt
   …
   Eₙ

会被翻译为

E₁ >>= fun () =>
  do Stmt
     …
     Eₙ

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

do let x := E₁
   Stmt
   …
   Eₙ

会被翻译为

let x := E₁
do Stmt
   …
   Eₙ

使用 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)

使用 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)

若没有 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)

使用 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)

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

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

使用嵌套操作，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

4.4.1. 练习🔗

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

4.4. 单子的 do-记法🔗

4.4.1. 练习🔗

4.4. 单子的 `do`-记法🔗