逐步执行

do 块可以逐行执行。从上一节的程序开始：

  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

标准 IO

第一行是 let stdin ← IO.getStdin，其余部分是：

  let stdout ← IO.getStdout
  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

要执行使用 ← 的 let 语句，首先求值箭头右侧的表达式（在本例中为 IO.getStdIn）。因为该表达式只是一个变量，所以查找它的值。结果值是一个内置的 IO 原语活动。下一步是执行此 IO 活动，结果是一个表示标准输入流的值，其类型为 IO.FS.Stream。然后将标准输入与箭头左侧的名称（此处为 stdin）关联，以用于 do 块的其余部分。"

执行第二行 let stdout ← IO.getStdout 的过程类似。首先，求值表达式 IO.getStdout，得到一个 IO 活动，该活动将返回标准输出。接下来，执行此活动，实际返回标准输出。最后，将此值与 do 块的其余部分关联起来，并命名为 stdout。"

提问

现在已经有了 stdin 和 stdout，该代码块的其余部分包括一个问题和一个答案：

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

该代码块中的第一个语句 stdout.putStrLn "How would you like to be addressed?" 由一个表达式组成。要执行一个表达式，首先要对其进行求值。在这种情况下，IO.FS.Stream.putStrLn 的类型为 IO.FS.Stream → String → IO Unit。这意味着它是一个接受流和字符串并返回 IO 活动的函数。该表达式使用访问器记法进行函数调用。此函数应用于两个参数：标准输出流和字符串。表达式的值为一个 IO 活动，该活动将字符串和换行符写入输出流。得到此值后，下一步是执行它，这会导致字符串和换行符写入到 stdout。仅由表达式组成的语句不会引入任何新变量。

下一条语句是 let input ← stdin.getLine。 IO.FS.Stream.getLine 的类型为 IO.FS.Stream → IO String，这意味着它是一个从流到 IO 活动的函数，该函数将返回一个字符串。同样，这也是访问器表示法的示例。此 IO 活动被执行时，程序会等待用户键入一行完整的输入。假设用户输入了「David」，则结果行（「David\n」）会与 input 关联，其中转义序列 \n 表示换行符。

  let name := input.dropRightWhile Char.isWhitespace
  stdout.putStrLn s!"Hello, {name}!"

下一行 let name := input.dropRightWhile Char.isWhitespace 是一个 let 语句。与本程序中的其他 let 语句不同，它使用 := 而不是 ←。这意味着将计算表达式，但结果值不必是 IO 活动，并且不会执行。在这种情况下，String.dropRightWhile 接受一个字符串和一个字符的谓词，并返回一个新字符串，其中字符串末尾满足谓词的所有字符都会被删除。例如，

#eval "Hello!!!".dropRightWhile (· == '!')

会产生

"Hello"

而

#eval "Hello...   ".dropRightWhile (fun c => not (c.isAlphanum))

会产生

"Hello"

其中所有非字母数字的字符均已从字符串的右侧删除。在程序的当前行中，空格符（包括换行符）从输入字符串的右侧删除，得到「David」，它在代码块的剩余部分与 name 关联。

向用户问好

do 块中剩余要执行的只有一条语句：

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

传递给 putStrLn 的字符串参数通过字符串插值构建，生成字符串 "Hello, David!"。由于此语句是一个表达式，因此它被求值以生成一个 IO 活动，该活动会将此字符串后加上换行符打印到标准输出。表达式求值后，将执行生成的 IO 活动，从而生成问候语。

`IO` 活动作为值

在上面的描述中，可能很难看出为什么需要区分求值表达式和执行 IO 活动。毕竟，每个活动在生成后都会立即执行。为什么不干脆在求值期间执行副作用，就像在其他语言中所做的那样呢？

