翻译-FPIL-01-了解 Lean

按照惯例，一门编程语言的介绍通常都始于 编译并运行一个能在控制台上显示 Hello, world! 的程序。 这个简单的程序用于确保 语言工具已被正确安装，以及 程序员能够运行已编译的代码。

然而编程自 20 世纪 70 年代以来早已改头换面： 如今的编译器通常被集成到了文本编辑器中， 编程环境会在编写程序时提供反馈； Lean 也不例外，它实现了 语言服务器协议 Language Server Protocol，LSP 的扩展版本，使得它 能够与文本编辑器通信，并 在用户键入时提供反馈。

像 Python、Haskell、JavaScript 等这样风格各异的语言 都支持 读取-求值-打印-循环 Read-Eval-Print-Loop，REPL（又称 交互式顶层环境 Interactive Top-Level、 浏览器控制台 Browser Console）， 于其中可以输入表达式或语句， 如此语言便会计算并显示用户输入的结果；然而 Lean 还将这些特性集成进了与编辑器的交互之中， 其提供的命令能让文本编辑器将对程序的反馈集成到程序文本之中。 本章简要介绍了在编辑器中与 Lean 的交互，至于 如何在批处理模式下以传统的命令行方式使用 Lean 请参考章节 Hello, World!。

如果你 能在编辑器中使用 Lean、 输入书中的每个示例并 运行它们， 那真是再好不过了。请尽情地尝试这些案例，并看看会发生什么。

1.1. 表达式求值 Evaluating Expressions

作为学习 Lean 的程序员，最重要的是理解求值的工作原理。 表达式求值是获取表达式值的过程，就像算术运算那样。例如， $15 − 6$ 的值为 $99$， $2 \times (3 + 1)$ 的值为 $8$。 要想得到第二个表达式的值， 首先需要将 $3+1$ 替换为 $4$ 以得到 $2\times 4$， 而它本身又可被归约为 $8$。 数学表达式有时也会包含变量，在知道 $x$ 的值之前 $x + 1$ 的值是无法被计算的。在 Lean 中， 程序首先得是表达式，因此计算的首要理解方式便是求值表达式。

大部分编程语言都是命令式 Imperative 的， 当中的程序都是一串串的语句， 这些语句会被按顺序执行以得到程序运行结果。 程序可以访问可变内存，因此变量引用的值会随时间而改变。 除了状态可变外，程序还可能产生其他副作用，例如 删除文件、 建立传出的网络连接、 抛出或捕获异常以及从数据库读取数据，等等。 “副作用 Side Effect”本质上是一个统称， 用于描述程序运行过程中可能发生的某些事情， 这些事情不遵循数学表达式求值的模型。

然而 Lean 中程序的工作方式与数学表达式相似， 变量一旦被赋值就无法再被重新赋值。 表达式求值也无法产生副作用， 如果两个表达式的值相同， 那么用一个表达式替换另一个并不会导致不同的计算结果。 这并非在说 Lean 无法向控制台写入 Hello, world!， 而是说在以求值表达式的方式使用 Lean 的体验中，IO 并非其核心部分。正因如此， 本章只负责介绍如何使用 Lean 交互地求值表达式； 至于如何编写、编译并运行 Hello, world! 程序， 请参考下一章。

要想让 Lean 对一个表达式求值， 请在编辑器中对应的表达式前加上 #eval，这样它才会返回结果。 通常求值结果可以通过将光标或鼠标指针悬浮在 #eval 上查看。 比如下述代码输出的值为 3：

#eval 1 + 2
-- 3

Lean 遵循一般的算术运算符优先级和结合性规则， 因此下述代码会输出值 11 而非 15：

#eval 1 + 2 * 5
-- 11

虽然普通数学记法和大多数编程语言 在表示函数应用的时候都用到了括号（例如 f(x)）， 但是在 Lean 中 您只需将实参写在函数后边即可（例如 f x）。 函数应用是非常常见的操作， 有必要保持简洁。与其编写

#eval String.append("Hello, ", "Lean!")

计算 "Hello, Lean"，不如编写

#eval String.append "Hello, " "Lean"
-- "Hello, Lean"

当中函数的两个实参只是简单地写在一起，并以空格分隔。

正如括号在算术运算表达式 (1 + 2) * 5 中是必不可少的， 在函数实参需要依赖其他函数的调用来计算时它们也是必不可少的； 例如在下述代码中括号就是必须的：

#eval String.append "great " (String.append "oak " "tree")
-- "great oak tree"

否则第二层的 String.append 就会被解释为 第一层函数的第二个实参，而非 一个接收 oak 和 tree 作为实参的函数。 内层的 String.append 的调用必须被先求值， 然后才可以被追加到 great 后面， 从而输出最终的值 great oak tree。

命令式语言通常有两种“条件”： 一种是根据布尔值确定哪些指令要被执行的条件语句 Statement， 另一种则是根据布尔值确定两个表达式中哪个要被计算的条件表达式 Statement。例如 在 C 和 C++ 中， 条件语句使用 if 和 else 书写，而 条件表达式使用三元运算符 ? 和 : 书写。 在 Python 中， 条件语句以 if 开头，而 条件表达式则将 if 放在中间。 由于 Lean 是一种面向表达式的函数式语言，因此 没有条件语句， 只有条件表达式。 条件表达式使用 if、then、else 书写。例如，

String.append "it is " (if 1 > 2 then "yes" else "no")

首先被求值为

String.append "it is " (if false then "yes" else "no")

进而被求值为

String.append "it is " "no"

最终被求值为

"it is no"

简洁起见，像这样的一系列求值步骤有时会通过箭头串联：

String.append "it is " (if 1 > 2 then "yes" else "no")
-- ==>
String.append "it is " (if false then "yes" else "no")
-- ==>
String.append "it is " "no"
-- ==>
"it is no"

1.1.1. 可能遇到的信息 Messages You May Meet

函数应用表达式实参缺省会导致求值报错。比如

#eval String.append "it is "
-- could not synthesize a 
--   `ToExpr`, `Repr`, or `ToString` instance 
-- for type
--   String → String

之所以出现这个报错是因为 Lean 函数在部分应用于某些实参后会返回一个新的函数， 后者等待接收剩余的实参；而 Lean 无法将函数直接显示给用户，进而导致报错。

1.1.2. 练习 Exercises

下述表达式的求值结果是什么呢？ 请先动脑计算， 然后再用 Lean 验证你的答案：

• #eval 42 + 19

• #eval String.append "A" (String.append "B" "C")

• String.append (String.append "A" "B") "C"

• #eval if 3 == 3 then 5 else 7

• #eval if 3 == 4 then "equal" else "not equal"

1.2. 类型 Evaluating Expressions

类型根据自己可计算的值对程序进行分类。 类型在程序中扮演着多种角色：它们

1. 允许编译器对值的内存表示做出决策。

2. 帮助程序员向他人传达他们的意图， 充当轻量级的函数输入输出的规范。 编译器会确保程序遵守此规范。

3. 预防各种潜在的错误 （比如将数字拼接到字符串上） 以减少程序所需的测试次数。

4. 帮助 Lean 编译器自动化生成辅助代码 以节省样板代码。

Lean 的类型系统异常富有表现力，其可以 编码 强规范（如“该排序函数可以返回实参的排列”）以及 灵活规范（如“该函数可以返回不同的类型，具体情况由实参决定）”，甚至还可以 被用作证明数学定理的完整逻辑。 然而这种尖端表达能力并不会使简单类型变得形同虚设， 相反，理解后者是使用这些高级功能的前提。

