多态

和大多数语言一样，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 : α
deriving Repr

就像函数定义的参数紧跟在被定义的名称之后一样，结构体的参数紧跟在结构体的名称之后。在 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 与任何多态的点一起使用，它本身必须是多态的。这是通过让其第一个参数成为点字段的类型，后面的参数引用第一个参数的名称来实现的。

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

可以编写一个函数，其参数是一个符号。如果参数为正，则函数返回 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 应用于 Sign.pos 会导致函数体和其返回类型中的参数名称 s 都被 Sign.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

链表

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 的第一个参数是列表的头部，第二个参数是其尾部。包含 \( 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 的函数以相同的方式定义。事实上，一种考虑链表的方式是将其视为一个 Nat，每个 succ 构造函数都悬挂着一个额外的数据字段。从这个角度来看，计算列表的长度的过程是将每个 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 的定义既是多态的（因为它将列表项类型作为参数），又是递归的（因为它引用了自身）。通常，函数遵循数据的形状：递归数据类型对应递归函数，多态数据类型对应多态函数。"

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：

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

隐式参数

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

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

#eval primesUnder10.length

正如 C# 和 Java 要求偶尔显式提供类型参数一样，Lean 并不总是能够得出隐式参数。在这些情况下，可以使用它们的名称来提供它们。例如，可以通过将 α 设置为 Int 来特化出适用于整数列表的 List.length：

#check List.length (α := Int)

List.length : List Int → Nat

更多内置数据类型

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

`Option` 可选类型

并非每个列表都有第一个条目，有些列表是空的。许多集合操作可能无法得出它们正在查找的内容。例如，查找列表中第一个条目的函数可能找不到任何此类条目。因此，必须有一种方法来表示没有第一个条目。

许多语言都有一个 null 值来表示没有值。Lean 没有为现有类型配备一个特殊的 null 值，而是提供了一个名为 Option 的数据类型，为其他类型配备了一个缺失值指示器。例如，一个可为空的 Int 由 Option Int 表示，一个可为空的字符串列表由类型 Option (List String) 表示。引入一个新类型来表示可空性意味着类型系统确保无法忘记对 null 的检查，因为 Option Int 不能在需要 Int 的上下文中使用。

Option 有两个构造函数，称为 some 和 none，它们分别表示基础类型的非空和空的版本。非空构造函数 some 包含基础值，而 none 不带参数：

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) 构造。另一方面，C# 禁止多层可空性，只允许将 ? 添加到不可空类型，而 Kotlin 将 T?? 视为等同于 T?。这种细微的差别在实践中大多无关紧要，但有时会很重要。

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

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

Lean 的命名约定是使用后缀 ? 定义可能失败的操作，用于返回 Option 的版本， ！ 用于在提供无效输入时崩溃的版本，D 用于在操作在其他情况下失败时返回默认值的版本。例如，head 要求调用者提供数学证据证明列表不为空，head? 返回 Option，head! 在传递空列表时使程序崩溃，headD 采用一个默认值，以便在列表为空时返回。问号和感叹号是名称的一部分，而不是特殊语法，因为 Lean 的命名规则比许多语言更自由。

由于 head? 在 List 命名空间中定义，因此它可以使用访问器记法：

#eval primesUnder10.head?

some 2

然而，尝试在空列表上测试它会产生两个错误：

#eval [].head?

don't know how to synthesize implicit argument
  @List.nil ?m.20264
context:
⊢ Type ?u.20261

don't know how to synthesize implicit argument
  @_root_.List.head? ?m.20264 []
context:
⊢ Type ?u.20261

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

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

none

类型也可以用类型标注提供：

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

none

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

`Prod` 积类型

Prod 结构体，即 积（Product） 的简写，是一种将两个值连接在一起的通用方法。例如，Prod Nat String 包含一个 Nat 和一个 String。换句话说，PPoint Nat 可以替换为 Prod Nat Nat。Prod 非常类似于 C# 的元组、Kotlin 中的 Pair 和 Triple 类型以及 C++ 中的 tuple。许多应用最适合定义自己的结构体，即使对于像 Point 这样的简单情况也是如此，因为使用领域术语可以使代码更加易读。此外，定义结构体类型有助于通过为不同的领域概念分配不同的类型来捕获更多错误，防止它们混淆。

