6.4. 更多 do 的特性🔗

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

6.4.1. 单分支 `if`🔗

在单子中工作时，一种常见的模式是只有当某些条件为真时才执行副作用。例如，countLetters 包含对元音或辅音的检查，而两者都不是的字母对状态没有影响。通过将 else 分支设置为 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 块的单子上添加一个局部转换器。

6.4.2. 提前返回🔗

标准库中有一个函数 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 块被转换为不使用提前返回的 do 块，方法是将其包裹在 runCatch 的使用中，并用 throw 替换提前返回：

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"。

6.4.3. 循环🔗

就像每个具有可变状态的程序都可以重写为将状态作为参数传递的程序一样，每个循环都可以重写为递归函数。从一个角度来看，List.find? 作为递归函数最为清晰。毕竟，它的定义反映了列表的结构：如果头部通过检查，则应将其返回；否则在尾部查找。当没有更多条目时，答案是 none。从另一个角度来看，List.find? 作为循环最为清晰。毕竟，程序按顺序查询条目，直到找到满意的条目，此时它终止。如果循环终止而没有返回，则答案是 none。

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

使用 ForM 可以对小于 5 的每个数字运行 IO.println：

4
3
2
1
0
#eval forM { num := 5 : AllLessThan } IO.println

仅在特定单子中工作的 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 包含：

                  File: test-dataHello!!!!!!12345abc123Ok

调用此程序（存储在 ForMIO.lean 中）会产生以下输出：

lean --run ForMIO.lean < test-data

Hello!
abc123
Ok

6.4.3.2. 停止迭代🔗

使用 ForM 很难提前终止循环。编写一个函数，在 AllLessThan 中的 Nat 上迭代，直到达到 3，这需要一种中途停止循环的方法。实现这一点的一种方法是将 ForM 与 OptionT 单子转换器一起使用。第一步是定义 OptionT.exec，它会丢弃有关返回值以及转换后的计算是否成功的信息：

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

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

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)

一个快速测试表明该解决方案有效：

6
5
4
3
#eval countToThree 7

然而，这段代码并不容易阅读。提前终止循环是一项常见任务，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

测试表明它的工作方式与之前的版本完全相同：

6
5
4
3
#eval countToThree 7

for ...in ...do ... 语法脱糖为使用名为 ForIn 的类型类，它是 ForM 的一个稍微复杂一点的版本，用于跟踪状态和提前终止。标准库提供了一个适配器，可以将 ForM 实例转换为 ForIn 实例，称为 ForM.forIn。要启用基于 ForM 实例的 for 循环，请添加类似以下内容，并适当替换 AllLessThan 和 Nat：

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

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

for 循环支持提前返回。将带有提前返回的 do 块转换为使用异常单子转换器，同样适用于 ForM 之下，就像前面使用 OptionT 停止迭代一样。此版本的 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

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

Expression	Start	Stop	Step	As List
`[:10]`	`0`	`10`	`1`	`[0, 1, 2, 3, 4, 5, 6, 7, 8, 9]`
`[2:10]`	`2`	`10`	`1`	`[2, 3, 4, 5, 6, 7, 8, 9]`
`[:10:3]`	`0`	`10`	`3`	`[0, 3, 6, 9]`
`[2:10:3]`	`2`	`10`	`3`	`[2, 5, 8]`

请注意，起始数字包含在范围内，而停止数字不包含。所有三个参数都是 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)

产生三行输出：

(currant, 4)
(gooseberry, 5)
(rowan, 6)
#eval parallelLoop

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

许多数据结构实现了 ForIn 类型类的增强版本，该版本向循环体添加了元素是从集合中提取的证据。可以通过在元素名称之前提供证据名称来使用这些证据。此函数打印数组的所有元素及其索引，并且编译器能够确定数组查找都是安全的，因为有证据 h：

def printArray [ToString α] (xs : Array α) : IO Unit := do
  for h : i in [0:xs.size] do
    IO.println s!"{i}:\t{xs[i]}"

在此示例中，h 是 i ∈ [0:xs.size] 的证据，并且检查 xs[i] 是否安全的策略能够将其转换为 i < xs.size 的证据。

6.4.4. 可变变量🔗

除了提前 return、无 else 的 if 和 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` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `found`, consider using `let found` insteadfound := found + 1
      go ys
  return found

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

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

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

6.4.5. 什么是 `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` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `x`, consider using `let x` insteadx := x + 1
  other

`x` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend 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 块独立于其周围的块。 -- The following program is not accepted:

以下程序不被接受：

example : Id Unit := do
  let mut x := 0
  let addFour (y : Id Nat) := Id.run y + 4
  addFour do
    `x` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `x`, consider using `let x` insteadx := 5

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

如果 do 关键字完全是多余的，那么它不会引入新的块。此程序被接受，并且等效于本节中的第一个程序：

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

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

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

6.4.6. 命令式还是函数式编程？🔗

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

6.4.7. 练习🔗

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