Lean 中 每个程序都必须拥有一个类型， 每个表达式在被求值前都必须有一个类型。 尽管对于目前为止的所有示例 Lean 都能自行推断类型， 但是仍然有需要提供类型的情况。 这是通过在括号内使用冒号运算符来完成的：

#eval (1 + 2 : Nat)
-- 3

其中的 Nat 是自然数类型， 它们是任意精度的无符号整数。 在 Lean 中，Nat 是非负整数字面量的默认类型。 但此默认类型并非总是最佳选择： 在 C 语言中，当减法运算结果小于零时， 无符号整数会下溢到最大可表示数；而 在 Lean 中 Nat 却可以表示任意大的无符号数， 也就没有最大数可以下溢。 因此 Nat 上的减法运算便会返回 zero， 而答案实际应为负数。例如：

#eval (1 - 2 : Nat)
-- 0

求值结果为 0 而非 -1。 要想使用可以求值为负数的类型， 请直接提供它：

#eval (1 - 2 : Int)
-- -1

有这个类型注解后 求值结果就是 -1 了，符合预期。

若只想检查表达式的类型而非求值， 则请用 #check 代替 #eval， 比如

#check (1 - 2 : Int)
-- 1 - 2 : Int

会报告 1 - 2 : Int 而不会执行减法计算。

当程序无法获得类型时 #check 和 #eval 都会报错。 例如下述代码便会导致报错：

#check String.append ["hello", " "] "world"
-- Application type mismatch: The argument
--   ["hello", " "]
-- has type
--   List String
-- but is expected to have type
--   String
-- in the application
--   String.append ["hello", " "]

因为 String.append 期待第一个实参的类型是字符串， 而实际的类型却是字符串列表。

1.3. 函数以及常量声明 Functions and Definitions

在 Lean 中，常量声明是通过 def 关键字实现的。例如， 想通过声明常量 hello 来调用字符串字面量 "Hello" 就可以这么写：

def hello := "Hello"

Lean 中新常量的声明用的是 := 而非 =，因为 = 已被用于描述现有表达式之间的等号关系， 使用两个不同的运算符可以避免混淆。

在 hello 的声明中，表达式 "Hello" 足够简单以至于 Lean 能自动推断常量类型； 然而大多数常量声明并不是那么简单， 因此通常需要补充类型注解。 只需在待声明常量名后添加冒号即可：

def lean : String := "Lean"

常量声明完成了，也就可被调用了；因此

#eval String.append hello (String.append " " lean)
-- "Hello Lean"

将输出 "Hello Lean"。

在 Lean 中，常量只有在被声明之后才可被调用。

大多数语言的函数常量声明语法都有别于其他值，例如 Python 里 函数常量声明以 def 关键字开头，而 其他常量声明则用的是等号；而 Lean 里 函数常量声明则与其他任何常量一样， 都是以同一个关键字 def 关键字实现的。尽管如此， 像 hello 这样的常量声明所引入的名称 都会直接指向对应的值，而 不会指向一个无参函数（即每次调用都返回相同结果的函数）

1.3.1. 函数常量声明 Defining Functions

Lean 中有多种声明函数常量的方法，最简单的一种就是 在返回类型前声明函数形参，各个形参用空格分隔。 比如一个将实参加 1 的函数就可以写成如下：

def add1 (n : Nat) : Nat := n + 1

使用 #eval 测试此函数便会得到 8，符合预期：

#eval add1 7
-- 8

正如 多参函数应用需要在每个实参间添加空格， 多参函数构造需要在每个形参（可能附带类型注解）间添加空格。 函数 maximum 的返回结果为两个实参中的最大者，它 接收 n 和 k 两个 Nat 并 返回一个 Nat。

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k 
  then k
  else n

类似地，函数 spaceBetween 用空格连接两个字符串：

def spaceBetween (before : String) (after : String) : String :=
  String.append before (String.append " " after)

在向 maximum 这样的已被声明的函数常量提供实参时， 其结果会首先用提供的值替换函数体中对应的参数名称， 然后对产生的函数体求值。例如：

maximum (5 + 8) (2 * 7)
-- ==>
maximum 13 14
-- ==>
if 13 < 14 then 14 else 13
-- ==>
14

任何能够被求值为自然数、整数和字符串的表达式都 拥有能够表明自身属性的类型（分别为 Nat、Int、String）。 函数亦是如此， 接收一个 Nat 并返回一个 Bool 的函数类型为 Nat → Bool，而 接收两个 Nat 并返回一个 Nat 的函数类型为 Nat → Nat → Nat。

特别地，当函数常量名称直接与 #check 一起使用时， Lean 会返回函数常量的类型签名。 输入 #check add1 会得到 add1 (n : Nat) : Nat。 然而我们可以通过将函数名称写在括号中来“欺骗” Lean， 这会导致函数常量被视为普通表达式；比如 #check (add1) 会得到 add1 : Nat → Nat，而 #check (maximum) 会得到 maximum : Nat → Nat → Nat。 这个箭头也可以用 ASCII 字符串 -> 来替代， 因此前面的函数类型就可以分别写成 example : Nat -> Nat := add1 和 example : Nat -> Nat -> Nat := maximum。

Lean 里面的所有函数其实都只接收一个实参： 像 maximum 这样看似接收多个实参的函数本质上是一个高阶函数，其 接收第一个实参，然后再返回一个新函数；后者 接收第二个实参。 这样的过程会一直持续，直至不再需要新实参为止。 我们可以通过向一个多参数函数提供一个实参来观察这个现象： #check maximum 3 会得到 maximum 3 : Nat → Nat，而 #check spaceBetween "Hello " 会得到 spaceBetween "Hello " : String → String。 通过返回函数的函数来实现多参函数的方法称作柯里化 Currying， 以数学家 Haskell Curry 命名。 函数箭头是右结合的，这意味着 Nat → Nat → Nat 应该写成如下带括号的形式 Nat → (Nat → Nat)。

1.3.1.1. 练习 Exercises

• 声明一个函数常量 joinStringsWith， 类型为 String → String → String → String： 它返回一个字符串，这是通过将第一个实参 放在第二、三个实参之间来完成的。 joinStringsWith ", " "one" "and another" 应该被求值为 "one, and another"。

  joinStringsWith ": " 的类型是什么？ 用 Lean 检查你的答案。

• 声明一个函数常量 volume， 类型为 Nat → Nat → Nat → Nat， 它通过给定的高度、宽度和深度来计算长方体的体积。

1.3.2. 类型常量声明 Defining Types

大多数带类型系统的编程语言都有某种声明类型常量别名的方法，比如 C 语言里的 typedef； 然而类型在 Lean 中是该语言的一等公民，它们和其他东西一样也不过是表达式而已。 这意味着常量声明也可以引用类型，正如它们可以引用其他值一样。

比方说，如果 String 太长，那么我们就可以声明一个缩写 Str：

1

def Str : Type := String

然后就可以在常量声明中使用 Str 而非 String：

def aStr : Str := "This is a string."

这之所以能奏效是因为类型遵循 Lean 其他的规则： 类型也是表达式，表达式中被声明的常量皆可被替换为其对应声明的具体内容。 由于 Str 的定义为 String，因此 aStr 的声明是有意义的。

1.3.2.1. 你可能遇到的信息 Messages You May Meet

