1.5. 数据类型和模式匹配
结构使多个独立的数据片段能够组合成一个连贯的整体，由一个全新的类型表示。 将值集合组合在一起的类型（如结构）称为 积类型（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 定义：
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） 意味着"比...大一"，所以五的后继是六，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 可以定义如下：
和类型也类似于在 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. 模式匹配
在许多语言中，这些类型的数据通过首先使用实例检查操作符来检查收到的是哪个子类，然后读取给定子类中可用字段的值来使用。 实例检查确定运行哪些代码，确保该代码所需的数据可用，而字段本身提供数据。 在 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 5 的求值类似地进行：
isZero 5isZero (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 => falsefalse
isZero 模式第二分支中的 k 不是装饰性的。
它使作为 Nat.succ 参数的 Nat 以提供的名称可见。
然后可以使用该较小的数字来计算表达式的最终结果。
正如某个数字 n 的后继比 n 大一（即 n + 1），数字的前驱比它小一。
如果 pred 是一个查找 Nat 的前驱的函数，那么以下示例应该找到预期的结果：
#eval pred 5#eval pred 839
因为 Nat 不能表示负数，Nat.zero 有点让人困惑。
通常，在使用 Nat 时，通常会产生负数的运算符被重新定义为产生 zero 本身：
#eval pred 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 产生以下步骤：
模式匹配可以与结构以及和类型一起使用。
例如，从 Point3D 提取第三维的函数可以写成如下形式：
def depth (p : Point3D) : Float :=
match p with
| { x:= h, y := w, z := d } => d
在这种情况下，只使用 Point3D.z 访问器会简单得多，但结构模式有时是编写函数的最简单方法。
1.5.2. 递归函数
引用正在定义的名称的定义称为 递归定义（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)错误消息的重要部分是 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 应用到 n 上 k 次。
类似地，乘法 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')
不是每个函数都可以使用结构递归轻松编写。
将加法理解为迭代 Nat.succ，乘法理解为迭代加法，减法理解为迭代前驱，这表明除法的实现是迭代减法。
在这种情况下，如果分子小于除数，结果为零。
否则，结果是将分子分子减去除数再除以除数的后继。
def div (n : Nat) (k : Nat) : Nat :=
if n < k then
0
else Nat.succ (div (n - k) k)
只要第二个参数不是 0，这个程序就会终止，因为它总是向基本情况进展。
但是，它不是结构递归的，因为它不遵循为零找到结果并将较小 Nat 的结果转换为其后继结果的模式。
特别是，函数的递归调用应用于另一个函数调用的结果，而不是输入构造器的参数。
因此，Lean 用以下消息拒绝它：
此消息意味着 div 需要手动终止证明。
这个主题在 最后一章 中探讨。