更多 do 的特性

Lean 的 do-标记为使用单子编写程序提供了一种类似命令式编程语言的语法。 除了为使用单子的程序提供方便的语法外，do-标记还提供了使用某些单子转换器的语法。

单分支 if

在单子中工作时，一种常见的模式是只有当某些条件为真时才执行副作用。 例如，countLetters 包含对元音或辅音的检查，而两者都不是的字母对状态没有影响。 通过将 else 分支设置为 pure ()，可以达成这一目的，因为 pure () 不会产生任何影响：

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

如果 if 是一个 do 块中的语句，而不是一个表达式，那么 else pure () 可以直接省略，Lean 会自动插入它。 下面的 countLetters 定义完全等价：

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 throw (.notALetter c)
      loop cs
  loop str.toList

使用状态单子计算列表中满足某种单子检查的条目的程序，可以写成下面这样：

def count [Monad m] [MonadState Nat m] (p : α → m Bool) : List α → m Unit
  | [] => pure ()
  | x :: xs => do
    if ← p x then
      modify (· + 1)
    count p xs

同样，if not E1 then STMT... 可以写成 unless E1 do STMT... 。 count 的相反（计算不满足单子检查的条目），的可以用 unless 代替 if：

def countNot [Monad m] [MonadState Nat m] (p : α → m Bool) : List α → m Unit
  | [] => pure ()
  | x :: xs => do
    unless ← p x do
      modify (· + 1)
    countNot p xs

理解单分支的 if 和 unless 不需要考虑单子转换器。 它们只需用 pure () 替换缺失的分支。 然而，本节中的其余扩展要求 Lean 自动重写 do 块，以便在写入 do 块的单子上添加一个局部转换器。

提前返回

标准库中有一个函数 List.find?，用于返回列表中满足某些检查条件的第一个条目。 一个简单的实现并没有利用 Option 是一个单子的事实，而是使用一个递归函数在列表中循环，并使用 if 在找到所需条目时停止循环：

def List.find? (p : α → Bool) : List α → Option α
  | [] => none
  | x :: xs =>
    if p x then
      some x
    else
      find? p xs

命令式语言通常会使用 return 关键字来终止函数的执行，并立即将某个值返回给调用者。 在 Lean 中，这个关键字在 do-标记中可用，return 停止了一个 do 块的执行，且 return 的参数是从单子返回的值。 换句话说，List.find? 可以这样写：

def List.find? (p : α → Bool) : List α → Option α
  | [] => failure
  | x :: xs => do
    if p x then return x
    find? p xs

在命令式语言中，提前返回有点像异常，只能导致当前堆栈帧被释放。 提前返回和异常都会终止代码块的执行，从而有效地用抛出的值替换周围的代码。 在后台，Lean 中的提前返回是使用 ExceptT 的一个版本实现的。 每个使用提前返回的 do 代码块都被包裹在异常处理程序中（在函数 tryCatch 的意义上）。 提前返回被转换为将值作为异常抛出，处理程序捕获抛出的值并立即返回。 换句话说，do 块的原始返回值类型也被用作异常类型。

更具体地说，当异常类型和返回类型相同时，辅助函数 runCatch 会从单子转换器栈的顶部删除一层 ExceptT ：

def runCatch [Monad m] (action : ExceptT α m α) : m α := do
  match ← action with
  | Except.ok x => pure x
  | Except.error x => pure x

将 List.find? 中使用提前返回的 do 块封装为使用 runCatch 的 do 块，并用 throw 代替提前返回，从而将其转换为不使用提前返回的 do 块：

def List.find? (p : α → Bool) : List α → Option α
  | [] => failure
  | x :: xs =>
    runCatch do
      if p x then throw x else pure ()
      monadLift (find? p xs)

提前返回有用的另一种情况是，如果参数或输入不正确，命令行应用程序会提前终止。 许多程序在进入主体部分之前，都会有一个验证参数和输入的部分。 以下版本的 问候程序 hello-name 会检查是否没有提供命令行参数：