由于 Lean 支持整数字面量的重载， 尝试使用类型常量声明变得更加复杂。 如果 Nat 太短，那么就可以定义一个 更长的名称 NaturalNumber：

def NaturalNumber : Type := Nat

然而，使用 NaturalNumber 而非 Nat 作为被调用的类型常量并不会产生预期的效果。比方说 下面的常量声明就会导致报错：

def thirtyEight : NaturalNumber := 38
-- failed to synthesize
--   OfNat NaturalNumber 38
-- numerals are polymorphic in Lean, 
-- but the numeral `38` cannot be used in a context 
-- where the expected type is
--   NaturalNumber
-- due to the absence of the instance above
-- 
-- Hint: Additional diagnostic information may be available 
-- using the `set_option diagnostics true` command.

此错误发生的原因是因为 Lean 允许数字字面量被重载 Overloaded。 如果这么做有意义，那么自然数字面量就可以被用于新类型， 就好像这些类型是系统内置的一样。 这是 Lean 让数学表示变得更便捷的核心使命之一， 并且不同的数学分支会将数字表示法用于不同的场景。 然而允许这种重载的特定功能在寻找重载规则前是不会预先 将所有已声明的名称替换为其底层的具体定义（即不会提前展开定义）的， 这就是导致上述报错的原因。

解决这一限制的一种办法是在常量声明的右侧提供类型注解 Nat 从而强制使数字 38 使用 Nat 的重载规则：

def thirtyEight : NaturalNumber := (38 : Nat)

上述声明依然是类型正确的，因为根据定义可知 NaturalNumber 与 Nat 是相同的类型。

另一种解决方案是为 NaturalNumber 定义一个重载， 其运作方式与 Nat 的重载等效。不过这需要 Lean 更高级的功能。

最后，使用 abbrev 而非 def 来为 Nat 创建新名称 可以允许重载解析使用其定义来替换名称。 由 abbrev 编写的定义总会被展开。 比如下面的代码就可以正常运行：

abbrev N : Type := Nat

def thirtyNine : N := 39

在背后， 某些声明会在重载解析期间被内部标记为可展开的，而 其他的则不会被标记。 待展开的常量称作是可归约的 Reducible。 可归约性的控制对于 Lean 的扩展至关重要： 完全展开所有声明可能会产生非常大的类型， 这些类型会让机器处理变慢，也让用户难以理解。 由 abbrev 生成的定义都会被标记为可归约的。

1.4. 结构 Structures

编写程序的第一步通常是识别问题域， 然后再为它们找到合适的代码表示。 有时一个域概念是其他更简单概念的集合。在此情况下， 将这些更简单的组件组合到一个单独的"包"中会很方便， 然后就可以为其赋予有意义的名称。在 Lean 中，这是通过 结构 Structure 来完成的，它类似于 C 或 Rust 中的 struct 和 C# 中的 record。

声明结构会向 Lean 引入一个全新的类型， 该类型无法被归约为任何其他类型。这很有用， 因为多个结构可能表示不同的概念， 但却包含相同的数据。例如， 一个点可以用笛卡尔坐标或极坐标表示， 每个坐标都是一对浮点数。声明单独的结构 可以防止 API 客户端将一个结构与另一个结构混淆。

Lean 的浮点数类型称为 Float， 浮点数以通常的记法编写。

#check 1.2
-- 1.2 : Float
#check -454.2123215
-- -454.2123215 : Float
#check 0.0
-- 0.0 : Float

当浮点数以小数点形式编写时，Lean 会将类型推断为 Float。 如果没有小数点，那么就需要进行类型注解补充：

#check 0
-- 0 : Nat
#check (0 : Float)
-- 0 : Float

二维笛卡尔坐标点是一个具有两个 Float 字段的结构， 分别称为 x 和 y。这是通过关键字 structure 声明的。

structure Point where
  x : Float
  y : Float

在此声明之后 Point 便构成一个新的结构类型。 构建结构类型下的项的典型方法是在花括号内为其所有字段提供值。 笛卡尔平面的原点是 x 和 y 都为零的地方：

def origin : Point := { 
  x := 0.0, 
  y := 0.0 
}

#eval origin 的结果看起来很像 origin 的定义：

#eval origin
-- { x := 0.000000, y := 0.000000 }

由于结构存在的目的是为了 将数据集合"打包"、 为其命名并 将其作为单个单元处理， 因此能够提取结构的各个字段也很重要。 这是通过点符号实现的，就像在 C、Python、Rust、JavaScript 中那样：

#eval origin.x
-- 0.000000
#eval origin.y
-- 0.000000

这可以用来构造那些接收结构作为实参的函数， 比如点的加法需要对坐标的每个分量的值进行求和。 下述代码的输出结果就应该是 { x := -6.500000, y := 32.200000 }：

#eval addPoints { 
  x := 1.5, 
  y := 32 
} { 
  x := -8, 
  y := 0.2 
}
-- { x := -6.500000, y := 32.200000 }

函数本身接收两个 Point 作为实参， 分别称作是 p1 和 p2。返回结果基于 p1、p2 各自的 x、y 字段：

def addPoints (p1 : Point) (p2 : Point) : Point := { 
  x := p1.x + p2.x, 
  y := p1.y + p2.y 
}

类似地，两点之间的距离——也就是它们 x、y 字段差值的平方和的开平方， 就可以写成如下代码：

def distance (p1 : Point) (p2 : Point) : Float :=
  Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))

比如 $(1,2)$ 和 $(5, -1)$ 之间的距离是 $5$：

#eval distance { 
  x := 1.0, 
  y := 2.0 
} { 
  x := 5.0, 
  y := -1.0 
}
-- 5.000000

多个结构可能具有相同名称的字段。 三维点数据类型可以共享字段 x、y 并使用相同的字段名实例化：

structure Point3D where
  x : Float
  y : Float
  z : Float

def origin3D : Point3D := { 
  x := 0.0, 
  y := 0.0, 
  z := 0.0
}

这意味着要使用花括号语法就必须知道结构的预期类型； 如果类型未知，那么 Lean 就无法实例化结构。例如，

#check { 
  x := 0.0, 
  y := 0.0 
}
-- invalid {...} notation, 
-- expected type is not known

通常可以通过类型注解补充来解决这种情况：

#check ({ 
  x := 0.0, 
  y := 0.0 
} : Point)
-- { x := 0.0, y := 0.0 } : Point

为了使程序更简洁，Lean 还允许在花括号内进行结构类型注解。

#check { 
  x := 0.0, 
  y := 0.0 
  : Point
}
-- { x := 0.0, y := 0.0 } : Point

1.4.1. 更新结构 Updating Structures

想象一个函数 zeroX：它将 Point 下的项中的 x 字段设置为 0。 在大多数编程语言的社区中， 这句话意味着 x 指向的内存位置会被新值覆盖。 然而 Lean 是一种函数式编程语言，在函数式编程语言社区中， 这种陈述几乎总是意味着一个新的 Point 将被分配：其中 字段 x 指向新值，而 其他所有字段则指向实参的原始值。 编写 zeroX 的其中一种方法是按字面意思遵循此描述，即 填写 x 的新值并手动传输 y：

def zeroX (p : Point) : Point :={ 
  x := 0, 
  y := p.y 
}

然而这种编程风格存在不少缺点： 首先， 如果向结构添加新字段， 那么代码中所有需要更新字段的位置都必须被修改，这会增加维护成本； 其次， 如果结构包含多个相同类型的字段， 那么复制粘贴代码可能导致字段内容有重复或被交换，会有风险。 最后， 代码会变得冗长且官僚化。

