翻译-TPIL-02-依值类型论

2025-11-12 约 5700 字预计阅读 27 分钟

依值类型论 Dependent Type Theory 是一种功能强大且富有表达力的语言，允许你表达复杂的数学断言，编写复杂的硬件和软件规范，并以一种自然且统一的方式对它们进行推理。 Lean 基于一种被称作构造演算 Calculus of Construction, CoC 的依值类型论变体，附带一个由可数个非积累性宇宙 Non-Cumulative Universe 构成的层级结构并且支持归纳类型 Inductive Type。本章结束时你会对这句话的含义有一个大致的理解。

2.1. 简单类型论 Simple Type Theory

“类型论”之所以得其名是因为其中的每个表达式都具有一个与之关联的类型。比如在某个已知的语境中， x + 0 可能表示一个自然数，而 f 可能表示一个定义在自然数上的函数。对那些想要精确定义的读者而言， Lean 中的自然数是任意精度的无符号整数。

下面的例子展示了该如何声明对象并检查其类型。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
/- 定义一些常数 -/
def m : Nat := 1       -- m 是自然数
def n : Nat := 0
def b1 : Bool := true  -- b1 是布尔型
def b2 : Bool := false

/- 检查类型 -/
#check m               -- 输出: Nat
-- m : Nat
#check n
-- n : Nat
#check n + 0           -- Nat
-- n + 0 : Nat
#check m * (n + 0)     -- Nat
-- m * (n + 0) : Nat
#check b1              -- Bool
-- b1 : Bool
#check b1 && b2        -- "&&" is the Boolean and
-- b1 && b2 : Bool
#check b1 || b2        -- Boolean or
-- b1 || b2 : Bool
#check true            -- Boolean "true"
-- Bool.true : Bool

/- 求值 -/
#eval 5 * 4
-- 20
#eval m + 2
-- 3
#eval b1 && b2
-- false

任何位于 /- 和 -/ 之间的文本都算是多行注释的内容，其会被 Lean 的编译器所忽略；同样一行内双横线 -- 后的内容也是注释，亦会被编译器所忽略。与其他编程语言一样，多行注释可以嵌套，这样就可以“注释掉”一整块代码。

关键字 def 用于声明工作环境中的新常量符号。上例中 def m : Nat := 1 定义了一个类型为 Nat 且值为 1 的新常量 m。 #check 命令则要求 Lean 提供它们的类型。 Lean 里面所有向系统询问信息的辅助命令通常都以井号（#）开头。 #eval 命令则要求 Lean 计算给出的表达式。你应该试着自己声明一些常量并检查一些表达式的类型。用这样的方式来声明新对象是熟悉 Lean 的好办法。

简单类型论的强大之处在于你可以通过其他类型构建新的类型。比如，若 a 和 b 是类型，则 a -> b 表示的类型包含所有从 a 到 b 的函数， a × b 表示的类型包含所有 a 中元素与 b 中元素组成的有序对，该类型也称作笛卡尔积 Cartesian Product。注意 × 是一个 Unicode 符号。合理地使用 Unicode 可提高易读性，所有现代编辑器都支持它。在 Lean 标准库中你会经常看到希腊字母被用于表示类型。另外 Unicode 符号 → 是 -> 的更紧凑版本。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
#check Nat → Nat          -- 用 "\to" or "\r" 来打出这个箭头
-- Nat → Nat : Type
#check Nat -> Nat         -- 也可以用 ASCII 符号
-- Nat → Nat : Type

#check Nat × Nat          -- 用 "\times" 打出乘号
-- Nat × Nat : Type
#check Prod Nat Nat       -- 换成 ASCII 符号
-- Nat × Nat : Type

#check Nat → Nat → Nat
-- Nat → Nat → Nat : Type
#check Nat → (Nat → Nat)  --  效果同上
-- Nat → Nat → Nat : Type

#check Nat × Nat → Nat
-- Nat × Nat → Nat : Type
#check (Nat → Nat) → Nat  -- 一个“泛函”
-- (Nat → Nat) → Nat : Type

#check Nat.succ           -- Nat → Nat
-- Nat.succ (n : Nat) : Nat
#check (0, 1)             -- Nat × Nat
-- (0, 1) : Nat × Nat

#check Nat.add            -- Nat → Nat → Nat
-- Nat.add : Nat → Nat → Nat

#check Nat.succ 2         -- Nat
-- Nat.succ 2 : Nat
#check Nat.add 3          -- Nat → Nat
-- Nat.add 3 : Nat → Nat
#check Nat.add 5 2        -- Nat
-- Nat.add 5 2 : Nat
#check (5, 9).1           -- Nat
-- (5, 9).fst : Nat
#check (5, 9).2           -- Nat
-- (5, 9).snd : Nat

#eval Nat.succ 2
-- 3
#eval Nat.add 5 2
-- 7
#eval (5, 9).1
-- 5
#eval (5, 9).2
-- 9

