数据类型与模式匹配

结构体使多个独立的数据块可以组合成一个连贯的整体，该整体由一个全新的类型表示。将一组值组合在一起的类型（如结构体）称为 积类型（Product Type） 。然而，许多领域的概念不能自然地表示为结构体。例如，应用程序可能需要跟踪用户权限，其中一些用户是文档所有者，一些用户可以编辑文档，而另一些用户只能阅读文档。计算器具有许多二元运算符，例如加法、减法和乘法。结构体无法提供一种简单的方法来编码多项选择。

同样，尽管结构体是跟踪固定字段集的绝佳方式，但许多应用程序需要可能包含任意数量元素的数据。大多数经典的数据结构（例如树和列表）具有递归结构，其中列表的尾部本身是一个列表，或者二叉树的左右分支本身是二叉树。在上述计算器中，表达式本身的结构体是递归的。例如，加法表达式中的加数本身可能是乘法表达式。

允许选择的类型称为 和类型（Sum Type） ，而可以包含自身实例的类型称为 递归类型（Recursive Datatype） 。递归和类型称为 归纳类型（Inductive Datatype） ，因为可以用数学归纳法来证明有关它们的陈述。在编程时，归纳类型通过模式匹配和递归函数来消耗。

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

inductive Bool where
  | false : Bool
  | true : Bool

此定义有两个主要部分。第一行提供了新类型（Bool）的名称，而其余各行分别描述了一个构造子。与结构体的构造子一样，归纳类型的构造子只是其他数据的接收器和容器，而不是插入任意初始化代码和验证代码的地方。与结构体不同，归纳类型可以有多个构造子。这里有两个构造子，true 和 false，并且都不接受任何参数。就像结构体声明将其名称放在与类型同名的命名空间中一样，归纳类型也将构造子的名称放在命名空间中。在 Lean 标准库中，true 和 false 从此命名空间中重新导出，以便可以单独编写它们，而不是分别写作 Bool.true 和 Bool.false。

从数据建模的角度来看，对于归纳数据类型的使用场景，在许多与其他语言中会使用 密封抽象类（Sealed Abstract Class）。在 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） 表示「比...大一」，因此 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.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 中的对象，这些对象包含一个标识内容的标记。

模式匹配

在很多语言中，这类数据首先会使用 instance-of 运算符来检查接收了哪个子类，然后读取给定子类中可用的字段值。instance-of 会检查确定要运行哪个代码，以确保此代码所需的数据可用，而数据由字段本身提供。在 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 并非装饰性符号。它使 succ 的参数 Nat 可见，并提供了名称。然后可以使用该较小的数字计算表达式的最终结果。

正如某个数字 \( n \) 的后继比 \( n \) 大 1（即 \( n + 1\)），某个数字的前驱比它小 1。如果 pred 是一个查找 Nat 前驱的函数，那么以下示例应该能得到预期的结果：

#eval pred 5

#eval pred 839

由于 Nat 无法表示负数，因此 0 有点令人费解。在使用 Nat 时，会产生负数的运算符通常会被重新定义为产生 0 本身：

#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 会产生以下步骤：

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

在这种情况下，直接使用 z 访问器会简单得多，但结构体模式有时是编写函数的最简单方法。

递归函数

引用正在定义的名称的定义称为 递归定义（Recursive Definition） 。归纳数据类型允许是递归的，事实上，Nat 就是这样的数据类型的一个例子，因为 succ 需要另一个 Nat。递归数据类型可以表示任意大的数据，仅受可用内存等技术因素限制。就像不可能在数据类型定义中为每个自然数编写一个构造器一样，也不可能为每个可能性编写一个模式匹配用例。

递归数据类型与递归函数可以很好地互补。一个简单的 Nat 递归函数是检查其参数是否是偶数。在这种情况下，zero 是偶数。像这样的代码的非递归分支称为 基本情况（Base Case） 。奇数的后继是偶数，偶数的后继是奇数。这意味着使用 succ 构建的数字当且仅当其参数不是偶数时才是偶数。

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

这种思维模式对于在 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 无法确定递归函数是否最终会到达基本情况（因为它不会）。

fail to show termination for
  evenLoops
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) arguments

尽管加法需要两个参数，但只需要检查其中一个参数。要将零加到数字 \( 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 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 × 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 会拒绝它，并显示以下消息：

fail to show termination for
  div
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

此消息表示 div 需要手动证明停机。这个主题在最后一章中进行了探讨。

Lean 函数式编程

数据类型与模式匹配

模式匹配

递归函数