单子的 `do`-记法

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

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

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

do E

会被翻译为

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

do let x ← E1
   Stmt
   ...
   En

会被翻译为

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

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

do E1
   Stmt
   ...
   En

会被翻译为

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

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

do let x := E1
   Stmt
   ...
   En

会被翻译为

let x := E1
do Stmt
   ...
   En

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

练习

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

Lean 函数式编程

单子的 do-记法

练习

单子的 `do`-记法