再强调一次：你应该自己运行一些例子。

来看一下基本语法。你可以通过输入 \to、\r 或者 \-> 来打出 →，也可以将其换成与之等价的 ASCII 字符串 ->；如此表达式 Nat -> Nat 和 Nat → Nat 的意思其实是一样的：它们都表示以一个自然数作为输入并返回一个自然数作为输出的函数类型。用于表示笛卡尔积的 Unicode 符号 × 可通过 \times 输入。未来你将习惯于用 α，β 和 γ 等小写希腊字母来表示类型变量，你可以用 \a，\b，和 \g 来打出这些特殊字符。

还有一些需要注意的事情：首先函数 f 对值 x 的应用写作 f x （如 Nat.succ 2），其次在写类型表达式时箭头往往是右结合 Associate to the Right 的（如 Nat.add 的类型是 Nat → Nat → Nat，等价于 Nat → (Nat → Nat)）。如此你便可以把 Nat.add 视作一个函数：它接收一个自然数并返回另一个函数，而后者接收一个自然数并返回一个自然数。在类型论中这通常比将 Nat.add 函数当作一个接收一对自然数作为输入并返回一个自然数作为输出的函数更方便。举个例子： Lean 允许你“部分应用”函数 Nat.add：前面的 Nat.add 3 具有类型 Nat → Nat，相当于 Nat.add 3 返回一个“等待接收”第二个参数 n 的函数，而这个函数的表达式其实就等价于 Nat.add 3 n。

你或许已经注意到如果有 m : Nat 和 n : Nat，那么 (m, n) 则表示 m 和 n 组成的有序对，其类型为 Nat × Nat。这个方法可以制造自然数有序对。反之如果有 p : Nat × Nat，那么之后你就可以写 p.1 : Nat 和 p.2 : Nat。这个方法用于提取它的两个组件。

2.2. 类型作为对象 Types as objects

相较于简单类型论，Lean 所基于的依值类型论的一个额外特点是类型本身（如 Nat 和 Bool 这些实体）也是对象，因此它们也具有对应的类型。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
#check Nat
-- Nat : Type
#check Bool
-- Bool : Type
#check Nat → Bool
-- Nat → Bool : Type
#check Nat × Bool
-- Nat × Bool : Type
#check Nat → Nat
-- Nat → Nat : Type
#check Nat × Nat → Nat
-- Nat × Nat → Nat : Type
#check Nat → Nat → Nat
-- Nat → Nat → Nat : Type
#check Nat → (Nat → Nat)
-- Nat → Nat → Nat : Type
#check Nat → Nat → Bool
-- Nat → Nat → Bool : Type
#check (Nat → Nat) → Nat
-- (Nat → Nat) → Nat : Type

你会发现上面的每个表达式都是类型为 Type 的对象。另外你也可以为类型声明新的常量：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
def α : Type := Nat
def β : Type := Bool
def F : Type → Type := List
def G : Type → Type → Type := Prod

#check α
-- α : Type
#check F α
-- F α : Type
#check F Nat
-- F Nat : Type
#check G α
-- G α : Type → Type
#check G α β
-- G α β : Type
#check G α Nat
-- G α Nat : Type

如上例所示，你已经看到了一个类型为 Type → Type → Type 的函数例子，也就是笛卡尔积 Prod：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
def α : Type := Nat
def β : Type := Bool

#check Prod α β
-- α × β : Type
#check α × β
-- α × β : Type

#check Prod Nat Nat
-- Nat × Nat : Type
#check Nat × Nat
-- Nat × Nat : Type

另外还有一个例子：对任意类型 α List α 都代表元素类型皆为 α 的列表所构成的类型。

1
2
3
4
5
6
def α : Type := Nat

#check List α
-- List α : Type
#check List Nat
-- List Nat : Type

貌似 Lean 中的任何一个表达式都有对应的类型。你可能会想：Type 自己的类型又会是什么呢？

1
2
#check Type
-- Type : Type 1

事实上你已经接触到了 Lean 类型系统中最微妙的一个方面， Lean 的底层基础拥有无限的类型层级：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
#check Type
-- Type : Type 1
#check Type 1
-- Type 1 : Type 2
#check Type 2
-- Type 2 : Type 3
#check Type 3
-- Type 3 : Type 4
#check Type 4
-- Type 4 : Type 5

可以考虑将 Type 0 看作是一个由“小”或“普通”类型组成的宇宙；然后 Type 1 是一个更大的类型范围，其中包含 Type 0 作为一个元素；紧接着 Type 2 是一个更大的类型范围，其中包含 Type 1 作为一个元素。这个列表是无限的，对每个自然数 n 都会有对应的 Type n。另外 Type 是 Type 0 的缩写：

1
2
3
4
#check Type
-- Type : Type 1
#check Type 0
-- Type : Type 1

