# 归纳类型与结构体
> inductive 的构造子与递归子、structure 与继承、参数与索引的区别、Nat 与 List 的真实定义。
- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/inductive-types
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）
## 归纳类型是地基
Lean 里几乎所有数据类型都是 `inductive` 定义的——包括 `Nat`、`List`、`Bool`，甚至逻辑联结词 `And`、`Or`。
```lean
inductive Color where
| red
| green
| blue
```
三个**构造子**，穷尽了 `Color` 的所有可能值。
```lean
#check Color.red -- Color.red : Color
#check Color -- Color : Type
```
带参数的构造子：
```lean
inductive Shape where
| circle (radius : Float)
| rect (width height : Float)
def area : Shape → Float
| .circle r => 3.14159 * r * r
| .rect w h => w * h
```
`.circle` 是 `Shape.circle` 的简写——**当类型能被推断时可以省略前缀**。这个点记法在模式匹配里用得极多。
## Nat 的真实定义
```lean
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat
```
**自然数不是机器整数，是一个归纳定义的链**：
```text
0 = Nat.zero
1 = Nat.succ Nat.zero
2 = Nat.succ (Nat.succ Nat.zero)
```
这解释了[上一章](https://daiw.org/manual/lean4/types-terms)的几件事：为什么 `Nat` 没有负数（构造子里没有）、为什么减法要截断（`0` 再减只能是 `0`）。
**性能上 Lean 不真的用一元表示。** 编译器对 `Nat` 有特殊处理，小数用机器整数、大数用 GMP。但**在证明层面它就是上面那个归纳定义**——归纳法证明依赖的正是这个结构。
这是 Lean 的一个典型模式：**语义定义要简洁可推理，运行时实现可以优化**，两者由编译器保证一致。
## List 的真实定义
```lean
inductive List (α : Type u) where
| nil : List α
| cons (head : α) (tail : List α) : List α
```
`[1, 2, 3]` 是 `1 :: 2 :: 3 :: []` 的语法糖，而 `::` 就是 `cons`、`[]` 就是 `nil`。
```lean
def length : List α → Nat
| [] => 0
| _ :: xs => 1 + length xs
```
**结构递归**：`xs` 比 `_ :: xs` 严格小，所以终止性自动通过。
## 递归子与归纳法
每定义一个 `inductive`，Lean 自动生成几个东西：
```lean
#check @Nat.rec -- 递归子（recursor），最基础的消去规则
#check @Nat.casesOn -- 分情况
#check @Nat.succ.inj -- 构造子单射性
#check @Nat.noConfusion -- 不同构造子不相等
```
`Nat.rec` 的类型（简化后）：
```text
{motive : Nat → Sort u}
→ motive Nat.zero
→ ((n : Nat) → motive n → motive n.succ)
→ (t : Nat) → motive t
```
读作：「要对所有 `Nat` 造出 `motive n`，只需给出：零的情况，以及从 `n` 的情况造 `n+1` 的情况。」
**这就是数学归纳法**。当 `motive n` 是命题时它是归纳证明，当 `motive n` 是数据时它是递归定义——**同一条规则**。
这是「命题即类型」的第一个具体例子，[第 2 部分](https://daiw.org/manual/lean4/propositions-as-types)会全面展开。
日常写证明用 `induction` tactic 而不是直接调 `Nat.rec`，见[归纳证明](https://daiw.org/manual/lean4/induction-proofs)。
## structure
只有一个构造子的归纳类型，用 `structure` 更方便：
```lean
structure Point where
x : Float
y : Float
```
Lean 自动生成：
```lean
#check Point.mk -- Float → Float → Point 构造子
#check Point.x -- Point → Float 投影
#check Point.y
```
三种构造写法：
```lean
def p1 : Point := ⟨1.0, 2.0⟩ -- 匿名构造子
def p2 : Point := Point.mk 1.0 2.0 -- 显式
def p3 : Point := { x := 1.0, y := 2.0 } -- 具名字段
```
**具名字段形式最可读**，字段多时尤其如此。
### 更新语法
```lean
def moved : Point := { p1 with x := 5.0 }
```
「除了 `x` 改成 5.0，其余同 `p1`」。函数式语言的标准做法——不修改原值，返回新值。
### 自定义构造子名与默认值
```lean
structure Config where
mk :: -- 自定义构造子名
host : String := "localhost" -- 默认值
port : Nat := 8080
#eval (({} : Config)).port -- 8080，全用默认值
#eval ({ port := 3000 } : Config).host -- "localhost"
```
## 结构体继承
```lean
structure Point3D extends Point where
z : Float
def q : Point3D := { x := 1, y := 2, z := 3 }
#eval q.x -- 1.0，继承来的字段直接可用
#eval q.toPoint -- 自动生成的向上转换
```
`extends` 生成 `toPoint` 投影。可以继承多个：
```lean
structure A where a : Nat
structure B where b : Nat
structure C extends A, B where c : Nat
```
这套机制正是[类型类](https://daiw.org/manual/lean4/typeclasses)层次结构的基础——Mathlib 里 `Monoid extends Semigroup, One` 之类的代数结构层次全靠它。
## 参数 vs 索引
这是归纳类型里**最需要理解的区别**。
```lean
-- α 是【参数】：在 : 左边，所有构造子里保持不变
inductive MyList (α : Type) where
| nil : MyList α
| cons : α → MyList α → MyList α
-- n 是【索引】：在 : 右边，不同构造子可以给不同的值
inductive Vec (α : Type) : Nat → Type where
| nil : Vec α 0
| cons : α → Vec α n → Vec α (n + 1)
```
| | 参数（parameter） | 索引（index） |
| --- | --- | --- |
| 位置 | `:` **左边** | `:` **右边** |
| 各构造子中 | **必须相同** | **可以不同** |
| 作用 | 泛型 | **让类型携带信息** |
`Vec α n` 是**长度写进类型的列表**：
```lean
def v : Vec Nat 3 := .cons 1 (.cons 2 (.cons 3 .nil))
-- def bad : Vec Nat 2 := .cons 1 (.cons 2 (.cons 3 .nil)) ← 类型错误！
```
**类型检查器会拒绝长度不对的向量**。这是依值类型的威力——把不变量编码进类型，编译期就排除一整类错误。
它的实际收益：
```lean
def head : Vec α (n + 1) → α
| .cons a _ => a
```
`head` 的类型要求输入长度**至少为 1**，所以**不需要处理空列表的情况**——空表根本传不进来。对比 `List.head` 必须返回 `Option` 或要求一个「非空」的证明。
[依值类型那一章](https://daiw.org/manual/lean4/dependent-types)会继续展开。
## 相互递归
```lean
mutual
inductive Tree (α : Type) where
| node : α → Forest α → Tree α
inductive Forest (α : Type) where
| nil : Forest α
| cons : Tree α → Forest α → Forest α
end
```
`mutual ... end` 包住相互引用的定义。函数也可以：
```lean
mutual
def isEven : Nat → Bool
| 0 => true
| n + 1 => isOdd n
def isOdd : Nat → Bool
| 0 => false
| n + 1 => isEven n
end
```
## deriving
```lean
inductive Color where
| red | green | blue
deriving Repr, DecidableEq, Inhabited
```
自动派生常用实例：
| 派生 | 得到什么 |
| --- | --- |
| `Repr` | 能被 `#eval` 打印 |
| `DecidableEq` | 相等性可判定，可用 `==` 与 `if` |
| `Inhabited` | 有默认值（`default`） |
| `BEq` | 布尔相等 |
| `Hashable` | 可做哈希表的键 |
**`#eval` 一个自定义类型报错「no `Repr` instance」时，加 `deriving Repr` 即可。** 这是最常见的新手卡点之一。
## 一个综合例子
```lean
inductive Expr where
| lit : Int → Expr
| add : Expr → Expr → Expr
| mul : Expr → Expr → Expr
| neg : Expr → Expr
deriving Repr
def eval : Expr → Int
| .lit n => n
| .add a b => eval a + eval b
| .mul a b => eval a * eval b
| .neg a => -eval a
def e : Expr := .add (.lit 3) (.mul (.lit 4) (.neg (.lit 2)))
#eval eval e -- -5
```
一个表达式求值器，20 行不到，且**穷尽性由编译器保证**——加一个新构造子，所有 `match` 都会报错提醒你处理。
而且我们可以**对它证明定理**：
```lean
theorem eval_neg (a : Expr) : eval (.neg a) = -eval a := rfl
```
这是 Lean 的价值所在：**同一段代码既能跑，又能证**。
下一篇：[类型类](https://daiw.org/manual/lean4/typeclasses)。