Lean 提供了一种方便的语法， 既可以替换结构常量中的某些字段， 又可以保持其他字段不变。 这是通过在结构构造时使用 with 关键字完成的。 未更改字段的来源出现在 with 之前， 新字段则出现在其后。 例如 zeroX 就可以只使用新的 x 值来编写：

def zeroX (p : Point) : Point :={ 
  p with x := 0 
}

请记住，此结构常量更新语法并不会修改现有值， 它创建的新值会与旧值共享某些字段。 给定点 fourAndThree，计算它， 然后使用 zeroX 计算它的更新， 最后再次计算它会产生原始值，便有：

def fourAndThree : Point :={ 
  x := 4.3, 
  y := 3.4 
}
#eval fourAndThree
-- { x := 4.300000, y := 3.400000 }
#eval zeroX fourAndThree
-- { x := 0.000000, y := 3.400000 }
#eval fourAndThree
-- { x := 4.300000, y := 3.400000 }

结构常量更新不修改原始结构的一个效果是 在从旧值计算新值的情况下推理会变得更容易： 所有对旧结构的引用将会继续引用新值中相同字段的值。

1.4.2. 幕后的原理 Behind the Scenes

每个结构都有一个构造器 Constructor。 在这里，术语“构造器”可能是混淆的罪魁祸首： 不同于 Java 或 Python 等语言中的构造器， Lean 中的构造器并非在数据类型初始化时运行的任意代码； 相反，构造器只负责 收集数据并 将其存储在新分配的数据结构中。 想要自己声明构造器来 预处理数据或 拒绝无效参数 在这里是不可能的。 这其实是“构造器”这个词在两种上下文中 具有不同但彼此相关的含义所导致的。

默认情况下，名为 S 的结构构造器 会被命名为 S.mk；其中 S 是命名空间限定符， mk 是构造器本身的名称。 除了使用花括号初始化语法外， 构造器也可以直接被拿去应用：

#check Point.mk 1.5 2.8
-- { x := 1.5, y := 2.8 } : Point

不过这通常不会被视作是良好的 Lean 代码风格， 甚至连 Lean 自己在返回反馈信息时 也会自动转换回标准结构初始化语法。

结构构造器为函数类型，也就意味着它们可以在任何 期待填入函数的地方使用。例如，Point.mk 是一个 接收两个 Float（分别为 x、y）并 返回一个新 Point 的函数：

#check (Point.mk)
-- Point.mk : Float → Float → Point

若想要覆盖结构构造器的默认名称，请在开头用两个冒号编写。 例如，要使用 Point.point 而非 Point.mk，请写：

structure Point where
  point ::
  x : Float
  y : Float

除了构造器外，Lean 还为结构的每个字段声明了访问器函数。 这些函数在结构对应的命名空间中与字段同名。比如 Point 就会有访问器函数 Point.x 和 Point.y：

#check (Point.x)
-- Point.x : Point → Float
#check (Point.y)
-- Point.y : Point → Float

正如花括号结构构造语法在背后 会被转换为对结构构造器的调用一样， 先前声明的 addPoints 中的 x 实际上也会被转换为对 x 访问器的调用；也就是说， #eval origin.x 和 #eval Point.x origin 都会输出 0.000000。

访问器点符号语法不仅可以用于结构字段，也 可以用于其他任何接收任意数量参数的函数。更一般地， 访问器记法具有形式 TARGET.f ARG1 ARG2 ...： 如果 TARGET 的类型为 T， 那么名为 T.f 的函数便会被调用， TARGET 将成为其最左边的类型为 T 的实参。 其通常是第一个实参，但也有例外。 ARG1 ARG2 ... 则作为其余参数按顺序提供。 比如 String.append 的调用就可以使用访问器记法， 尽管 String 结构并没有 append 字段：

#eval "one string".append " and another"
-- 等同于 String.append 
--  "one string"   -- TARGET
--  " and another" -- ARG1
-- "one string and another"

在此示例中 TARGET 表示 "one string" 而 ARG1 表示 " and another"。

函数 Point.modifyBoth（即在 Point 命名空间中声明的 modifyBoth） 会将接收的函数实参（对应 f）应用于 Point 中的两个字段：

def Point.modifyBoth (f : Float → Float) (p : Point) : Point :={ 
  x := f p.x, 
  y := f p.y 
}

即使 Point 参数在函数实参（对应 f）之后， 它也可以与点符号一起使用：

#eval fourAndThree.modifyBoth Float.floor
-- 等同于 Point.modifyBoth 
--  Float.floor    -- ARG1
--  fourAndThree   -- TARGET
-- { x := 4.000000, y := 3.000000 }

在此情况下 TARGET 表示 fourAndThree，而 ARG1 则是 Float.floor； 这是因为在访问器记法中 TARGET 是首个类型匹配的实参，而 其未必是函数的首个实参。

1.4.3. 练习 Exercises

• 声明一个结构 RectangularPrism， 包含长方体的高度、宽度和深度，每个都是 Float。 RectangularPrism 的声明引入了哪些名称？

• 声明一个函数常量 volume : RectangularPrism → Float 以计算长方体的体积。

• 声明一个结构 Segment，通过其端点表示线段， 并声明一个函数常量 length : Segment → Float 来计算线段的长度。 Segment 最多应该有两个字段。

• 以下 Hamster 和 Book 的声明 引入了哪些名称？它们的类型是什么？

  1 2 3 4 5 6 7 8 9

  structure Hamster where name : String fluffy : Bool structure Book where makeBook :: title : String author : String price : Float

1.5. 数据类型和模式匹配 Data Types and Patterns

结构使得 多个独立的数据片段能够被组合成一个连贯的整体， 并由一个全新的类型表示。 如结构这样将值组合在一起的类型称作是积类型 Product Types。 然而不少域的概念无法自然地被表示为结构，比方说： 应用程序可能需要跟踪用户权限，其中 一部分人是文档所有者， 另一部分有编辑文档的权限，而 其余的只有阅读文档的权限；再比如 计算器支持一系列的二元运算，包括 加法、减法和乘法。 可见结构不具备编码多种选择的简单方法。

类似地，尽管结构是跟踪固定字段集的绝佳方法， 但是许多应用程序依赖的数据可能包含任意数量的元素。 大多数经典数据结构都具有递归结构，比如树和列表： 列表的尾部本身就是一个列表，或者 二叉树的左右分支本身就是二叉树； 再比如在刚才提到的计算器中表达式本身的结构也是递归的，例如： 加法表达式中的被加数本身可能构成一个乘法表达式。

允许选择的数据类型称为和类型 Sum Types， 可以包含自身实例的数据类型称为递归数据类型 Recursive Datatypes。 递归和类型则称作归纳数据类型 Inductive Datatypes， 这是因为与其相关的陈述的可通过数学归纳法来证明。 在编程时，归纳数据类型通过模式匹配和递归函数来操作。

许多内置类型实际上都是标准库中的归纳数据类型。 例如 Bool 就是一个归纳数据类型：

inductive Bool where
  | false : Bool
  | true : Bool