下表或许有助于具体说明所讨论的关系。列方向对应宇宙的变化，行方向对应“度”（degree）的变化。

Sort	Type	Term
`Prop` (`Sort 0`)	`True`	`True.intro`
`Type 0` ( `Sort 1` )	`Bool`	`true`
`Type 1` ( `Sort 2` )	`Nat -> Type 0`	`fun n => Fin n`
`Type 2` ( `Sort 3` )	`Type 0 -> Type 1`	`fun (_ : Type) => Type`

然而有些操作需要在类型宇宙上具有多态性 Polymorphic；例如， List α 应对任何类型的 α 都有意义，无论 α 存在于哪种层级的宇宙中。如此也就解释了函数 List 的类型签名：

1
2
#check List    
-- List.{u} (α : Type u) : Type u

这里 u 是一个类型宇宙变量。 #check 命令的输出意味着：只要 α 有类型 Type n ， List α 亦会有类型 Type n。函数 Prod 同样也有类似的多态性：

1
2
#check Prod    
-- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)

想定义多态常量可以考虑使用 universe 命令来声明宇宙变量：

1
2
3
4
universe u
def F (α : Type u) : Type u := Prod α α
#check F
-- F.{u} (α : Type u) : Type u

想避免使用 universe 命令，可以在定义 F 时提供 universe 参数：

1
2
3
def F.{u} (α : Type u) : Type u := Prod α α
#check F
-- F.{u} (α : Type u) : Type u

2.3. 函数抽象和求值 Function Abstraction and Evaluation

Lean 提供关键字 fun（或 λ）以便根据给定的表达式创建函数，如：

1
2
3
4
5
6
7
8
#check fun (x : Nat) => x + 5   -- Nat → Nat
-- fun x ↦ x + 5 : Nat → Nat
#check λ (x : Nat) => x + 5     -- λ 和 fun 是同义词
-- fun x ↦ x + 5 : Nat → Nat
#check fun x : Nat => x + 5     -- 同上
-- fun x ↦ x + 5 : Nat → Nat
#check λ x : Nat => x + 5       -- 同上
-- fun x ↦ x + 5 : Nat → Nat

上例中的类型 Nat 可以被自动推断出来：

1
2
3
4
#check fun x => x + 5           -- 同上
-- fun x ↦ x + 5 : Nat → Nat
#check λ x => x + 5             -- 同上
-- fun x ↦ x + 5 : Nat → Nat

你可以通过传入所需的参数来求值 Lambda 函数：

1
2
#eval (λ x : Nat => x + 5) 10   
-- 15

利用一个表达式创建函数的过程称为 Lambda 抽象 Lambda Abstraction 。假如你有一个变量 x : α 并且可以构建一个表达式 t : β，那么表达式 fun (x : α) => t 或 λ (x : α) => t 便是一个类型为 α → β 的对象。可以将其视作一个从 α 到 β 的函数，任意值 x 都会被其映射到对应的值 t。

更多例子见下：

1
2
3
4
5
6
#check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2
-- fun x y ↦ if (!y) = true then x + 1 else x + 2 : Nat → Bool → Nat
#check fun (x : Nat) (y : Bool) => if not y then x + 1 else x + 2
-- fun x y ↦ if (!y) = true then x + 1 else x + 2 : Nat → Bool → Nat
#check fun x y => if not y then x + 1 else x + 2
-- fun x y ↦ if (!y) = true then x + 1 else x + 2 : Nat → Bool → Nat

Lean 将刚才的三个例子解释为相同的表达式；在最后一个表达式中， Lean 可以根据表达式 if not y then x + 1 else x + 2 自动推断出 x 和 y 的类型。

一些数学上常见的操作函数的例子可以用 Lambda 抽象的项来描述:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0

#check fun x : Nat => x
-- fun x ↦ x : Nat → Nat
#check fun x : Nat => true
-- fun x ↦ true : Nat → Bool
#check fun x : Nat => g (f x)
-- fun x ↦ g (f x) : Nat → Bool
#check fun x => g (f x)
-- fun x ↦ g (f x) : Nat → Bool

思考一下这些表达式的意思：表达式 fun x : Nat => x 表示一个 Nat 上的恒等函数；表达式 fun x : Nat => true 表示一个常值函数，其输出结果永远为 true；表达式 fun x : Nat => g (f x) 表示 f 和 g 复合后的结果。通常情况下你可以省略类型注解并让 Lean 自己推断它，因此你可以用 fun x => g (f x) 来代替 fun x : Nat => g (f x)。

你可以将函数当作参数传入并通过将其命名为 f 和 g 以便在函数表达式中调用这些函数：

1
2
#check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
-- fun g f x ↦ g (f x) : (String → Bool) → (Nat → String) → Nat → Bool

你也可以将类型当作参数传入：

1
2
#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
-- fun α β γ g f x ↦ g (f x) : (α β γ : Type) → (β → γ) → (α → β) → α → γ