def main (argv : List String) : IO UInt32 := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  let stderr ← IO.getStderr

  unless argv == [] do
    stderr.putStrLn s!"Expected no arguments, but got {argv.length}"
    return 1

  stdout.putStrLn "How would you like to be addressed?"
  stdout.flush

  let name := (← stdin.getLine).trim
  if name == "" then
    stderr.putStrLn s!"No name provided"
    return 1

  stdout.putStrLn s!"Hello, {name}!"

  return 0

在不带参数的情况下运行该程序并输入姓名 David，得到的结果与前一版本相同：

$ lean --run EarlyReturn.lean
How would you like to be addressed?
David
Hello, David!

将名称作为命令行参数而不是答案提供会导致错误：

$ lean --run EarlyReturn.lean David
Expected no arguments, but got 1

不提供名字也会导致其他错误：

$ lean --run EarlyReturn.lean
How would you like to be addressed?

No name provided

使用提前返回的程序可以避免像下面这个不使用提前返回的版本一样嵌套控制流：

def main (argv : List String) : IO UInt32 := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  let stderr ← IO.getStderr

  if argv != [] then
    stderr.putStrLn s!"Expected no arguments, but got {argv.length}"
    pure 1
  else
    stdout.putStrLn "How would you like to be addressed?"
    stdout.flush

    let name := (← stdin.getLine).trim
    if name == "" then
      stderr.putStrLn s!"No name provided"
      pure 1
    else
      stdout.putStrLn s!"Hello, {name}!"
      pure 0

Lean 中的提前返回与命令式语言中的提前返回之间的一个重要区别是，Lean 的提前返回仅适用于当前的 do 块。 当函数的整个定义都在同一个 do 块中时，这个区别并不重要。 但如果 do 出现在其他结构之下，那么这种差异就会变得很明显。 例如，下面这个 greet 的定义：

def greet (name : String) : String :=
  "Hello, " ++ Id.run do return name

表达式 greet "David" 被求值为 "Hello, David" ，而不只是 "David" 。

循环

正如每个具有可变状态的程序都可以改写成将状态作为参数传递的程序一样，每个循环都可以改写成递归函数。 从某个角度看，List.find? 作为递归函数是最清晰不过的了。 毕竟，它的定义反映了列表的结构：如果头部通过了检查，那么就应该返回；否则就在尾部查找。 当没有条目时，答案就是 none。 从另一个角度看，List.find? 作为一个循环最为清晰。 毕竟，程序会按顺序查询条目，直到找到合适的条目，然后终止。 如果循环没有返回就终止了，那么答案就是 none。

使用 ForM 循环

Lean 包含一个类型类，用于描述在某个单子中对容器类型的循环。 这个类型类叫做 ForM：

class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂)) where
  forM [Monad m] : γ → (α → m PUnit) → m PUnit

该类型类非常通用。 参数 m 是一个具有某些预期作用的单子， γ 是要循环的集合，α 是集合中元素的类型。 通常情况下，m 可以是任何单子，但也可以是只支持在 IO 中循环的数据结构。 方法 forM 接收一个集合、一个要对集合中每个元素产生影响的单子操作，然后负责运行这些动作。

List 的实例允许 m 是任何单子，它将 γ 设置为 List α，并将类型类的 α 设置为列表中的 α：

def List.forM [Monad m] : List α → (α → m PUnit) → m PUnit
  | [], _ => pure ()
  | x :: xs, action => do
    action x
    forM xs action

instance : ForM m (List α) α where
  forM := List.forM

来自 doug 的函数 doList 是针对列表的 forM。 由于 forM 的目的是在 do 块中使用，它使用了 Monad 而不是 Applicative。 使用 forM 可以使 countLetters 更短：

def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
  forM str.toList fun c => do
    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 throw (.notALetter c)

Many 的实例也差不多：