另一方面，在某些情况下，并不值得定义新类型。此外，一些库足够通用，以至于没有比 偶对（Pair） 更具体的概念。最后，标准库也包含了各种便利函数，让使用内置偶对类型变得更容易。

标准偶对结构体叫做 Prod。

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

列表的使用如此频繁，以至于有特殊的语法使它们更具可读性。出于同样的原因，积类型及其构造子都有特殊的语法。类型 Prod α β 通常写为 α × β，反映了集合的笛卡尔积的常用记法。与此类似，偶对的常用数学记法可用于 Prod。换句话说，不必写：

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

只需写

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

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

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

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

换句话说，所有超过两种类型的积及其对应的构造子，实际上都是嵌套的积和嵌套的偶对。

`Sum` 和类型

和（Sum） 数据类型是一种允许在两种不同类型的值之间进行选择的一般方式。例如，Sum String Int 要么是 String，要么是 Int。与 Prod 一样， Sum 应该在编写非常通用的代码时使用，对于没有合适的特定领域类型的一小段代码，或者当标准库包含有用的函数时使用。在大多数情况下，使用自定义归纳类型更具可读性和可维护性。

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

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

这些名称分别是「左注入（left injection）」和「右注入（right injection）」的缩写。就像笛卡尔积符号用于 Prod 一样，「圆圈加号」符号用于 Sum，因此 α ⊕ β 是 Sum α β 的另一种记法。Sum.inl 和 Sum.inr 没有特殊语法。

例如，如果宠物名称可以是狗名或猫名，那么它们的类型可以作为字符串的和来引入：

def PetName : Type := String ⊕ String

在实际程序中，通常最好为此目的自定义一个归纳数据类型，并使用有意义的构造子名称。在这里，Sum.inl 用于狗的名字，Sum.inr 用于猫的名字。这些构造子可用于编写动物名称列表：

def animals : List PetName :=
  [Sum.inl "Spot", Sum.inr "Tiger", Sum.inl "Fifi", Sum.inl "Rex", Sum.inr "Floof"]

模式匹配可用于区分两个构造子。例如，一个函数用于统计动物名称列表中狗的数量（即 Sum.inl 构造子的数量），如下所示：

def howManyDogs (pets : List PetName) : Nat :=
  match pets with
  | [] => 0
  | Sum.inl _ :: morePets => howManyDogs morePets + 1
  | Sum.inr _ :: morePets => howManyDogs morePets

函数调用在中缀运算符之前进行求值，因此 howManyDogs morePets + 1 等价于 (howManyDogs morePets) + 1。如预期的那样，#eval howManyDogs animals 会产生 3。

`Unit` 单位类型

Unit 是仅有一个无参构造子（称为 unit）的类型。换句话说，它只描述一个值，该值由没有应用于任何参数的构造子组成。Unit 定义如下：

inductive Unit : Type where
  | unit : Unit

单独使用时，Unit 并不是特别有用。但是，在多态代码中，它可以用作缺少数据的占位符。例如，以下归纳数据类型表示算术表达式：

inductive ArithExpr (ann : Type) : Type where
  | int : ann → Int → ArithExpr ann
  | plus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
  | minus : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann
  | times : ann → ArithExpr ann → ArithExpr ann → ArithExpr ann

类型参数 ann 表示标注，每个构造子都有标注。来自解析器的表达式可能带有源码位置标注，因此 ArithExpr SourcePos 的返回类型需要确保解析器在每个子表达式中放置 SourcePos。然而，不来自于解析器的表达式没有源码位置，因此它们的类型可以是 ArithExpr Unit。

此外，由于所有 Lean 函数都有参数，因此其他语言中的零参数函数可以表示为接受 Unit 参数的函数。在返回位置，Unit 类型类似于 C 的语言中的 void。在 C 系语言中，返回 void 的函数会将控制权返回给调用者，但不会返回任何有意义的值。 Unit 作为一个特意表示无意义的值，可以在类型系统无需具有特殊用途的 void 特性的情况下表达这一点。Unit 的构造子可以写成空括号： () : Unit。

`Empty` 空类型

Empty 数据类型没有任何构造子。因此，它表示不可达代码，因为任何调用序列都无法以 Empty 类型的返回值终止。