刚才的表达式为一个函数，其接收三个类型 α、β、γ 以及两个函数 g : β → γ、f : α → β 并返回 g 和 f 的复合结果（要理解这个函数的类型需要理解依值积类型 Dependent Product ，后面会对此进行解释）

Lambda 表达式的一般形式是 fun x : α => t，其中的变量 x 是一个约束变量（Bound Variable）——这其实是一个占位符，其“作用域”没有扩展到表达式 t 之外。比如说，表达式 fun (b : β) (x : α) => b 中的变量 b 与前面声明的常量 b 没有任何关系。这个表达式所表示的函数与 fun (u : β) (z : α) => u 其实是一样的。

正式点说，如果两个表达式仅在约束变量的命名上有所不同，那么它们就可以看作是 Alpha 等价 Alpha Equivalent 的，即可被视作是“相同的”。 Lean 可以识别出这种等价性。

注意到将项 t : α → β 应用到项 s : α 后会获得表达式 t s : β。回到前面的例子。清晰起见我们重命名约束变量。留意下述表达式的类型:

1
2
3
4
5
6
7
8
9
#check (fun x : Nat => x) 1
-- (fun x ↦ x) 1 : Nat
#check (fun x : Nat => true) 1
-- (fun x ↦ true) 1 : Bool

def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
#check (fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
-- (fun α β γ u v x ↦ u (v x)) Nat String Bool g f 0 : Bool

表达式 (fun x : Nat => x) 1 的类型是 Nat，正如预期的那样。不仅如此，(fun x : Nat => x) 应用到 1 上后返回的值还应该是 1。而事实也确实如此：

1
2
3
4
#eval (fun x : Nat => x) 1     
-- 1
#eval (fun x : Nat => true) 1  
-- true

接下来你将看到这些项是如何被求值的。请注意：这是依值类型论的一个重要特性：每个项都有对应的计算行为，并支持“规范化 Normalization”的概念。原理是：两个可以被化简为相同形式的项称作是定义等价 Definitionally Equal 的，它们会被 Lean 的类型检查器视作是“相同的”，并且 Lean 尽其所能地识别和支持这些识别结果。

Lean 是一个完备的编程语言。它有一个可以生成二进制可执行文件的编译器以及一个交互式解释器。你可以用 #eval 命令来求值表达式，这也是你测试函数的首选方法。

2.4. 定义 Definitions

记得关键字 def 提供了一个声明新对象的重要方式：

1
2
def double (x : Nat) : Nat :=
  x + x

若有了解过其他编程语言中函数的工作方式，那么这段代码可能会让你觉得更熟悉：名称 double 被定义为一个函数，其接受一个类型为 Nat 的输入参数 x，并且调用后结果是 x + x，因此其返回的类型是 Nat。如此就可以调用这个函数:

1
2
3
4
def double (x : Nat) : Nat :=
 x + x
#eval double 3    
-- 6

此时你可以把 def 当作是被命名的 fun。下例给出了相同的结果：

1
2
3
4
def double : Nat → Nat :=
  fun x => x + x
#eval double 3    
-- 6

你可以省略类型声明—— 如果 Lean 有足够的信息进行推导。类型推导是 Lean 的重要组成部分

1
2
def double :=
  fun (x : Nat) => x + x

定义的一般形式是 def foo : α := bar，其中 α 为表达式 bar 所返回的类型。尽管 Lean 通常可以自动推断出类型 α，但准确地指明类型是一个好习惯：它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，那么 Lean 就会标记一个错误。

bar 可以是任何表达式，不一定非得是一个 Lambda 表达式。如此 def 也可以用于给一些值命名，比如：

1
def pi := 3.141592654

def 可以接受多个输入参数。我们来创建一个计算加法的函数：

1
2
3
4
def add (x y : Nat) : Nat :=
  x + y
#eval add 3 2
-- 5

参数列表也可以分开写，比如：

1
2
3
4
5
6
def double (x : Nat) : Nat :=
  x + x
def add (x : Nat) (y : Nat) :=
  x + y
#eval add (double 3) (7 + 9)  
-- 22

注意这里我们用了 double 函数来创建 add 函数的第一个参数。

你还可以在 def 里写一些更有趣的表达式：

1
2
3
def greater (x y : Nat) :=
  if x > y then x
  else y

可以猜猜看这个函数会做什么。

你还可以定义一个函数，其接收另一个函数作为输入。下例里给定函数被调用了两次，第一次调用的输出结果被传递给第二次调用:

1
2
3
4
5
6
def double (x : Nat) : Nat :=
  x + x
def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
  f (f x)
#eval doTwice double 2   
-- 8

如果要更抽象一点，你也可以指定额外的函数参数，比如类型参数：

1
2
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