这个声明有两个主要部分： 第一行提供新类型的名称（Bool），而 其余行则各自描述一个构造器。 与结构构造器一样，归纳数据类型的构造器 仅仅只是其他数据的惰性接收者和容器， 而非插入任意初始化和验证代码的地方。 与结构有所不同的是，归纳数据类型可以拥有多个构造器： 这里有两个构造器 true 和 false，它们都不接收任何参数。就像 结构声明会将其构造器名称置于以待声明类型为名称的命名空间中一样， 归纳数据类型也会将其构造器的名称置于一个命名空间中。 Lean 标准库中的 true 和 false 被从这个命名空间重新导出以便直接调用， 如此就不用每次都写 Bool.true、Bool.false 了。

从数据建模的角度来说，归纳数据类型的使用场景可能会与 其他语言中的密封抽象类高度重叠。在 C# 或 Java 等语言中， 大部分人可能会如下声明 Bool ：

1
2
3

abstract class Bool {}
class True  : Bool {}
class False : Bool {}

然而这些表示的具体细节是相当不同的，比方说 每个非抽象类都声明了新的类型和数据分配方式。 在面向对象的示例中， True 和 False 都是比 Bool 更具体的类型，而 Lean 的代码 仅引入新类型 Bool。

非负整数类型 Nat 也是一个归纳数据类型：

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

这里 zero 表示 0， succ 表示某个数字的后继。 succ 的声明里提到的 Nat 就是正在被声明的类型 Nat。 后继 Successor 意味着“比……大一”，所以 5 的后继是 6， 32,185 的后继是 32,186。 根据这个规定， 4 就可以被表示为 Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))。 这个声明和 Bool 的定义几乎一样，只是名称略有不同； 唯一真正的区别在于 succ 后面跟着 (n : Nat)， 它指定构造器 succ 接收一个类型为 Nat 且名为 n 的形参。 名称 zero 和 succ 都位于以其类型 Nat 命名的命名空间中， 因此必须分别通过 Nat.zero 和 Nat.succ 来调用。

像 n 这样的形参名称可能 出现在 Lean 的错误消息中，或是 出现在编写数学证明时提供的反馈中。 Lean 还提供了一个可选语法以便按名称提供实参。 尽管如此，通常形参名称的选择并没有像结构字段名称那样重要， 因为 API 里的大部分内容并不是由它构成的。

在 C# 或 Java 中 Nat 可如下声明：

1
2
3
4
5
6
7
8

abstract class Nat {}
class Zero : Nat {}
class Succ : Nat {
  public Nat n;
  public Succ(Nat pred) {
    n = pred;
  }
}

就像上面的 Bool 示例一样， 上述代码声明了比 Lean 等价代码更多的类型；此外 这个示例凸显出 Lean 数据类型构造器 更像抽象类的子类而非 C# 或 Java 中的构造器， 因为这里显示的构造器还包含待执行的初始化代码。

和类型也有点类似在 TypeScript 里 使用字符串标签来编码识别联合。 TypeScript 中 Nat 可如下声明：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

interface Zero {
  tag: "zero";
}

interface Succ {
  tag: "succ";
  predecessor: Nat;
}

type Nat = Zero | Succ;

就像 C# 和 Java 一样，这种方式相比于 Lean 始终都会声明更多的类型， 因为 Zero 和 Succ 各自都构成一个类型。它也体现了 Lean 构造器 对应于 JavaScript 或 TypeScript 中包含标识内容标签的对象。

1.5.1. 模式匹配 Pattern Matching

在许多语言中，此类数据的应用都是这样进行的： 首先利用实例检查操作符检查收到的子类， 然后读取给定子类中可用字段的值。 实例检查会 确定哪些代码会被运行， 确保该代码所需的数据可用，而 字段本身则提供数据。 在 Lean 中这两个任务同时由模式匹配 Pattern Matching 完成。

一个使用模式匹配的函数的例子是 isZero：该函数 在实参为 Nat.zero 时返回 true， 否则返回 false。

def isZero (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => false

match 表达式根据实参 n 进行解构： 如果 n 由 Nat.zero 所构造， 那么便采用模式匹配的第一个分支，返回结果为 true； 如果 n 由 Nat.succ 所构造， 那么便采用模式匹配的第二个分支，返回结果为 false。

isZero Nat.zero 的逐步求值过程如下：

isZero Nat.zero
-- ==>
match Nat.zero with
  | Nat.zero => true
  | Nat.succ k => false
-- ==>
true
-- ==>

isZero 5 的求值过程也差不多：

isZero 5
-- ==>
isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))
-- ==>
match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
  | Nat.zero => true
  | Nat.succ k => false
-- ==>
false

isZero 模式里第二个分支中的 k 并不是装饰性的： 它使得作为 Nat.succ 的实参的自然数以提供的名称可见， 如此便可通过对其的调用来计算表达式最终结果。

正如某个数字 $n$ 的 后继会比其大 $1$（即 $n+1$），其 前驱也会比其小 $1$。 如果 pred 是一个查找实参前驱的函数， 那么以下示例应该找到预期的结果：

#eval pred 5
-- 4
#eval pred 839
-- 838

由于 Nat 无法表示负数，Nat.zero 可能会让人有点困惑。一般来说 在使用 Nat 时，运算符输出负数通常会被重新定义为输出 zero 本身：

#eval pred 0
-- 0

要找到 Nat 的前驱， 第一步是检查创建它的构造器是哪个： 如果是 Nat.zero，那么结果为 Nat.zero。 如果是 Nat.succ，那么名称 k 用于引用其下面的 Nat。 由于这个 Nat 是所需的前驱， 因此 Nat.succ 分支的结果是 k。

def pred (n : Nat) : Nat :=
  match n with
  | Nat.zero => Nat.zero
  | Nat.succ k => k

将此函数应用于 5 的求值步骤如下：

pred 5
-- ==>
pred (Nat.succ 4)
-- ==>
match Nat.succ 4 with
  | Nat.zero => Nat.zero
  | Nat.succ k => k
-- ==>
4

模式匹配也可以与结构或者和类型一起使用。例如， 从 Point3D 提取第三个分量的函数便可写成如下形式：

def depth (p : Point3D) : Float :=
  match p with
  | { x:= h, y := w, z := d } => d

在此情况下，只使用访问器 Point3D.z 会简单得多， 但有时结构的模式匹配可能是编写函数的更简单的方法。

1.5.2. 递归函数 Recursive Functions

调用待声明常量的常量声明称作是递归声明 Recursive Definitions。 归纳数据类型是允许递归的。实际上 Nat 正是这种数据类型的一个示范， 因为 succ 需要另一个 Nat。 递归数据类型可以表示任意大的数据， 仅受限于可用内存等技术因素。 正如在数据类型的声明中 不可能为每个自然数都写下一个构造器，我们也 不可能为每种可能性写下模式匹配情况。

递归数据类型可以与递归函数很好地进行配合。 一个简单的 Nat 上递归函数的例子便是检查实参的奇偶性， 此案例中 Nat.zero 是偶数。 像这样的代码的非递归分支称作是基本情况 Base Cases。 奇数的后继是偶数，偶数的后继是奇数；这意味着 Nat.succ 构建出偶数当且仅当实参不是偶数：

