# 类型与项
> 一切皆项、类型宇宙层级、Type 与 Prop 的分工，以及为什么需要宇宙。
- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/types-terms
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）
## 一切皆项
Lean 里只有一种东西：**项（term）**。每个项都有一个**类型**，而类型本身也是项，也有类型。
```lean
#check 42 -- 42 : Nat
#check Nat -- Nat : Type
#check Type -- Type : Type 1
#check Type 1 -- Type 1 : Type 2
```
读这条链：
```text
42 的类型是 Nat
Nat 的类型是 Type
Type 的类型是 Type 1
Type 1 的类型是 Type 2
...无穷
```
**没有「顶层类型」**——这是刻意的。
## 为什么需要宇宙层级
朴素的想法是让 `Type : Type`。但那会导致**罗素悖论**的类型论版本（Girard 悖论），使系统不一致——一旦不一致，任何命题都能被「证明」，整个系统失去意义。
解法是**宇宙层级（universe hierarchy）**：
```text
Type 0 (写作 Type) : Type 1
Type 1 : Type 2
Type 2 : Type 3
...
```
每一层的类型住在**更高一层**，永远没有自己包含自己的情况。
日常写代码几乎不用关心层级——Lean 自动推断。只在写**通用库代码**时才需要显式处理：
```lean
universe u
def myId {α : Type u} (a : α) : α := a
```
`universe u` 声明宇宙变量，`Type u` 表示「某一层」。这让 `myId` 能作用于任意层级的类型，而不必为每层写一遍。
**宇宙多态**（universe polymorphism）通常是自动的：写 `{α : Type _}` 或 `{α : Sort _}`，Lean 会推断出所需的层级参数。
报错里出现 `universe` 字样时，通常是把不同层级的东西混用了——比如试图让一个 `Type` 的集合包含 `Type` 自身。
## Sort、Type、Prop
Lean 的宇宙有一个统一形式 `Sort`：
```text
Sort 0 = Prop 命题的宇宙
Sort 1 = Type 0 = Type
Sort 2 = Type 1
Sort (n+1) = Type n
```
所以 **`Prop` 是第 0 层宇宙**，`Type` 是 `Type 0` 的简写。
```lean
#check Prop -- Prop : Type
#check (2 = 2) -- 2 = 2 : Prop
#check Nat -- Nat : Type
```
### Prop 与 Type 的分工
| | `Prop` | `Type` |
| --- | --- | --- |
| 住在里面的是 | **命题** | **数据类型** |
| 它的项是 | **证明** | **值** |
| 例子 | `2 = 2`、`p ∧ q`、`∀ n, n + 0 = n` | `Nat`、`String`、`List α` |
| 项之间是否相关 | **无关**（proof irrelevance） | 相关 |
| 编译后 | **被擦除** | 保留 |
**Proof irrelevance（证明无关性）** 是 `Prop` 的关键特性：同一个命题的任意两个证明被认为**相等**。
```lean
example (p : Prop) (h1 h2 : p) : h1 = h2 := rfl
```
这在 `Type` 上不成立——`(1 : Nat)` 与 `(2 : Nat)` 显然不等。
为什么这样设计：**我们关心「命题是否成立」，不关心「怎么证的」**。这让编译器可以把所有证明**完全擦除**——形式化验证过的代码，运行时不带任何证明开销。
Proof irrelevance 有个实际后果：**不能对 `Prop` 里的项做模式匹配把信息带回 `Type`**（除少数受限的消去规则）。
想在数据层面区分情况，命题要放进 `Type`，或者用可判定性（`Decidable`），见[类型类](https://daiw.org/manual/lean4/typeclasses)。
## 函数类型
```lean
#check Nat → Nat -- Nat → Nat : Type
#check (fun n => n + 1) -- fun n => n + 1 : Nat → Nat
```
`→` 是**右结合**的：
```lean
#check Nat → Nat → Nat -- 等价于 Nat → (Nat → Nat)
```
所以多参数函数实际是**返回函数的函数**（柯里化）：
```lean
def add (a b : Nat) : Nat := a + b
#check add -- Nat → Nat → Nat
#check add 3 -- Nat → Nat ← 部分应用，合法
#eval add 3 4 -- 7
```
`add 3` 是一个「还差一个参数」的函数。这是函数式语言的标准行为，在 Lean 里用得非常多。
## 基本类型速览
```lean
#check (42 : Nat) -- 自然数（0, 1, 2, ...），无负数
#check (-5 : Int) -- 整数
#check (true : Bool)
#check ("hi" : String)
#check ('a' : Char)
#check ([1, 2, 3] : List Nat)
#check ((1, "a") : Nat × String) -- 积类型
#check (some 5 : Option Nat)
```
两个**必须立刻注意**的点。
### Nat 是任意精度且不会下溢
```lean
#eval (3 : Nat) - 5 -- 0 不是 -2
```
`Nat` 上的减法是**截断减法**：结果小于 0 时变 0。这不是 bug，是 `Nat` 的定义——它没有负数。
需要负数用 `Int`：
```lean
#eval (3 : Int) - 5 -- -2
```
**这是初学者最常踩的坑之一。** 涉及减法的证明里，`Nat` 的截断行为会让很多「显然成立」的等式**不成立**——比如 `a - b + b = a` 在 `a < b` 时左边是 `b` 而非 `a`。
正确的形式需要前提 `b ≤ a`（Mathlib 里对应 `Nat.sub_add_cancel`）。写涉及 `Nat` 减法的命题时，先问自己「会不会下溢」。
### Bool 与 Prop 是不同的东西
```lean
#check true -- Bool ← 一个【值】
#check True -- Prop ← 一个【命题】
#check (2 == 2) -- Bool
#check (2 = 2) -- Prop
```
| | `Bool` | `Prop` |
| --- | --- | --- |
| 是什么 | 数据类型，有 `true`/`false` 两个值 | 命题的宇宙 |
| 相等判断 | `==`（`BEq` 类型类） | `=`（命题相等） |
| 用于 | `if` 条件、可计算判断 | 定理陈述 |
两者靠 `Decidable` 连接——可判定的命题能自动转成 `Bool`：
```lean
#eval (2 = 2 : Bool) -- true，通过 Decidable 实例转换
```
`if` 的条件需要是 `Bool` 或**可判定的 `Prop`**。详见[类型类](https://daiw.org/manual/lean4/typeclasses)。
## variable 与 section
```lean
section
variable (n : Nat)
def addN (m : Nat) : Nat := m + n -- n 自动成为参数
end
```
`variable` 声明「后续定义可能用到的参数」——**只有实际用到时才会被加进签名**。写一组共享参数的定义时非常省事。
`section ... end` 限定作用域；`namespace ... end` 则同时加名字前缀：
```lean
namespace MyLib
def helper : Nat := 42
end MyLib
#check MyLib.helper
open MyLib in
#check helper -- open 之后可省略前缀
```
## 类型即规格
最后回到 Lean 的核心思想。看这个签名：
```lean
def myId {α : Type} (a : α) : α
```
**这个类型几乎唯一地确定了实现**：对任意类型 `α`，给一个 `α` 造一个 `α`——除了返回参数本身无事可做（这叫参数性 / 自由定理）。
类型携带的信息越多，实现的自由度越小、正确性保证越强。[依值类型](https://daiw.org/manual/lean4/dependent-types)把这一点推到极致——那时类型可以精确表达「返回长度为 n 的列表」这种规格。
下一篇：[函数](https://daiw.org/manual/lean4/functions)。