Empty 的使用频率远不及 Unit。然而，它在一些特殊情况下很有用。许多多态数据类型并非在其所有构造子中使用其所有类型参数。例如，Sum.inl 和 Sum.inr 各自只使用 Sum 的一个类型参数。将 Empty 用作 Sum 的类型参数之一可以在程序的特定点排除一个构造子。这能让我们在具有额外限制的语境中使用泛型代码。

命名：和类型，积类型与单位类型

一般来说，提供多个构造子的类型称为 和类型（Sum Type） ，而其单个构造子接受多个参数的类型称为 积类型（Product Type） 。这些术语与普通算术中使用的和与积有关。当涉及的类型包含有限数量的值时，这种关系最容易看出。如果 α 和 β 是分别包含 \( n \) 和 \( k \) 个不同值的数据类型，则 α ⊕ β 包含 \( n + k \) 个不同值，α × β 包含 \( n \times k \) 个不同值。例如，Bool 有两个值：true 和 false，Unit 有一个值：Unit.unit。积 Bool × Unit 有两个值 (true, Unit.unit) 和 (false, Unit.unit)，和 Bool ⊕ Unit 有三个值 Sum.inl true、Sum.inl false 和 Sum.inr unit。类似地，\( 2 \times 1 = 2 \)，\( 2 + 1 = 3 \)。

你可能会遇到的信息

并非所有可定义的结构体或归纳类型都可以具有类型 Type。特别是，如果一个构造子将任意类型作为参数，则归纳类型必须具有不同的类型。这些错误通常会说明一些关于「宇宙层级」的内容。例如，对于这个归纳类型：

inductive MyType : Type where
  | ctor : (α : Type) → α → MyType

Lean 会给出以下错误：

invalid universe level in constructor 'MyType.ctor', parameter 'α' has type
  Type
at universe level
  2
it must be smaller than or equal to the inductive datatype universe level
  1

后面的章节会描述为什么会这样，以及如何修改定义使其正常工作。现在，尝试将类型作为参数传递给整个归纳类型，而不是传递给构造子。

与此类似，如果构造子的参数是一个将正在定义的数据类型作为参数的函数，那么该定义将被拒绝。例如：

inductive MyType : Type where
  | ctor : (MyType → Int) → MyType

会产生以下信息：

(kernel) arg #1 of 'MyType.ctor' has a non positive occurrence of the datatypes being declared

出于技术原因，允许这些数据类型可能会破坏 Lean 的内部逻辑，使其不适合用作定理证明器。

忘记归纳类型的参数也可能产生令人困惑的消息。例如，当参数 α 没有传递给 ctor 的类型中的 MyType 时：

inductive MyType (α : Type) : Type where
  | ctor : α → MyType

Lean 会返回以下错误：

type expected, got
  (MyType : Type → Type)

该错误信息表明 MyType 的类型 Type → Type 本身并不描述类型。 MyType 需要一个参数才能成为一个真正的类型。

在其他语境中省略类型参数时也会出现相同的消息，例如在定义的类型签名中：

inductive MyType (α : Type) : Type where
  | ctor : α → MyType α

def ofFive : MyType := ctor 5

练习

编写一个函数来查找列表中的最后一个条目。它应该返回一个 Option。
编写一个函数，在列表中找到满足给定谓词的第一个条目。从 def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α := 开始定义。
编写一个函数 Prod.swap，用于交换偶对中的两个字段。定义以 def Prod.swap {α β : Type} (pair : α × β) : β × α := 开始。
使用自定义数据类型重写 PetName 示例，并将其与使用 Sum 的版本进行比较。
编写一个函数 zip，用于将两个列表组合成一个偶对列表。结果列表的长度应与最短的输入列表相同。定义以 def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) := 开始。
编写一个多态函数 take，返回列表中的前 \( n \) 个条目，其中 \( n \) 是一个 Nat。如果列表包含的条目少于 n 个，则结果列表应为输入列表。 #eval take 3 ["bolete", "oyster"] 应当产生 ["bolete", "oyster"]，而 #eval take 1 ["bolete", "oyster"] 应当产生 ["bolete"]。
利用类型和算术之间的类比，编写一个将积分配到和上的函数。换句话说，它的类型应为 α × (β ⊕ γ) → (α × β) ⊕ (α × γ)。
利用类型和算术之间的类比，编写一个将乘以 2 转换为和的函数。换句话说，它的类型应为 Bool × α → α ⊕ α。

Lean 函数式编程