def Many.forM [Monad m] : Many α → (α → m PUnit) → m PUnit
  | Many.none, _ => pure ()
  | Many.more first rest, action => do
    action first
    forM (rest ()) action

instance : ForM m (Many α) α where
  forM := Many.forM

因为 γ 可以是任何类型，所以 ForM 可以支持非多态集合。 一个非常简单的集合是按相反顺序排列的小于某个给定数的自然数：

structure AllLessThan where
  num : Nat

它的 forM 操作符将给定的操作应用于每个更小的 Nat：

def AllLessThan.forM [Monad m] (coll : AllLessThan) (action : Nat → m Unit) : m Unit :=
  let rec countdown : Nat → m Unit
    | 0 => pure ()
    | n + 1 => do
      action n
      countdown n
  countdown coll.num

instance : ForM m AllLessThan Nat where
  forM := AllLessThan.forM

在每个小于 5 的数字上运行 IO.println 可以用 forM 来实现：

#eval forM { num := 5 : AllLessThan } IO.println

4
3
2
1
0

一个仅在特定单子中工作的 ForM 实例示例是，循环读取从 IO 流（如标准输入）获取的行：

structure LinesOf where
  stream : IO.FS.Stream

partial def LinesOf.forM (readFrom : LinesOf) (action : String → IO Unit) : IO Unit := do
  let line ← readFrom.stream.getLine
  if line == "" then return ()
  action line
  forM readFrom action

instance : ForM IO LinesOf String where
  forM := LinesOf.forM

forM 的定义被标记为 partial ，因为无法保证流是有限的。 在这种情况下，IO.FS.Stream.getLine 只在 IO 单子中起作用，因此不能使用其他单子进行循环。

本示例程序使用这种循环结构过滤掉不包含字母的行：

def main (argv : List String) : IO UInt32 := do
  if argv != [] then
    IO.eprintln "Unexpected arguments"
    return 1

  forM (LinesOf.mk (← IO.getStdin)) fun line => do
    if line.any (·.isAlpha) then
      IO.print line

  return 0

test-data 文件包含：

Hello!
!!!!!
12345
abc123

Ok

调用保存在 ForMIO.lean 的这个程序，产生如下输出：

$ lean --run ForMIO.lean < test-data
Hello!
abc123
Ok

中止循环

使用 forM 时很难提前终止循环。 要编写一个在 AllLessThan 中遍历 Nat 直到 3 的函数，就需要一种中途停止循环的方法。 实现这一点的方法之一是使用 forM 和 OptionT 单子转换器。 第一步是定义 OptionT.exec，它会丢弃有关返回值和转换计算是否成功的信息：

def OptionT.exec [Applicative m] (action : OptionT m α) : m Unit :=
  action *> pure ()

然后，Alternative 的 OptionT 实例中的失败可以用来提前终止循环：

def countToThree (n : Nat) : IO Unit :=
  let nums : AllLessThan := ⟨n⟩
  OptionT.exec (forM nums fun i => do
    if i < 3 then failure else IO.println i)

快速测试表明，这一解决方案是可行的：

#eval countToThree 7

6
5
4
3

然而，这段代码并不容易阅读。 提前终止循环是一项常见的任务，Lean 提供了更多语法糖来简化这项任务。 同样的函数也可以写成下面这样：

def countToThree (n : Nat) : IO Unit := do
  let nums : AllLessThan := ⟨n⟩
  for i in nums do
    if i < 3 then break
    IO.println i

测试后发现，它用起来与之前的版本一样：

#eval countToThree 7

6
5
4
3

在撰写本文时，for ... in ... do ... 语法会解糖为使用一个名为 ForIn 的类型类，它是 ForM 的一个更为复杂的版本，可以跟踪状态和提前终止。 不过，我们计划重构 for 循环，使用更简单的 ForM，并在必要时插入单子转换器。 与此同时，我们还提供了一个适配器，可将 ForM 实例转换为 ForIn 实例，称为 ForM.forIn。 要启用基于 ForM 实例的 for 循环，请添加类似下面的内容，并适当替换 AllLessThan 和 Nat：