上述代码的意思是：compose 是一个函数，其接收的参数为两个函数——只要这两个函数各自都能接收单个输入就行。类型代数 \beta → \gamma 和 \alpha → \beta 要求第二个函数的输出类型必须与第一个函数的输入类型匹配——这很合理，否则这两个函数将无法复合。

compose 还接收第三个类型为 α 的参数，以此来调用第二个函数（局部命名为 f）并将该函数的返回结果（类型为 β）作为输入传入第一个函数（局部命名为 g）。第一个函数返回结果的类型为 γ，而这便是 compose 函数最终返回的类型。

compose 的使用范围非常宽泛，其可以用在任意类型 α β γ 上。它可以复合任意两个函数，只要前一个函数的输出类型能够匹配后一个函数的输入类型即可。例如：

1
2
3
4
5
6
7
8
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)
def double (x : Nat) : Nat :=
  x + x
def square (x : Nat) : Nat :=
  x * x
#eval compose Nat Nat Nat double square 3  
-- 18

2.5. 局部定义 Local Definitions

Lean 还允许你使用 let 关键字来引入“局部定义”。表达式 let a := t1; t2 相当于是把 t2 中所有 a 的出现都换成 t1。

1
2
3
4
5
6
7
8
9
#check let y := 2 + 2; y * y   
-- let y := 2 + 2;
-- y * y : Nat
#eval  let y := 2 + 2; y * y   
-- 16
def twice_double (x : Nat) : Nat :=
  let y := x + x; y * y
#eval twice_double 2   
-- 16

这里 twice_double x 等价于项 (x + x) * (x + x)。

你可以连续使用多个 let 命令来串联多个替换：

1
2
3
4
5
6
#check let y := 2 + 2; let z := y + y; z * z
-- let y := 2 + 2;
-- let z := y + y;
-- z * z : Nat
#eval  let y := 2 + 2; let z := y + y; z * z
-- 64

换行可以省略分号 ;。

1
2
3
def t (x : Nat) : Nat :=
  let y := x + x
  y * y

表达式 let a := t1; t2 的意思与 (fun a => t2) t1 非常相似，但二者却并不相同：前者中你应当把 t2 中每一个 a 的实例都看作是 t1 的一个缩写；而后者中 a 是一个变量，表达式 fun a => t2 可以不依赖 a 的取值而具有独自的意义。 let 是一种更为强大的缩写方式，存在一些形如 let a := t1; t2 但却无法被表示为 (fun a => t2) t1 的表达式。作为一个练习，请试着理解为什么下面的 foo 定义合法但 bar 却不是。

1
2
3
4
5
6
7
8
9
def foo := let a := Nat; fun x : a => x + 2
/-
def bar := (fun a => fun x : a => x + 2) Nat
-- failed to synthesize 
--   HAdd a Nat (?m.16 a x)
--
-- Hint: Additional diagnostic information may be available 
-- using the `set_option diagnostics true` command.
-/

注：

因为在确定 x 所属的 a 之前是无法让它 + 2 的。

2.6 变量和小节 Variables and Sections

考虑下面这三个函数的定义：

1
2
3
4
5
6
def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)
def doTwice (α : Type) (h : α → α) (x : α) : α :=
  h (h x)
def doThrice (α : Type) (h : α → α) (x : α) : α :=
  h (h (h x))

Lean 提供了 variable 指令以使这些声明变得更紧凑：

1
2
3
4
5
6
7
8
variable (α β γ : Type)

def compose (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)
def doTwice (h : α → α) (x : α) : α :=
  h (h x)
def doThrice (h : α → α) (x : α) : α :=
  h (h (h x))

你可以声明任意类型的变量，不单单只是 Type 类型：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)

def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))

#print compose
-- def compose : (α β γ : Type) → (β → γ) → (α → β) → α → γ :=
-- fun α β γ g f x ↦ g (f x)
#print doTwice
-- def doTwice : (α : Type) → (α → α) → α → α :=
-- fun α h x ↦ h (h x)
#print doThrice
-- def doThrice : (α : Type) → (α → α) → α → α :=
-- fun α h x ↦ h (h (h x))

将它们打印出来后会发现三个定义的效果完全一致：

variable 命令指示 Lean 将声明的变量作为约束变量插入到引用它们的定义之中。Lean 足够聪明，可以弄明白定义中哪些变量被显式/隐式地使用；如此在写定义时你就可以将 α、β、γ、g、f、h 和 x 视作固定对象并让 Lean 自动帮你抽象这些定义。

若是以这种方式声明，变量则将一直保持在论域内直到所处理的文件结束为止。然而有时需要限制变量的作用范围；为此 Lean 提供了小节记号 section ：

1
2
3
4
5
6
7
8
9
section useful
  variable (α β γ : Type)
  variable (g : β → γ) (f : α → β) (h : α → α)
  variable (x : α)

  def compose := g (f x)
  def doTwice := h (h x)
  def doThrice := h (h (h x))
end useful

