运行程序

运行 Lean 程序最简单的方法是使用 Lean 可执行文件的 --run 选项。创建一个名为 Hello.lean 的文件并输入以下内容：

def main : IO Unit := IO.println "Hello, world!"

然后，在命令行运行：

lean --run Hello.lean

该程序会在显示 Hello, world! 后退出。

问候程序的剖析

当使用 --run 选项调用 Lean 时，它会调用程序的 main 定义。对于不从命令行接受参数的程序，main 的类型应该是 IO Unit。这意味着 main 不是一个函数，因为它的类型中没有箭头（→）。 main 不是一个具有副作用的函数，而是由要执行的作用的描述组成。

如上一章所述，Unit 是最简单的归纳类型。它有一个名为 unit 的构造子，不接受任何参数。C 系的语言中有一个 void 函数的概念，它不返回任何值。在 Lean 中，所有函数都接受一个参数并返回一个值，而使用 Unit 类型可以表示没什么参数或返回值。如果 Bool 表示一个比特的信息，那么 Unit 就表示零比特的信息。

IO α 是一个程序的类型，当执行时，它要么抛出一个异常，要么返回一个类型为 α 的值。在执行期间，此程序可能会产生副作用。这些程序被称为 IO 活动（Action） 。 Lean 区分表达式的 求值（Evaluation）（严格遵循用变量值替换值和无副作用地归约子表达式的数学模型）和 IO 活动的 执行（Execution）（依赖于外部系统与世界交互）。 IO.println 是一个从字符串到 IO 活动的函数，当执行时，它将给定的字符串写入标准输出。由于此活动在发出字符串的过程中不会从环境中读取任何有趣的信息，因此 IO.println 的类型为 String → IO Unit。如果它确实要返回一些有趣的东西，那么将通过 Unit 类型以外的 IO 活动来表示。

函数式编程与副作用

Lean 的计算模型基于数学表达式的求值，其中变量会被赋予一个不会随时间改变的精确值。求值表达式的结果不会改变，再次求值相同的表达式会始终产生相同的结果。

另一方面，有用的程序必须与世界交互。既不进行输入也不进行输出的程序无法向用户询问数据、创建磁盘文件或打开网络连接。Lean 是用它自己编写的，而 Lean 编译器当然会读取文件、创建文件并与文本编辑器交互。当这些文件的内容可能随时间而改变时，在文件内容可能随时间改变的情况下，一种相同的表达式总是产生相同结果的语言，要如何编写可以从磁盘读取文件的程序呢？

只要换个角度思考副作用，即可解决这种明显的矛盾。想象一家出售咖啡和三明治的咖啡厅。这家咖啡厅有两个员工：一名厨师负责完成订单，一名柜员负责与顾客互动并下订单。厨师是个暴脾气的人，他真的不喜欢与外界有任何接触，但他非常擅长始终如一地提供咖啡厅著名的食物和饮料。然而，为了做到这一点，厨师需要安静，不能被谈话打扰。柜员很友好，但在厨房里完全没有能力。顾客与柜员互动，后者将所有实际烹饪委托给厨师。如果厨师对顾客有疑问，例如澄清过敏源，他们会给柜台工作人员发一张小纸条，柜员与顾客互动，并将一张写有结果的纸条传回给厨师。

在这个类比中，厨师是 Lean 语言。当收到订单时，厨师会忠实且始终如一地提供所要求的内容。柜员是与世界交互的外围运行时系统，它可以接受付款、分发食物并与顾客交谈。这两名员工共同承担了餐厅的所有职能，但他们的职责是分开的，每个人都执行自己最擅长的任务。就像让顾客远离可以让厨师专注于制作真正美味的咖啡和三明治一样， Lean 缺乏副作用可以让程序用作形式化数学证明的一部分。它还有助于程序员独立理解程序的各个部分，因为没有隐藏的状态改变会在组件之间造成微妙的耦合。厨师的笔记表示通过求值 Lean 表达式产生的 IO 活动，而柜员的回复是通过副作用传递回来的值。

这种副作用模型与 Lean 语言、编译器和运行时系统（Run-Time System，RTS）整体配合的工作方式非常相似。运行时系统中的原语（Primitive，用 C 语言编写）实现了所有基本副作用。在运行程序时， RTS 调用 main 活动，该活动将新的 IO 活动返回给 RTS 以执行。 RTS 执行这些活动，委托给用户的 Lean 代码来执行计算。从 Lean 的内部角度来看，程序没有副作用，而 IO 活动只是要执行的任务的描述。从程序用户的外部角度来看，存在一层副作用，它创建了一个与程序核心逻辑交互的接口。