instance : ForIn m AllLessThan Nat where
  forIn := ForM.forIn

但请注意，这个适配器只适用于保持无约束单子的 ForM 实例，大多数实例都是如此。 这是因为适配器使用的是 StateT 和 ExceptT 而不是底层单子。

for 循环支持提前返回。 将提前返回的 do 块转换为异常单子转换器的使用，与之前使用 OptionT 来停止迭代一样，同样适用于 forM 循环。 这个版本的 List.find? 同时使用了这两种方法：

def List.find? (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if p x then return x
  failure

除了 break 以外，for 循环还支持 continue 以在迭代中跳过循环体的其余部分。 List.find? 的另一种表述方式（但容易引起混淆）是跳过不满足检查条件的元素：

def List.find? (p : α → Bool) (xs : List α) : Option α := do
  for x in xs do
    if not (p x) then continue
    return x
  failure

Range 是一个由起始数、终止数和步长组成的结构。 它们代表一个自然数序列，从起始数到终止数，每次增加一个步长。 Lean 有特殊的语法来构造范围，由方括号、数字和冒号组成，有四种类型。 必须始终提供终止数，而起始数和步长是可选的，默认值分别为 0 和 1：

请注意，起始数 包含 在范围内，而终止数不包含在范围内。 所有三个参数都是 Nat，这意味着范围不能向下计数 —— 当起始数大于或等于终止数时，范围中就不包含任何数字。

范围可与 for 循环一起使用，从范围中抽取数字。 该程序将偶数从 4 数到 8：

def fourToEight : IO Unit := do
  for i in [4:9:2] do
    IO.println i

运行它会输出：

4
6
8

最后，for 循环支持并行迭代多个集合，方法是用逗号分隔 in 子句。 当第一个集合中的元素用完时，循环就会停止，因此定义：

def parallelLoop := do
  for x in ["currant", "gooseberry", "rowan"], y in [4:8] do
    IO.println (x, y)

产生如下输出：

#eval parallelLoop

(currant, 4)
(gooseberry, 5)
(rowan, 6)

可变变量

除了提前 return、无 if 的 else 和 for 循环之外，Lean 还支持在 do 代码块中使用局部可变变量。 在后台，这些可变变量是通过使用 StateT 来实现的，而不是通过真正的可变变量来实现。 函数式编程再次被用来模拟命令式编程。

使用 let mut 而不是普通的 let 来引入局部可变变量。 定义 two 使用恒等单子 Id 来启用 do 语法，但不引入任何副作用，计数到 2：

def two : Nat := Id.run do
  let mut x := 0
  x := x + 1
  x := x + 1
  return x

这段代码等同于使用 StateT 添加两次 1 的定义：

def two : Nat :=
  let block : StateT Nat Id Nat := do
    modify (· + 1)
    modify (· + 1)
    return (← get)
  let (result, _finalState) := block 0
  result

局部可变变量与 do-标记的所有其他特性配合得很好，这些特性为单子转换器提供了方便的语法。 定义 three 计算一个三条目列表中的条目数：

def three : Nat := Id.run do
  let mut x := 0
  for _ in [1, 2, 3] do
    x := x + 1
  return x

同样，six 将条目添加到一个列表中：

def six : Nat := Id.run do
  let mut x := 0
  for y in [1, 2, 3] do
    x := x + y
  return x

List.count 计算列表中满足某些检查条件的条目的数量：

def List.count (p : α → Bool) (xs : List α) : Nat := Id.run do
  let mut found := 0
  for x in xs do
    if p x then found := found + 1
  return found

局部可变变量比局部显式使用 StateT 更方便，也更易于阅读。 然而，它们并不具备命令式语言中无限制的可变变量的全部功能。 特别是，它们只能在引入它们的 do 块中被修改。 例如，这意味着 for 循环不能被其他等价的递归辅助函数所替代。 该版本的 List.count：

def List.count (p : α → Bool) (xs : List α) : Nat := Id.run do
  let mut found := 0
  let rec go : List α → Id Unit
    | [] => pure ()
    | y :: ys => do
      if p y then found := found + 1
      go ys
  return found

在尝试修改 found 时产生以下错误：

`found` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `found`, consider using `let found` instead

这是因为递归函数是用恒等单子编写的，只有引入变量的 do 块的单子才会被 StateT 转换。

什么算作 do 区块？

do-标记的许多特性只适用于单个 do 块。 提前返回会终止当前代码块，可变变量只能在其定义的代码块中被改变。 要有效地使用它们，了解什么是 “同一代码块” 尤为重要。

一般来说，do 关键字后的缩进块算作一个块，其下的语句序列是该块的一部分。 独立代码块中的语句如果包含在另一个代码块中，则不被视为该独立代码块的一部分。 不过，关于哪些语句属于同一代码块的规则略有微妙，因此需要举例说明。 可以通过设置一个带有可变变量的程序来测试规则的精确性，并查看允许修改的地方。 这个程序中的允许可变的区域显然与可变变量位于同一快中：

example : Id Unit := do
  let mut x := 0
  x := x + 1

如果变化发生在使用 := 定义名称的 let 语句的一部分的 do 块中，则它不被视为该块的一部分：

example : Id Unit := do
  let mut x := 0
  let other := do
    x := x + 1
  other

`x` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `x`, consider using `let x` instead

但是，在 let 语句下，使用 ← 定义名称的 do 块被视为周围块的一部分。 以下程序是可以接受的：

example : Id Unit := do
  let mut x := 0
  let other ← do
    x := x + 1
  pure other

同样，作为函数参数出现的 do 块与周围的块无关。 以下程序并不合理：

example : Id Unit := do
  let mut x := 0
  let addFour (y : Id Nat) := Id.run y + 4
  addFour do
    x := 5

`x` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `x`, consider using `let x` instead

如果 do 关键字完全是多余的，那么它就不会引入一个新的程序块。 这个程序可以接受，等同于本节的第一个程序：

example : Id Unit := do
  let mut x := 0
  do x := x + 1

无论是否添加了多余的 do ，do 下的分支内容（例如由 match 或 if 引入的分支）都被视为周围程序块的一部分。 以下程序均可接受：

example : Id Unit := do
  let mut x := 0
  if x > 2 then
    x := x + 1

example : Id Unit := do
  let mut x := 0
  if x > 2 then do
    x := x + 1

example : Id Unit := do
  let mut x := 0
  match true with
  | true => x := x + 1
  | false => x := 17

example : Id Unit := do
  let mut x := 0
  match true with
  | true => do
    x := x + 1
  | false => do
    x := 17

同样，作为 for 和 unless 语法的一部分出现的 do 只是其语法的一部分，并不引入新的 do 块。 这些程序也被接受：

example : Id Unit := do
  let mut x := 0
  for y in [1:5] do
   x := x + y

example : Id Unit := do
  let mut x := 0
  unless 1 < 5 do
    x := x + 1

命令式还是函数式编程？

Lean 的 do-标记提供的命令式特性让许多程序与 Rust、Java 或 C# 等语言中的对应程序非常相似。 在将命令式算法转化为 Lean 的算法时，这种相似性非常方便，而且有些任务可以很自然地以命令式的方式进行思考。 单子和单子转换器的引入使得命令式程序可以用纯函数式语言编写，而作为单子（可能是局部转换的）专用语法的 do-标记则让函数式程序员获得了两全其美的结果：不变性提供了强大的推理原则，通过类型系统对可用作用进行了严格控制，同时还结合了语法和库，使得具有副作用的程序看起来熟悉且易于阅读。 单子和单子转换器让函数式编程与命令式编程成为一个视角问题。

练习

• 重写 doug 以使用 for 代替 doList 函数。是否还有其他机会使用本节介绍的功能来改进代码？如果有，请使用它们！