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`-记法🔗