def even (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (even k)

对于在 Nat 上编写递归函数， 刚才的思维模式是非常典型的： 首先确定要对 Nat.zero 做什么， 然后确定如何将任意 Nat 的结果转换为其后继的结果， 并将此转换应用于递归调用的结果。 这种思维模式称为结构递归 Structural Recursion。

与许多语言不同，Lean 默认会确保每个递归函数最终都会落到基本情况。 从编程角度来看，这排除了意外的无限循环。 这个特性在证明定理时也特别重要，因为无限循环会造成大麻烦。 一个案例是 Lean 不会接受尝试将函数自身递归应用在输入数字上的 even：

def evenLoops (n : Nat) : Bool :=
  match n with
  | Nat.zero => true
  | Nat.succ k => not (evenLoops n)
-- fail to show termination for 
--   evenLoops
-- with errors
-- failed to infer structural recursion:
-- Not considering parameter n of evenLoops:
--   it is unchanged in the recursive calls
-- no parameters suitable for structural recursion
-- 
-- well-founded recursion cannot be used, 
-- 'evenLoops' does not take any (non-fixed) arguments

错误消息中的重要部分是 Lean 无法确定该递归函数是否总能落到基本情况（因为并不能）。

尽管加法需要两个实参， 但其实只需要检查其中一个即可： 要将 $0$ 加到数字 $n$，只需将 $n$ 原样返回即可； 要将 $k$ 的后继加到 $n$，只需将 $k$ 加到 $n$ 的结果的后继返回即可。

def plus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => Nat.succ (plus n k')

在 plus 的声明中，名称 k' 被选中 是为了暗示它与 plus 的形参 k 相关联但不相同。 做个示范，plus 3 2 的求值过程将会产生如下步骤：

plus 3 2
-- ==>
plus 3 (Nat.succ (Nat.succ Nat.zero))
-- ==>
match Nat.succ (Nat.succ Nat.zero) with
  | Nat.zero => 3
  | Nat.succ k' => Nat.succ (plus 3 k')
-- ==>
Nat.succ (plus 3 (Nat.succ Nat.zero))
-- ==>
Nat.succ (match Nat.succ Nat.zero with
  | Nat.zero => 3
  | Nat.succ k' => Nat.succ (plus 3 k'))
-- ==>
Nat.succ (Nat.succ (plus 3 Nat.zero))
-- ==>
Nat.succ (Nat.succ (match Nat.zero with
  | Nat.zero => 3
  | Nat.succ k' => Nat.succ (plus 3 k')))
-- ==>
Nat.succ (Nat.succ 3)
-- ==>
5

实现加法 $n+k$ 的一种方法是将 Nat.succ 应用到 $n$ 上 $k$ 次。类似地， 乘法 $n\times k$ 会将 $n$ 加到自身 $k$ 次：

def times (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => Nat.zero
  | Nat.succ k' => plus n (times n k')

减法 $n-k$ 则会将 $n$ 的前驱应用到 $n$ 上 $k$ 次：

def minus (n : Nat) (k : Nat) : Nat :=
  match k with
  | Nat.zero => n
  | Nat.succ k' => pred (minus n k')

不是每个函数都可以使用结构递归轻松编写。如果将 加法理解为迭代 Nat.succ， 乘法理解为迭代加法， 减法理解为迭代前驱，那么 除法貌似是迭代减法；如果真是这样，那么 如果分子小于除数，则结果为零； 否则结果是将分子减去除数再除以除数的后继：

def div (n : Nat) (k : Nat) : Nat :=
  if n < k 
  then 0
  else Nat.succ (div (n - k) k)
-- fail to show termination for
--   div
-- with errors
-- failed to infer structural recursion:
-- Not considering parameter k of div:
--   it is unchanged in the recursive calls
-- Cannot use parameter k:
--   failed to eliminate recursive application
--     div (n - k) k
-- 
-- 
-- failed to prove termination, possible solutions:
--   - Use `have`-expressions to prove the remaining goals
--   - Use `termination_by` to specify a different well-founded relation
--   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-- k n : Nat
-- h✝ : ¬n < k
-- ⊢ n - k < n

只要第二个参数不是 $0$， 那么这个程序就一定会终止， 因为它总是向基本情况进展； 然而它不是结构递归的， 因为它并不遵循下述模式： 为 0 找到结果并将较小 Nat 的结果转换为其后继结果， 尤其是函数的递归调用被应用于 另一个函数调用后的结果（(n - k)）而非 输入值可能对应的构造器所接收的实参（比如前面 | Nat.succ k' 里的 k' ）。 因此 Lean 会产生上述报错。

此消息意味着 div 的证明需要被手动终止。 这个主题会在最后一章中探讨。

1.6. 多态性 Polymorphism

就像大多数语言一样，Lean 中的类型也可以接收实参；例如，类型 List Nat 对应自然数列表， List String 对应字符串列表， List (List Point) 对应点的列表的列表。 这分别与 C# 或 Java 等语言中的 List<Nat>、 List<String>、 List<List<Point>> 类似。 正如 Lean 使用空格向函数传递实参一样， 它也通过空格向类型传递实参。

在函数式编程中，术语“多态性 Polymorphism” 通常用于描述那些接收类型作为实参的数据类型或声明。 这与面向对象编程社区不同，在那里，这个术语 通常用于描述可能覆盖其超类某些行为的子类。 在本书中"多态性"始终指该词的第一种含义。 这些类型形参可以被用于数据类型或声明当中， 使得同一个数据类型或声明可以推广到各种不同类型。

Point 结构要求 x 和 y 字段都是 Float， 但现实中的点并没有要求每个坐标都非得采用某种特定的表示。 Point 的多态版本 PPoint 可以接收一个类型作为实参， 然后将该类型用于两个字段之中：

structure PPoint (α : Type) where
  x : α
  y : α

就像函数常量声明里形参紧跟在待声明函数常量之后一样， 结构里形参也紧跟在结构名称之后。在 Lean 中， 在没有更具体的名称时，习惯上我们会用希腊字母来命名类型形参。 Type 是一个描述其他类型的类型，因此 Nat、List String 和 PPoint Int 都具有类型 Type。

同 List 一样， PPoint 也可以通过提供特定类型作为其实参来使用：

def natOrigin : PPoint Nat :={ 
  x := Nat.zero, 
  y := Nat.zero
}

在这个例子中，两个字段的类型都被期望是 Nat。 正如函数调用是通过将形参调用替换为实参的值完成的， 向 PPoint 提供类型实参 Nat 同样也会创建一个结构， 其字段 x、y 的类型为 Nat，因为形参 α 已被类型实参 Nat 替换。 类型也是 Lean 中的普通表达式， 将实参传递给多态类型（如 PPoint） 不需要依赖任何特殊语法。

常量声明也可以接收类型作为实参，这使得它们同样具有多态性。 函数 replaceX 会用新值替换 PPoint 的 x 字段。 想让 replaceX 能够与任何多态的点结构一起工作， 那么 replaceX 本身也必须得是多态的。 这是通过将点的字段类型设置为首个形参实现的， 后续形参都会引用第一个形参。

def replaceX (α : Type) (point : PPoint α) (newX : α) : PPoint α :={ 
  point with x := newX 
}

也就是说：如果形参 point 和 newX 的类型提到了 α， 那么它俩指的都是那个被作为首个实参传进来的具体类型。 这类似于函数体内的形参调用 指的其实是函数在应用于实参时传进来的具体值。

要观察上述现象，可以让 Lean 检查 replaceX 的类型，然后 检查 replaceX Nat 的类型：

#check (replaceX)
-- replaceX : (α : Type) → PPoint α → α → PPoint α