当一个小节结束后，变量将脱离论域并无法再被引用。

你不需要缩进一个小节中的行。也不需要命名一个小节，也就是说你可以使用一对匿名的 section / end；但如果一个小节被命名了，那么你就必须使用相同的名字来关闭它。小节也可以嵌套，允许我们累加新变量的声明。

2.7. 命名空间 Namespaces

Lean 允许你将定义组织进层次化且可嵌套的命名空间 namespace 里：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7

  def fa : Nat := f a
  def ffa : Nat := f (f a)

  #check a
  -- Foo.a : Nat
  #check f
  -- Foo.f (x : Nat) : Nat
  #check fa
  -- Foo.fa : Nat
  #check ffa
  -- Foo.ffa : Nat
  #check Foo.fa
  -- Foo.fa : Nat
end Foo

-- #check a
-- -- error
-- #check f
-- -- error
#check Foo.a
-- Foo.a : Nat
#check Foo.f
-- Foo.f (x : Nat) : Nat
#check Foo.fa
-- Foo.fa : Nat
#check Foo.ffa
-- Foo.ffa : Nat

open Foo

#check a
-- Foo.a : Nat
#check f
-- Foo.f (x : Nat) : Nat
#check fa
-- Foo.fa : Nat
#check Foo.fa
-- Foo.fa : Nat

当你声称将在命名空间 Foo 中工作时，你声明的每一个标识符名称都会带有一个前缀 “Foo.”。在此命名空间内，你可以使用较短的名称来引用这些标识符；但一旦你结束该命名空间，你就必须使用较长的名称。与 section 不同，命名空间需要命名。匿名命名空间只有一个，在根级别上。

open 命令允许你在当前语境下使用较短的名称。在导入一个模块时，你通常会想着去打开它包裹的一个或多个命名空间以访问短标识符；但有时你希望将这些信息保留在一个完全限定的名称中——比如当它们与你想要使用的另一个命名空间中的标识符产生冲突的时侯。因此命名空间为你提供了一种在工作环境中管理名称的方式。

例如，Lean 把所有与列表相关的定义和定理都放在了命名空间 List 之中。

1
2
3
#check List.nil
#check List.cons
#check List.map

open List 命令允许你使用短一些的名字：

1
2
3
4
5
open List

#check nil
#check cons
#check map

像小节一样，命名空间也是可以嵌套的：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7

  def fa : Nat := f a

  namespace Bar
    def ffa : Nat := f (f a)

    #check fa
    -- Foo.fa : Nat
    #check ffa
    -- Foo.Bar.ffa : Nat
  end Bar

  #check fa
  -- Foo.fa : Nat
  #check Bar.ffa
  -- Foo.Bar.ffa : Nat
end Foo

#check Foo.fa
-- Foo.fa : Nat
#check Foo.Bar.ffa
-- Foo.Bar.ffa : Nat

open Foo

#check fa
-- Foo.fa : Nat
#check Bar.ffa
-- Foo.Bar.ffa : Nat

关闭的命名空间之后可以重新打开，甚至是在另一个文件里：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7

  def fa : Nat := f a
end Foo

#check Foo.a
-- Foo.a : Nat
#check Foo.f
-- Foo.f (x : Nat) : Nat

namespace Foo
  def ffa : Nat := f (f a)
end Foo

与小节一样，嵌套的名称空间必须按照打开的相反顺序关闭。命名空间和小节有不同的用途：命名空间组织数据，而小节声明变量以便在定义中插入。小节还可用于限定 set_option 和 open 等命令的作用范围。

然而在许多方面 namespace ... end 结构块和 section ... end 结构块的行为是一样的。比如你在命名空间中使用 variable 命令时，它的作用范围就会被限制在命名空间里。类似地，如果你在命名空间中使用 open 命令，那么它的效果在小节关闭后消失。

2.8. 依值类型论究竟“依赖”着什么? What makes dependent type theory dependent?

简单来说就是类型可以依赖于参数。你已经看到了一个很好的例子：类型 List α 依赖于参数 α，而这种依赖性是区分 List Nat 和 List Bool 的关键；再比如考虑类型 Vector α n——即所有长度为 n 且元素类型为 α 的向量。这个类型取决于两个参数：向量中元素的类型 α : Type 以及向量的长度 n : Nat。

假设你希望写一个函数 cons 能够将一个新元素插到列表的开头上，那 cons 的类型应该是怎样的呢？这样的函数是多态的：你期望 Nat，Bool 或任意类型 α 的 cons 函数都会有相似的行为，因此将类型作为 cons 的第一个参数是有道理的。如此对于任何类型 α ， cons α 始终都是 α 类型下的项构成的列表的插入函数。换句话说就是：对每个 α 函数 cons α 都会接收一个元素 a : α 并将其插入列表 as : List α 以返回一个新的列表，如此有 cons α a as : List α。