答案有两个。首先，将求值与执行分开意味着程序必须明确说明哪些函数可以产生副作用。由于没有副作用的程序部分更适合数学推理，无论是在程序员的头脑中还是使用 Lean 的形式化证明工具，这种分离可以更容易地避免错误。其次，并非所有 IO 活动都需要在它们产生时执行。在不执行活动的情况下提及活动的能力能够将普通函数用作控制结构。

例如，函数 twice 将 IO 活动作为其参数，返回一个新的活动，该活动将第一个活动执行两次。

def twice (action : IO Unit) : IO Unit := do
  action
  action

例如，执行

twice (IO.println "shy")

会打印

shy
shy

这可以推广为一个通用函数，它可以运行底层活动任意次：

def nTimes (action : IO Unit) : Nat → IO Unit
  | 0 => pure ()
  | n + 1 => do
    action
    nTimes action n

在 Nat.zero 的基本情况下，结果是 pure ()。函数 pure 创建一个没有副作用的 IO 活动，但返回 pure 的参数，在本例中是 Unit 的构造子。作为不执行任何活动且不返回任何有趣内容的活动， pure () 既非常无聊又非常有用。在递归步骤中，do 块用于创建一个活动，该活动首先执行 action，然后执行递归调用的结果。执行 nTimes (IO.println "Hello") 3 会输出以下内容：

Hello
Hello
Hello

除了将函数用作控制结构体之外，IO 活动是一等值的事实意味着它们可以保存在数据结构中供以后执行。例如，函数 countdown 接受一个 Nat 并返回一个未执行的 IO 活动列表，每个 Nat 对应一个：

def countdown : Nat → List (IO Unit)
  | 0 => [IO.println "Blast off!"]
  | n + 1 => IO.println s!"{n + 1}" :: countdown n

此函数没有副作用，并且不打印任何内容。例如，它可以应用于一个参数，并且可以检查结果活动列表的长度：

def from5 : List (IO Unit) := countdown 5

此列表包含六个元素（每个数字一个，外加一个对应零的 "Blast off!" 活动）：

#eval from5.length

函数 runActions 接受一个活动列表，并构造一个按顺序运行所有活动的单个活动：

def runActions : List (IO Unit) → IO Unit
  | [] => pure ()
  | act :: actions => do
    act
    runActions actions

其结构本质上与 nTimes 相同，只是没有一个对每个 Nat.succ 执行的活动，而是在每个 List.cons 下的活动将被执行。类似地，runActions 本身不会运行这些活动。而是创建一个将要运行这些活动的新活动，并且该活动必须放置在将作为 main 的一部分执行的位置：

def main : IO Unit := runActions from5

运行此程序会产生以下输出：

5
4
3
2
1
Blast off!

当运行此程序时会发生什么？第一步是求值 main，它产生如下输出：

main
===>
runActions from5
===>
runActions (countdown 5)
===>
runActions
  [IO.println "5",
   IO.println "4",
   IO.println "3",
   IO.println "2",
   IO.println "1",
   IO.println "Blast off!"]
===>
do IO.println "5"
   IO.println "4"
   IO.println "3"
   IO.println "2"
   IO.println "1"
   IO.println "Blast off!"
   pure ()

产生的 IO 活动是一个 do 块。然后逐个执行 do 块的每个步骤，产生预期的输出。最后一步 pure () 没有产生任何作用，它的存在只是因为 runActions 的定义需要一个基本情况。

练习

在纸上逐步执行以下程序：

def main : IO Unit := do
  let englishGreeting := IO.println "Hello!"
  IO.println "Bonjour!"
  englishGreeting

在逐步执行程序时，要察觉到何时正在求值表达式，以及何时正在执行 IO 活动。当执行 IO 活动产生副作用时，请将其写下来。在纸上执行完毕后，使用 Lean 运行程序，并仔细检查你对副作用的预测是否正确。

Lean 函数式编程

逐步执行

标准 IO

提问

向用户问好

IO 活动作为值

练习

`IO` 活动作为值