# 依值类型

> Pi 类型与 Sigma 类型、类型依赖值的三种典型用法，以及依值模式匹配与「绿色黏液」问题。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/dependent-types
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## 核心概念：类型可以依赖值

普通类型系统里，类型和值是两个世界：`List Nat` 是类型，`[1,2,3]` 是值，类型不知道值的任何信息。

**依值类型打破这道墙**——类型里可以出现值：

```lean
def Vec (α : Type) (n : Nat) : Type := { xs : List α // xs.length = n }
```

`Vec Nat 3` 与 `Vec Nat 4` 是**不同的类型**，区别只在那个数字。

[前面](https://daiw.org/manual/lean4/inductive-types)见过的归纳版本更常用：

```lean
inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)
```

## Pi 类型：依值函数

普通函数类型 `α → β` 里，`β` 不能提到参数。**Pi 类型**可以：

```lean
def replicate : (n : Nat) → α → Vec α n
  | 0,     _ => .nil
  | n + 1, a => .cons a (replicate n a)
```

看这个类型：`(n : Nat) → α → Vec α n`。**返回类型里出现了参数 `n`**——返回的向量长度由第一个参数决定。

写法上：

```lean
(n : Nat) → Vec α n        -- 显式 Pi
∀ (n : Nat), Vec α n       -- 同一个东西的另一种写法
```

<Callout type="info">
  **`→` 是 Pi 类型的特例。** `α → β` 只是 `(_ : α) → β` 的简写——参数没被用到，所以名字可以省。

  同样，**`∀` 与 `→` 在 Lean 里是同一个东西**。写 `∀ x, P x` 与写 `(x : α) → P x` 完全等价，只是习惯上命题用 `∀`、数据用 `→`。这个统一是「命题即类型」的直接后果，[下一章](https://daiw.org/manual/lean4/propositions-as-types)展开。
</Callout>

## Sigma 类型：依值对

```lean
#check Sigma          -- (α : Type u) → (α → Type v) → Type (max u v)
#check @Subtype       -- {α : Sort u} → (α → Prop) → Sort (max 1 u)
```

**普通积** `α × β`：两个独立的值。
**Sigma 类型** `Σ x : α, β x`：第二个分量的**类型依赖第一个分量的值**。

```lean
def someVec : Σ n : Nat, Vec Nat n := ⟨3, .cons 1 (.cons 2 (.cons 3 .nil))⟩
```

「一个长度，以及那个长度的向量」——长度被打包进去了。

### Subtype：带性质的值

更常用的是 `Subtype`（`Prop` 版的 Sigma）：

```lean
def PosNat := { n : Nat // n > 0 }

def three : PosNat := ⟨3, by decide⟩

#eval three.val        -- 3
#check three.property   -- three.val > 0
```

`{ x : α // p x }` 读作「满足 `p` 的 `α`」。它是一个**值 + 该值满足性质的证明**的配对。

由于 [proof irrelevance](https://daiw.org/manual/lean4/types-terms)，证明部分在运行时被完全擦除——`PosNat` 的运行时表示就是一个 `Nat`，**零开销**。

Mathlib 里到处都是这个模式：

```lean
-- 非空集合、可逆元、连续函数……都是「值 + 性质」
```

## 三种典型用法

### 1. 把不变量编码进类型

```lean
def head : Vec α (n + 1) → α
  | .cons a _ => a
```

**类型要求非空，所以不需要处理空的情况**。对比：

```lean
def List.head? : List α → Option α     -- 必须返回 Option
def List.head! : List α → α            -- 会 panic
```

前者调用方要处理 `none`，后者可能崩。依值版本**在编译期就排除了空表**。

### 2. 让长度参与运算

```lean
def append : Vec α m → Vec α n → Vec α (m + n)
  | .nil,       ys => ys
  | .cons x xs, ys => .cons x (append xs ys)
```

**返回类型自动是 `m + n`**——类型检查器验证了「拼接后长度等于两者之和」。这个性质不需要另外写定理证明，它写在类型里。

### 3. 按值决定类型

```lean
def NatOrString (b : Bool) : Type :=
  match b with
  | true  => Nat
  | false => String

def get : (b : Bool) → NatOrString b
  | true  => 42
  | false => "hello"
```

**返回什么类型由参数决定**。这在建模协议、配置、DSL 时很有用。

## 依值模式匹配

匹配一个分支时，**其他参数的类型可能随之精化**：

```lean
def zip : Vec α n → Vec β n → Vec (α × β) n
  | .nil,       .nil       => .nil
  | .cons a as, .cons b bs => .cons (a, b) (zip as bs)
```

注意**只需要两个分支**：两个向量长度都是 `n`，所以「一个空一个非空」的情况**类型上就不可能**——Lean 知道这一点，不要求你处理。

这就是依值类型的实际收益：**穷尽性检查变强了**。

## 「绿色黏液」问题

依值类型的经典困难：

```lean
-- 想证明 append 的结合律，但类型对不上
-- append (append xs ys) zs : Vec α ((m + n) + k)
-- append xs (append ys zs) : Vec α (m + (n + k))
```

`(m + n) + k` 与 `m + (n + k)` **在数学上相等，但不是同一个项**。所以这两个表达式**类型不同**，连「相等」都无法直接陈述。

解法有几种：

**一、`Nat.add_assoc` + `▸`（cast）**

```lean
-- 用等式把类型「搬」过去，但表达式会变得很难看
```

**二、`HEq`（异构相等）**——允许比较不同类型的项，但用起来很痛苦。

**三、避免它。** 实践中的主流做法：**不要把太多信息塞进类型**。

<Callout type="warn">
  **这是依值类型的核心权衡，也是初学者最容易过度使用的地方。**

  把长度写进 `Vec` 看起来很美，但一旦要对它做非平凡的证明，就会陷入 cast 与 `HEq` 的泥潭（社区叫这个现象 `dependent type hell` 或 `green slime`）。

  **Mathlib 的实际选择是：大部分时候用普通 `List` + 单独的长度引理**，而不是 `Vec`。信息放在类型里还是放在旁边的定理里，是一个工程判断，不是「越依值越好」。

  经验法则：**索引应该是「构造时自然产生、之后不参与复杂运算」的量**。参与算术的量放进类型往往得不偿失。
</Callout>

## 依值类型与代码生成

```lean
def replicate : (n : Nat) → α → Vec α n
```

运行时 `Vec α n` 的表示就是一个列表——**类型里的 `n` 被完全擦除**。依值类型的检查全在编译期，不带运行时开销。

这与 [proof irrelevance](https://daiw.org/manual/lean4/types-terms) 是同一套机制的两面：**用于验证的信息不进入运行时**。

## 一个完整例子

类型安全的有限下标访问：

```lean
def Vec.get : Vec α n → Fin n → α
  | .cons a _,  ⟨0,     _⟩ => a
  | .cons _ as, ⟨i + 1, h⟩ => as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩
```

`Fin n` 是「小于 n 的自然数」——它本身就是一个 Subtype 式的依值类型：

```lean
structure Fin (n : Nat) where
  val  : Nat
  isLt : val < n
```

于是 `Vec.get` **不可能越界**：下标的类型保证了它在范围内，函数不需要（也无法）返回 `Option`。

```lean
def v : Vec Nat 3 := .cons 10 (.cons 20 (.cons 30 .nil))
#eval v.get ⟨1, by decide⟩      -- 20
-- #eval v.get ⟨5, by decide⟩   -- 编译失败：无法证明 5 < 3
```

**越界访问在编译期被拒绝**，而不是运行时 panic。这是依值类型最有说服力的应用场景。

下一篇：[命题即类型](https://daiw.org/manual/lean4/propositions-as-types)——全书的转折点。