很明显 cons α 具有类型 α → List α → List α，但 cons 本身的类型呢？初步猜测是 Type → α → list α → list α，但仔细一想会发现这没有道理：α 在这个表达式中并没有指向任何东西，但实际上它应指向某个类型为 Type 的参数；换句话说，假如 α : Type 是函数的首个参数，那么接下来的两个参数的类型分别是 α 和 List α，它们的类型都依赖于首个参数 α。

1
2
3
4
5
6
7
8
9
def cons (α : Type) (a : α) (as : List α) : List α :=
  List.cons a as

#check cons Nat
-- cons Nat : Nat → List Nat → List Nat
#check cons Bool
-- cons Bool : Bool → List Bool → List Bool
#check cons
-- cons (α : Type) (a : α) (as : List α) : List α

这就是依值函数类型 Dependent Function Type ，或者说是依值箭头类型 Dependent Arrow Type ：给定 α : Type 和 β : α → Type 并把 β 考虑成 α 之上的类型类，也就是说对每个 a : α 都有会类型 β a；此时类型 (a : α) → β a 表示具有如下性质的函数 f：对每个 a : α f a 都是 β a 的一个元素，换句话说即 f 返回值的类型取决于其输入。

注意到 (a : α) → β 对任意表达式 β : Type 都有意义。若 β 的值依赖 a（比如前一段里的表达式 β a）则 (a : α) → β 就代表一个依值函数类型；若 β 的值不依赖 a 则 (a : α) → β 便与类型 α → β 无异。实际上在依值类型论（以及 Lean）中 α → β 就等价于 β 的值不依赖于 a 时的 (a : α) → β。

回到刚才关于列表的例子，你可以使用 #check 命令检查下列的 List 函数。 @ 符号以及圆/花括号之间的区别将在后面进行解释。

1
2
3
4
5
6
7
8
#check @List.cons
-- @List.cons : {α : Type u_1} → α → List α → List α
#check @List.nil
-- @List.nil : {α : Type u_1} → List α
#check @List.length
-- @List.length : {α : Type u_1} → List α → Nat
#check @List.append
-- @List.append : {α : Type u_1} → List α → List α → List α

正如依值函数类型 (a : α) → β a 通过允许 β 依赖 α 从而推广了函数类型 α → β，依值笛卡尔积类型 (a : α) × β a 也以类似的方式推广了笛卡尔积 α × β。依值积类型又称为 Sigma 类型 Sigma Type ，也可以将其写作是 Σ a : α, β a。你可以用 ⟨a, b⟩ 或者 Sigma.mk a b 来创建依值对。符号 ⟨ 和 ⟩ 可以用 \langle 和 \rangle 或 \< 和 \> 来输入。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
  ⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
  Sigma.mk a b

def h1 (x : Nat) : Nat :=
  (f Type (fun α => α) Nat x).2
#eval h1 5
-- 5
def h2 (x : Nat) : Nat :=
  (g Type (fun α => α) Nat x).2
#eval h2 5
-- 5

函数 f 和 g 表示的是同样的函数。

2.9. 隐式参数 Implicit Arguments

假设对于列表我们有下述实现：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst
-- Lst.{u} (α : Type u) : Type u
#check Lst.cons
-- Lst.cons.{u} (α : Type u) (a : α) (as : Lst α) : Lst α
#check Lst.nil
-- Lst.nil.{u} (α : Type u) : Lst α
#check Lst.append
-- Lst.append.{u} (α : Type u) (as bs : Lst α) : Lst α

然后你便可如下构建一个元素类型为 Nat 的列表：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst
-- Lst.{u} (α : Type u) : Type u
#check Lst.cons
-- Lst.cons.{u} (α : Type u) (a : α) (as : Lst α) : Lst α
#check Lst.nil
-- Lst.nil.{u} (α : Type u) : Lst α
#check Lst.append
-- Lst.append.{u} (α : Type u) (as bs : Lst α) : Lst α
#check Lst.cons Nat 0 (Lst.nil Nat)
-- Lst.cons Nat 0 (Lst.nil Nat) : Lst Nat

def as : Lst Nat := Lst.nil Nat
def bs : Lst Nat := Lst.cons Nat 5 (Lst.nil Nat)
#check Lst.append Nat as bs
-- Lst.append Nat as bs : Lst Nat

由于构造子对类型而言是多态的，我们不得不将类型 Nat 作为一个参数重复插入。但是这个信息是多余的：我们可以推断出表达式 Lst.cons Nat 5 (Lst.nil Nat) 中参数 α 的类型，因为第二个参数 5 的类型是 Nat。同理我们也可以推断出 Lst.nil Nat 所接收的参数的类型：不是因为它所包含的项，而是因为它被作为参数传入函数 Lst.cons 且后者期望在此位置接收一个具有 Lst α 类型的参数。