这个函数的类型包含了首个形参的名称， 其余的形参都会用到这个名称。正如 函数应用的值是通过 将函数体中形参调用替换为实参具体值来计算的， 函数应用的类型是通过 将函数类型中形参调用替换为提供的具体值来计算的。 传入第一个实参 Nat 会导致 函数类型里其余部分中 α 的所有出现都被替换为 Nat：

#check replaceX Nat
-- replaceX Nat : PPoint Nat → Nat → PPoint Nat

由于没有指明其余实参，在提供更多实参前不会再发生进一步的替换：

#check replaceX Nat natOrigin
-- replaceX Nat natOrigin : Nat → PPoint Nat
#check replaceX Nat natOrigin 5
-- replaceX Nat natOrigin 5 : PPoint Nat

将类型作为实参传入来确定整个函数应用表达式的类型， 这对求值能力并没有太多影响。

#eval replaceX Nat natOrigin 5
-- { x := 5, y := 0 }

多态函数通过 接收类型作为实参并 允许后续类型引用该实参来工作。 尽管如此，类型形参的命名本身并无特殊要求。 考虑一个表示正号或负号的数据类型：

inductive Sign where
  | pos
  | neg

我们可以编写一个以 Sign 为参数的函数，实参 如果是正数就返回一个 Nat， 如果是负数就返回一个 Int：

def posOrNegThree (s : Sign) :
  match s with 
    | Sign.pos => Nat 
    | Sign.neg => Int :=
  match s with
    | Sign.pos => ( 3 : Nat)
    | Sign.neg => (-3 : Int)

由于类型是第一层级的，并且可以通过 Lean 语言的普通规则来计算， 因此它们也可以通过对数据类型进行模式匹配来计算。 Lean 在检查这个函数时会发现 函数体中的 match 表达式对应于 类型中的 match 表达式，于是便 让 Nat 成为 pos 情况的预期类型，并 让 Int 成为 neg 情况的预期类型。

将 posOrNegThree 应用于 pos 会使得函数体以及返回类型中的形参调用 s 都会被替换为 pos。求值可以在表达式及其对应类型中发生：

(posOrNegThree Sign.pos :
  match Sign.pos with 
  | Sign.pos => Nat 
  | Sign.neg => Int)
-- ==>
((match Sign.pos with
  | Sign.pos => (3 : Nat)
  | Sign.neg => (-3 : Int)) :
  match Sign.pos with 
  | Sign.pos => Nat 
  | Sign.neg => Int)
-- ==>
((3 : Nat) : Nat)
-- ==>
3

1.6.1. 链表 Linked Lists

Lean 的标准库包含一个 称为 List 的规范的链表数据类型，以及 使其更便于使用的特殊语法。 列表用方括号编写。例如，包含小于 10 的质数的列表就可以写成如下形式：

def primesUnder10 : List Nat := [2, 3, 5, 7]

List 在背后其实是一个归纳数据类型，定义如下：

inductive List (α : Type) where
  | nil : List α
  | cons : α → List α → List α

标准库中的实际定义其实略有不同，因为它使用了尚未介绍的功能。 但本质上它们是相似的。这个定义意味着 List 接收单个类型作为其参数，就像 PPoint 一样： 这个类型是列表中元素的类型。根据其构造器的描述， List α 可以用 nil 或 cons 构建。 构造器 nil 表示空列表， 构造器 cons 用于非空列表。 cons 的 第一个参数是列表的首个元素（head）， 第二个参数是列表的剩余部分（tail）。 包含 $n$ 个元素的链表将会 包含 $n$ 个 cons 构造器，其中 最后一个以 nil 作为其尾部。

前面的示例 primesUnder10 可以通过 直接使用 List 的构造器更明确地编写：

def explicitPrimesUnder10 : List Nat :=
  List.cons 2 (List.cons 3 (List.cons 5 (List.cons 7 List.nil)))

这两个列表声明完全等价，但 primesUnder10 比 explicitPrimesUnder10 更容易阅读。

操作 List 的函数可以通过类似 操作 Nat 的函数的方式来构造。 实际上，有一种思考方式是将链表视作是 每个 succ 构造器都悬挂着额外数据字段的 Nat。 按照这个角度，列表长度的计算过程便是 将每个 cons 替换为 succ， 将最后的 nil 替换为 zero。 正如 replaceX 将坐标点字段的类型作为实参， length 接收列表元素的类型作为实参。 例如，如果列表元素皆为字符串， 那么第一个参数就应该是 String， 函数常量的应用就应该写成 length String ["Sourdough", "bread"]。 求值步骤如下：

length String ["Sourdough", "bread"]
-- ==>
length String (List.cons "Sourdough" (List.cons "bread" List.nil))
-- ==>
Nat.succ (length String (List.cons "bread" List.nil))
-- ==>
Nat.succ (Nat.succ (length String List.nil))
-- ==>
Nat.succ (Nat.succ Nat.zero)
-- ==>
2

常量 length 的声明 既是多态的（因为它将列表元素的类型作为实参）， 也是递归的（因为它引用自身）。 通常函数都会遵循数据的形状： 递归数据类型会产生递归函数， 多态数据类型会产生多态函数。

1
2
3
4

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | List.nil => Nat.zero
  | List.cons y ys => Nat.succ (length α ys)

诸如 xs 和 ys 之类的名称通常被用来表示未知值的列表。 名称中的 s 表示它们是复数，因此它们应被分别 读作“exes”和“whys”而非“x s”和“y s”。

为了更使操作列表的函数被容易阅读， 方括号记法 [] 可用来对 nil 进行模式匹配， 中缀 :: 可用来代替 cons：

1
2
3
4

def length (α : Type) (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length α ys)

1.6.2. 隐式参数 Implicit Arguments

replaceX 和 length 用起来都有些繁琐， 因为类型实参每次都要手动输入。实际上在大多数语言中， 编译器完全能自行确定类型实参，只不过是偶尔需要用户的提示。 Lean 也是如此。在定义函数时，可以通过将形参包装在花括号 而非圆括号中来将其声明为隐式的 Implicit。例如， 带隐式类型形参的 replaceX 如下所示：

def replaceX {α : Type} (point : PPoint α) (newX : α) : PPoint α :={ 
  point with x := newX 
}

它可以直接与 natOrigin 一起使用而无需提供 Nat， 因为 Lean 可以根据后续的实参中推断出 α 的值：

#eval replaceX natOrigin 5
-- { x := 5, y := 0 }

类似地，length 可以重新定义为隐式接收条目类型：

def length {α : Type} (xs : List α) : Nat :=
  match xs with
  | [] => 0
  | y :: ys => Nat.succ (length ys)

新的 length 函数可以直接应用于 primesUnder10：

#eval length primesUnder10
-- 4

在标准库中，Lean 将此函数称为 List.length， 这意味着用于结构字段访问的点语法也可以用来查找列表的长度：

#eval primesUnder10.length
-- 4

正如在 C# 和 Java 有时需要明确提供类型实参一样， Lean 也不是总能找到隐式参数的值。在这些特殊情况下， 我们可以借助它们的名称来进行额外提示。例如， 只适用于整数列表的 List.length 版本就可以通过 将 α 设置为 Int 来指定：

#check List.length (α := Int)
-- List.length : List Int → Nat

1.6.3. 更多内置数据类型 More Built-In Datatypes

除了列表之外，Lean 的标准库 还包含许多其他结构和归纳数据类型， 可用于各种场景。

1.6.3.1. 可空类型 Option