现实世界的函数式编程

考虑 Lean 中副作用的另一种方式，就是将 IO 活动看做一个函数，它将整个世界作为参数输入，并返回一个值和一个新的世界。在这种情况下，从标准输入读取一行文本是一个 纯（Pure） 函数，因为每次都提供了一个不同的世界作为参数。向标准输出写入一行文本也是一个纯函数，因为函数返回的世界与它最初的世界不同。程序确实需要小心，不要重复使用世界，也不要没能返回一个新世界——毕竟，这将相当于时间旅行或者世界末日。谨小慎微的抽象边界可以使这种编程风格变得安全。如果每个原语 IO 活动都接受一个世界并返回一个新世界，并且它们只能与保持这种不变性的工具结合使用，那么问题就不会发生。

当然，这种模型无法真正实现，毕竟整个世界无法变成 Lean 的值放入内存中。然而，可以实现一个此模型的变体，它带有代表世界的抽象标识。当程序启动时，它会提供一个世界标识。然后将此标识传递给 IO 原语，之后它们的返回标识同样地传递到下一步。在程序结束时，标识将返回给操作系统。

这种副作用模型很好地描述了 IO 活动作为 RTS 要执行的任务描述是如何在 Lean 内部表示的。用于转换现实世界的实际函数隐藏在抽象屏障之后。但实际的程序通常不只有一个作用，而是由一系列作用组成。为了使程序能够使用多个作用，Lean 中有一个称为 do-记法的子语言，它能够将这些原语 IO 活动安全地组合成一个更大、更有用的程序。

组合 `IO` 活动

大多数有用的程序除了产生输出外还要接受输入。此外，它们可以根据输入做出决策，将输入数据用作计算的一部分。以下程序名为 HelloName.lean，它向用户询问他们的姓名，然后向他们问好：

def main : IO Unit := 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}!"

在此程序中，main 活动由一个 do 代码块组成。此块包含一系列的 语句（Statement），它们既可以是局部变量（使用 let 引入），也可以是要执行的活动。正如 SQL 可以被认为是与数据库交互的专用语言一样，do 语法可以被认为是 Lean 中的一个专用子语言，专门用于建模命令式程序。使用 do 块构建的 IO 活动通过按顺序执行语句来执行。

此程序可以与之前的程序一样的方式运行：

lean --run HelloName.lean

如果用户回应 David，则与程序交互的会话会读取回应：

How would you like to be addressed?
David
Hello, David!

它的类型签名与 Hello.lean 的类型签名一样：

def main : IO Unit := do

唯一的区别是它以关键字 do 结尾，该关键字会执行一系列命令。关键字 do 后面的每一行缩进都是同一系列命令的一部分。

前两行，读取：

  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

它们分别通过执行库中的活动 IO.getStdin 和 IO.getStdout 来检索 stdin 和 stdout 的勾柄（Handle）。在 do 块中，let 的含义与在普通表达式中略有不同。通常，let 中的局部定义只能在一个表达式中使用，该表达式紧跟在局部定义之后。在 do 块中，由 let 引入的局部绑定在 do 块其余部分的所有语句中都可用，而不仅仅是下一个语句。此外，let 通常使用 := 将所定义的名称与其定义关联起来，而 do 中的一些 let 绑定则使用向左箭头（← 或 <-）代替。使用箭头表示表达式的值是一个 IO 活动，该活动应该被执行，活动的结果保存在局部变量中。换句话说，如果箭头右侧的表达式的类型为 IO α，那么该变量在 do 块的其余部分中的类型为 α。 IO.getStdin 和 IO.getStdout 是 IO 活动，以便允许在程序中局部覆盖 stdin 和 stdout，这很方便。如果它们是像 C 中那样的全局变量，那么将不存在有意义的方法来覆盖它们，但是 IO 活动每次执行时都可以返回不同的值。

do 块的下一部分负责询问用户姓名：

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace

第一行将问题写入 stdout，第二行从 stdin 请求输入，第三行从输入行中删除尾部的换行符（以及任何其他尾部空格）。name 的定义使用 := 而非 ←，因为 String.dropRightWhile 是作用于字符串的普通函数，而非 IO 活动。

最后，程序中的最后一行是：

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

它使用字符串插值将提供的名称插入到问候字符串中，并将结果写入到 stdout。

Lean 函数式编程

运行程序

问候程序的剖析

函数式编程与副作用

现实世界的函数式编程

组合 IO 活动

组合 `IO` 活动