这是依值类型论的一个主要特点：项包含大量信息，并且部分信息可以通过语境推导得出。在 Lean 中我们使用下划线 _ 来指定那些需要系统自动填写的信息。这便是所谓的“隐式参数”。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons (α : Type u) (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil (α : Type u) : Lst α := List.nil
def Lst.append (α : Type u) (as bs : Lst α) : Lst α := List.append as bs
#check Lst
-- Lst.{u} (α : Type u) : Type u
#check Lst.cons
-- Lst.cons.{u} (α : Type u) (a : α) (as : Lst α) : Lst α
#check Lst.nil
-- Lst.nil.{u} (α : Type u) : Lst α
#check Lst.append
-- Lst.append.{u} (α : Type u) (as bs : Lst α) : Lst α
#check Lst.cons _ 0 (Lst.nil _)
-- Lst.cons Nat 0 (Lst.nil Nat) : Lst Nat

def as : Lst Nat := Lst.nil _
def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _)
#check Lst.append _ as bs
-- Lst.append Nat as bs : Lst Nat

当然敲这么多下划线还是很无聊。当一个函数接收的参数可依据语境大致推导出来时， Lean 允许你将该参数设置为在默认情况下保持隐式。这是通过将参数放入花括号来实现的，见下：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
universe u
def Lst (α : Type u) : Type u := List α
def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α := List.cons a as
def Lst.nil {α : Type u} : Lst α := List.nil
def Lst.append {α : Type u} (as bs : Lst α) : Lst α := List.append as bs

#check Lst.cons 0 Lst.nil
-- Lst.cons 0 Lst.nil : Lst Nat

def as : Lst Nat := Lst.nil
def bs : Lst Nat := Lst.cons 5 Lst.nil

#check Lst.append as bs
-- as.append bs : Lst Nat

唯一变化的是变量声明 α : Type u 两侧的花括号。我们也可以将类似的写法用在函数定义里：

1
2
universe u
def ident {α : Type u} (x : α) := x

要检查 ident 的类型需要把它包在括号里以避免显示出它的完整签名：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
universe u
def ident {α : Type u} (x : α) := x
#check (ident)
-- ident : ?m.1 → ?m.1
#check ident 1
-- ident 1 : Nat
#check ident "hello"
-- ident "hello" : String
#check @ident
-- @ident : {α : Type u_1} → α → α

这使得 ident 的第一个参数是隐式的。从记号上讲，这隐藏了类型的说明，使得 ident 看起来就像是可以接受任何类型的参数一样。事实上标准库中的函数 id 正是以这样的方式定义的。选择一个不同于惯例的名称只是为了避免名字冲突而已。

我们也可以在 variable 里用类似的方式把变量变成隐式的：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
universe u
section
  variable {α : Type u}
  variable (x : α)
  def ident := x
end

#check ident
-- ident.{u} {α : Type u} (x : α) : α
#check ident 4
-- ident 4 : Nat
#check ident "hello"
-- ident "hello" : String

此处 ident 的定义和上面那个效果是一样的。

Lean 有着非常复杂的机制来实例化隐式参数，我们将看到它们可以被用来推断函数类型、谓词，甚至是证明。这些“洞”或“占位符”实例化的过程通常被称作是繁饰 Elaboration 。隐式参数的存在意味着有时可能没有足够的信息来精确地推断表达式的含义。类似 id 或 List.nil 这样的表达式常被称作是“多态的”，因为它们在不同的上下文中可以有不同的含义。

我们可以通过 (e : T) 来指定表达式 e 的类型 T，如此在求解隐式参数时 Lean 的繁饰器就会使用 T 作为 e 的类型。在下面的第二对例子中，这种机制被用于指定表达式 id 和 List.nil 所需的类型：

1
2
3
4
5
6
7
8
9
#check (List.nil)
-- [] : List ?m.1
#check (id)
-- id : ?m.1 → ?m.1

#check (List.nil : List Nat)
-- [] : List Nat
#check (id : Nat → Nat)
-- id : Nat → Nat

数字在 Lean 中是重载的，但在数字的类型无法被推断出时 Lean 就会默认其为自然数。因此下例的前两个 #check 命令中的表达式被以同样的方式繁饰，而第三个 #check 命令则将 2 解释为整数。

1
2
3
4
5
6
#check 2
-- 2 : Nat
#check (2 : Nat)
-- 2 : Nat
#check (2 : Int)
-- 2 : Int

然而有时我们可能会发现自己处于这样的情况：我们已将函数的参数声明为隐式的，但现在却需要显式地提供参数。假如 foo 是这样的函数，那么符号 @foo 则表示同样的函数，只不过其中所有参数都是显式的。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
#check @id
-- @id : {α : Sort u_1} → α → α
#check @id Nat
-- id : Nat → Nat
#check @id Bool
-- id : Bool → Bool

#check @id Nat 1
-- id 1 : Nat
#check @id Bool true
-- id true : Bool