1.5. 数据类型与模式
结构使得多个相互独立的数据片段能够组合成一个连贯的整体，并由一个全新的类型来表示。 像结构这样把一组值组合在一起的类型称为积类型。 然而，许多领域概念无法自然地表示为结构。 例如，一个应用程序可能需要跟踪用户权限，其中一些用户是文档所有者，一些用户可以编辑文档，而另一些用户只能读取文档。 计算器具有若干二元运算符，例如加法、减法和乘法。 结构并不提供一种简便方式来编码多种选择。
类似地，虽然结构体是跟踪固定字段集合的绝佳方式，但许多应用需要可能包含任意数量元素的数据。 多数经典数据结构，如树和列表，都具有递归结构：列表的尾部本身是一个列表，或者二叉树的左右分支本身也是二叉树。 在前述计算器中，表达式自身的结构是递归的。 例如，加法表达式中的各个加数本身可能是乘法表达式。
允许选择的数据类型称为和类型，而能够包含其自身实例的数据类型称为递归数据类型。 递归和类型称为归纳数据类型，因为可以使用数学归纳法来证明关于它们的陈述。 在编程时，归纳数据类型通过模式匹配和递归函数来使用。
许多内建类型实际上是标准库中的归纳数据类型。
例如，Bool 是一个归纳数据类型：
inductive Bool where
| false : Bool
| true : Bool
此定义有两个主要部分。
第一行给出了新类型的名称（Bool），而其余各行分别描述一个构造子。
与结构的构造子一样，归纳数据类型的构造子只是惰性的接收者和其他数据的容器，而不是插入任意初始化和验证代码的位置。
不同于结构，归纳数据类型可以有多个构造子。
这里有两个构造子，true 和 false，且二者都不接受任何实参。
正如结构声明会把其名称放入一个以所声明类型命名的命名空间中，归纳数据类型也会把其构造子的名称放入一个命名空间中。
在 Lean 标准库中，true 和 false 从此命名空间重新导出，因此它们可以单独书写，而不必分别写作 Bool.true 和 Bool.false。
从数据建模的角度看，归纳数据类型用于许多与其他语言中密封抽象类类似的场景。
在 C# 或 Java 这样的语言中，可以写出类似的 Bool 定义：
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 本身。
后继的意思是“比……大一”，因此五的后继是六，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.zero 和 Nat.succ 引用它们。
参数名称（例如 n）可能出现在 Lean 的错误消息中，也可能出现在编写数学证明时提供的反馈中。
Lean 还提供了一种可选语法，用于按名称提供参数。
不过，一般而言，参数名称的选择不如结构字段名称的选择重要，因为它并不构成 API 的那么大一部分。
在 C# 或 Java 中，Nat 可以定义如下：
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 可以如下定义：
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. 模式匹配
在许多语言中，使用这类数据时，首先用 instance-of 运算符检查收到的是哪个子类，然后读取该给定子类中可用字段的值。 instance-of 检查决定运行哪段代码，从而确保该代码所需的数据可用，而字段本身则提供这些数据。 在 Lean 中，这两个目的由模式匹配同时实现。
使用模式匹配的函数示例之一是 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 5 的求值过程类似：
isZero 中模式第二个分支里的 k 并非装饰性的。
它使作为 Nat.succ 的参数的 Nat 以给定名称变得可见。
随后可以使用这个较小的数来计算表达式的最终结果。
正如某个数 n 的后继比 n 大一（即 n + 1）一样，一个数的前驱比它小一。
如果 pred 是求 Nat 的前驱的函数，那么下面的示例应当得到预期结果：
#eval pred 5#eval pred 839
要寻找 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 会产生以下步骤：
1.5.2. 递归函数
引用正在被定义的名称的定义称为递归定义。
归纳数据类型允许递归；事实上，Nat 就是这种数据类型的一个例子，因为 succ 要求另一个 Nat。
递归数据类型可以表示任意大的数据，只受可用内存等技术因素限制。
正如不可能在数据类型定义中为每个自然数写出一个构造子，也不可能为每一种可能性写出一个模式匹配分支。
递归数据类型与递归函数相辅相成。
一个关于 Nat 的简单递归函数会检查其参数是否为偶数。
在此情形中，Nat.zero 是偶数。
像这样的非递归代码分支称为基本情形。
奇数的后继是偶数，偶数的后继是奇数。
这意味着，用 Nat.succ 构造出的数为偶数，当且仅当它的参数不是偶数。
def even (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (even k)
这种思考模式是为 Nat 编写递归函数时的典型方式。
首先，确定对 Nat.zero 应当做什么。
然后，确定如何把任意 Nat 的结果转换为其后继的结果，并将这个转换应用于递归调用的结果。
这种模式称为结构递归。
与许多语言不同，Lean 默认确保每个递归函数最终都会到达一个基本情形。
从编程角度看，这排除了意外的无限循环。
但在证明定理时，这一特性尤其重要，因为无限循环会造成重大困难。
其结果是，Lean 不会接受试图在原始数上递归调用自身的 even 版本：
def evenLoops (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (evenLoops n)该错误消息的重要部分在于，Lean 无法判定这个递归函数总是会到达一个基本情形（因为它并不会）。
尽管加法接受两个参数，但只需要检查其中一个。
要把零加到一个数 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' 是为了表明它与实参 k 有关联，但并不相同。
例如，逐步考察 plus 3 2 的求值过程，会得到以下步骤：
plus 3 2plus 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 作用 k 次于 n。
类似地，乘法 n × k 将 n 与自身相加 k 次，而减法 n - 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')def minus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k' => pred (minus n k')