并非每个列表都有第一个条目，有些列表是空的。 许多集合操作可能无法得出它们正在查找的内容。例如， 查找列表中第一个条目的函数可能找不到任何此类条目。因此， 必须有一种方法来表示没有第一个条目。 许多语言都有一个 null 值来表示没有值。 Lean 没有为现有类型配备一个特殊的 null 值， 而是提供了一个名为 Option 的数据类型， 为其他类型配备了一个缺失值指示器。例如， 一个可为空的 Int 由 Option Int 表示， 一个可为空的字符串列表由类型 Option (List String) 表示。 引入一个新类型来表示可空性意味着类型系统确保无法忘记对 null 的检查， 因为 Option Int 不能在需要 Int 的上下文中使用。

Option 有两个构造器， 分别称为 some 和 none， 分别表示底层类型的非空和空版本。 非空构造器 some 包含基础值， 而 none 不接收任何参数：

1
2
3

inductive Option (α : Type) : Type where
  | none : Option α
  | some (val : α) : Option α

Option 类型非常类似于 C# 和 Kotlin 中的可空类型，但并不完全相同。在这些语言中， 如果一个类型（例如 Boolean）总是引用该类型的实际值（true 和 false）， 则类型 Boolean? 或 Nullable<Boolean> 还额外允许 null 值。 在类型系统中跟踪这一点非常有用：类型检查器和其他工具可以帮助程序员记住检查 null， 并且通过类型签名显式描述可空性的 API 比不描述的可空性 API 更有信息量。然而， 这些可空类型与 Lean 的 Option 有一个非常重要的区别，那就是它们不允许多层可空性。 Option (Option Int) 可以通过 none、some none 或 some (some 360) 构造。 另一方面，Kotlin 将 T?? 视为与 T? 等价。 这种微妙的差异在实践中很少相关，但有时可能很重要。

要查找列表中的第一个条目（如果存在），使用 List.head?。 问号是名称的一部分，这与在 C# 或 Kotlin 中使用问号表示可空类型无关。 在 List.head? 的定义中，下划线用于表示列表的尾部。 在模式匹配中，下划线匹配任何东西，但不会引入变量来引用匹配的数据。 使用下划线而不是名称是向读者清楚地传达输入的一部分被忽略的一种方式。

1
2
3
4

def List.head? {α : Type} (xs : List α) : Option α :=
  match xs with
  | [] => none
  | y :: _ => some y

Lean 的命名约定是 使用后缀 ? 定义可能失败的组操作的版本，该版本返回一个 Option； 使用后缀 ! 定义版本，会在提供无效输入时崩溃； 使用后缀 D 定义版本，会在操作本应失败时返回默认值。 按照这个模式， List.head 要求调用者提供数学证据证明列表不为空， List.head? 返回一个 Option， List.head! 当传递空列表时崩溃， List.headD 接收一个默认值，在列表为空时返回。 问号和感叹号是名称的一部分，而不是特殊语法， 因为 Lean 的命名规则比许多语言更宽松。

因为 head? 定义在 List 命名空间中，它可以使用访问器表示法：

1
2

#eval primesUnder10.head?
-- some 2

然而，在空列表上测试它会导致两个错误：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

#eval [].head?
-- don't know how to synthesize implicit argument 'α'
--    @List.nil ?m.3
-- context:
-- ⊢ Type ?u.61664
--
-- don't know how to synthesize implicit argument 'α'
--   @_root_.List.head? ?m.3 []
-- context:
-- ⊢ Type ?u.61664

这是因为 Lean 无法完全确定表达式的类型。特别是，它 既找不到 List.head? 的隐式类型参数， 也找不到 List.nil 的隐式类型参数。 在 Lean 的输出中，?m.XYZ 表示一个无法推断的部分程序。 这些未知部分称为元变量 Metavariables， 它们出现在一些错误消息中。为了评估表达式，Lean 需要能够找到它的类型， 而类型不可用是因为空列表没有可以从中找到类型的条目。 我们需要显式提供类型以允许 Lean 继续执行代码：

1
2

#eval [].head? (α := Int)
-- none

也可以通过类型标注提供类型：

1
2

#eval ([] : List Int).head?
-- none

错误消息提供了一个有用的线索。两个消息都使用相同的元变量 来描述缺失的隐式参数，这意味着 Lean 已经确定两个缺失的部分 将共享一个解决方案，即便其无法确定实际值。

1.6.3.2. 积类型 Prod

结构 Prod （即“Product”的简称）是一个 通用的将两个值连接在一起的方式。例如， Prod Nat String 包含 一个 Nat 和 一个 String。 换句话说，Point Nat 可被替换为 Prod Nat Nat。Prod 非常类似于 C# 的元组、 Kotlin 的 Pair 和 Triple 类型以及 C++ 的 tuple。 许多应用程序最好通过定义自己的结构来实现，即使是简单的案例 Point，因为 使用领域术语可以使代码更易读。此外， 定义结构类型可以通过为不同的领域概念分配不同的类型来捕获更多的错误，防止它们被混淆。另一方面， 有些情况下定义新类型的开销不值得，此外 一些库已经足够通用，以至于没有比偶对（Pair）更具体的概念了。最后， 标准库包含许多方便函数，使内置的 Pair 类型更容易使用。

结构 Prod 使用两个类型参数定义：

1
2
3

structure Prod (α : Type) (β : Type) : Type where
  fst : α
  snd : β

列表使用非常频繁，因此有特殊的语法使其更易读。 出于同样的原因，积类型和其构造器都有特殊的语法。 类型 Prod α β 通常写为 α × β，模仿集合的笛卡尔积的通常表示法。类似地， Prod 可以使用通常的数学表示法表示偶对。换句话说，不必写：

1
2
3
4

def fives : String × Int := { 
  fst := "five", 
  snd := 5 
}

只需写：

1
2
3
4

def fives : String × Int := (
  "five", 
  5
)

两种表示法都是右结合的。这意味着以下定义是等价的：

1
2
3
4

def sevens : String × Int × Nat := 
  ("VII", 7, 4 + 3)
def sevens : String × (Int × Nat) := 
  ("VII", (7, 4 + 3))

换句话说，所有大于两个类型的积类型及其对应的构造器实际上是嵌套的积类型和嵌套的偶对。

1.6.3.3. 和类型 Sum

和类型 Sum 是允许在两个不同类型的值之间进行选择的一般方式。 例如，Sum String Int 要么是一个 String， 要么是一个 Int。 类似于 Prod，当编写非常通用的代码时， 在没有任何有意义的领域特定类型的小部分代码中， 或者当标准库包含有用函数时，应该使用 Sum。 在大多数情况下，使用自定义归纳数据类型更可读和更易维护。

正像 Prod，当编写非常通用的代码时， 在没有任何有意义的领域特定类型的小部分代码中， 或者当标准库包含有用函数时，应该使用 Sum。 在大多数情况下，使用自定义归纳数据类型更可读和更易维护。

类型为 Sum α β 的值 要么是构造器 inl 应用于类型为 α 的值， 要么是构造器 inr 应用于类型为 β 的值：

1
2
3

inductive Sum (α : Type) (β : Type) : Type where
  | inl : α → Sum α β
  | inr : β → Sum α β

这些名字分别是“左注入 Left Injection”和“右注入 Right Injection”的缩写。 正如笛卡尔积表示法用于 Prod， “圆加”表示法用于 Sum，所以 α ⊕ β 是 Sum α β 的另一种写法。 对于 Sum.inl 和 Sum.inr 没有特殊的语法。