到第 04 篇为止，STLC 已经把直觉主义命题逻辑全部装进类型系统。但日常数学和工程里大量命题超出命题逻辑范围：“对任意自然数 n，n + 0 = n”、“对任意列表 xs，reverse (reverse xs) = xs”。这些命题都带量词，命题逻辑写不出来。

让类型系统能表达量词的关键扩展叫依值类型（dependent types）：允许类型本身依赖值。一旦允许类型依赖值，∀ x : A, P(x) 就能翻译成"对每个 x : A 都给出 P(x) : Prop 的函数"——这条函数本身有依值的返回类型。

本篇说清楚依值函数 Π、依值积 Σ、Vec n α 这种经典例子，并把它们与一阶逻辑的 ∀、∃ 精确对应起来。

STLC 卡在哪里

STLC 里函数类型形如 τ1 → τ2，τ2 必须是与 τ1 完全无关的、固定的类型。例如可以写：

1
length : List Nat → Nat

但写不出：

1
replicate : (n : Nat) → Vec n Nat

后者的返回类型 Vec n Nat 依赖输入 n。STLC 的 → 不允许这件事。

类似地，命题层面 STLC 能写：

1
even_is_decidable : Bool        -- 一个固定结果

但写不出：

1
even_or_odd : (n : Nat) → Even n + Odd n

后者要求"返回类型 Even n + Odd n 依赖输入 n"。

依值类型把这条限制取消：

  • 把 → 升级为 (x : A) → B(x)，记作 Π x : A. B(x)。
  • 把 × 升级为 (x : A) × B(x)，记作 Σ x : A. B(x)。

这两条扩展之后，类型系统第一次能直接谈"对所有的"和"存在某个"。

Π 类型：依值函数

依值函数类型 Π x : A. B(x) 的元素是函数 f，对每个输入 a : A，f a 的类型是 B(a)。

写在 Lean 4 里：

1
2
3
4
-- 一个返回 n 个 0 的列表
def replicate_zero : (n : Nat) → Vector Nat n
  | 0     => Vector.nil
  | n + 1 => Vector.cons 0 (replicate_zero n)

这里：

  • 输入是 n : Nat。
  • 输出类型 Vector Nat n 依赖输入 n。replicate_zero 3 的类型是 Vector Nat 3，replicate_zero 5 的类型是 Vector Nat 5。

把 n 和 Vector Nat n 之间的依赖关系看清楚之后，Π 类型就不再神秘：它就是"返回类型可以提到输入"的函数类型。

Π 类型对应 ∀

Curry-Howard 同构在依值层的形式：

逻辑端 类型端 项构造 项消费
∀ x : A, P(x) Π x : A, P(x) fun x => proof_of_P(x) f a : P(a)

例：证明"任意自然数加 0 等于自身"。

1
2
theorem add_zero (n : Nat) : n + 0 = n := by
  rfl

这里 add_zero 的类型是 (n : Nat) → n + 0 = n，即 ∀ n : Nat, n + 0 = n。它的"证明"是一个依值函数：对每个 n，返回一个类型为 n + 0 = n 的项。Lean 内部 Nat.add 是按第二参数递归定义的，所以 n + 0 直接定义性等于 n，证明就是 rfl（反身性）。

这条定理调用时：

1
2
#check add_zero 3       -- : 3 + 0 = 3
#check add_zero 100     -- : 100 + 0 = 100

返回类型按调用时实参 n 变化。这是 STLC 里不存在的能力。

Σ 类型：依值积

依值积类型 Σ x : A. B(x) 的元素是一对 ⟨a, b⟩，其中 a : A，b : B(a)。这是"存在性证明"的精确形态：给出见证 a 与该见证满足性质的证明 b。

写在 Lean 4 里（用 Sigma 或 Exists）：

1
2
3
4
5
def find_zero_in_singleton : Σ n : Nat, n = 0 :=
  ⟨0, rfl⟩

theorem exists_zero : ∃ n : Nat, n + 1 = 1 :=
  ⟨0, rfl⟩

Sigma 与 Exists 在 Lean 4 里几乎是同一个机制，区别仅在 Prop 与 Type 宇宙。两种写法的"证明形态"都一样：一对 ⟨见证, 性质的证明⟩。

Σ 类型对应 ∃

逻辑端 类型端 项构造 项消费
∃ x : A, P(x) Σ x : A, P(x) ⟨a, proof⟩ .fst（取见证）、.snd（取证明）

注意 BHK 解释下"存在"必须给见证。Σ 类型把这一要求强制到类型层：要构造 Σ n : Nat. P n，必须给出具体的 n，没有"非构造性存在"的逃生通道。

古典数学里有"非构造性存在证明"（例如鸽笼原理推出某种染色存在但不告诉你哪种）。在 Lean 这种系统里，要写出这种证明要么改用 Classical.choice 公理（属于"主动加坏公理"，第 09 篇会讨论），要么改写成构造性形式。

Vec n α：把不变量编进类型

依值类型最常被引用的工程例子是长度索引列表 Vec n α：长度 n 出现在类型里。

Lean 4 里：

1
2
3
4
5
6
7
8
9
10
inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

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

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

看几件 STLC 做不到的事：

  1. head 拒绝空列表，编译期保证。head 的参数类型是 Vec α (n + 1)，意味着长度至少是 1。传 Vec.nil（类型为 Vec α 0）进去时，类型直接不匹配，编译失败。运行时不会出现"空列表取首元素"的崩溃。
  2. append 的长度由类型守住。两个长度 m、n 的向量拼起来长度必然 m + n，这件事写在返回类型里。任何把 append 实现错（少接一个元素、多接一个元素）都通不过类型检查。
  3. 不变量被编译器保证，不靠运行时断言。STLC 或 Java 里"列表长度"是运行时数据，要在编译期检查需要换一套类型系统。依值类型直接让长度成为类型的一部分。

工程对照：Rust 的 const generics（[T; N]）是这种思想的极弱版本（N 必须是常量），Idris / Agda / Lean 4 / F* 是完整版。日常 Java / Python / TypeScript 都没有这个能力。

Π 与 Σ 把命题与数据统一

读到这里，会发现 Π 与 Σ 同时在干两件事：

用法 解读为命题 解读为数据
Π x : A, B(x) “对所有 x，B(x) 成立” “给定 x 产出依赖 x 的值”
Σ x : A, B(x) “存在 x 使 B(x) 成立” “一对：见证与对应数据”

Lean 4 / Coq / Agda 把这两件事用同一套机制处理：Π 是函数类型的依值化，Σ 是积类型的依值化。命题端的 ∀/∃ 与数据端的依值函数/依值积本质同一——这就是为什么形式化系统能让"定理"和"算法"在同一个文件、同一个语法、同一个类型检查器里被等价对待。

CompCert 的核心思路正是这件事：

  • 编译器是一段程序（数据视角）。
  • 编译器的正确性是一条 ∀ src : Source, Behavior(src) ⊆ Behavior(compile src) 的命题（命题视角）。
  • 在 Coq 里这条命题与那段编译器在同一个语法层共存，类型检查器同时验证"程序能跑"和"程序符合规约"。

表达力的代价

依值类型不是免费的。把类型与值混在一起带来三件事：

  1. 类型相等性变难判断。STLC 里 Arrow(A, B) = Arrow(A, B) 只看结构。依值系统里 Vec α (3 + 0) 与 Vec α 3 需要先把 3 + 0 归约到 3 才能判等。类型检查需要内嵌求值器。
  2. 强归一化必须显式守住。一旦能写无限递归，类型检查就可能不停。Lean / Coq / Agda 都要求递归良基，每条 def 都被自动检查终止性，不通过就拒绝接受。
  3. 宇宙层级避免悖论。如果允许 Type : Type，会出现 Girard 悖论（依值版本的 Russell 悖论）。Lean 4 引入宇宙层级 Type 0、Type 1、…，每一层只能"装"低一层的类型，避免自指。

这三件代价的工程含义：

  • 类型检查器内核要内嵌求值器与归一化器。
  • 递归定义需要带终止性证据。
  • 写日常代码时大部分宇宙处理可由 Lean 自动推断；只有写元理论或库基础时才会撞到宇宙层级。

用 Python 模拟依值索引

Python 没有依值类型，但可以用运行时类型工厂模拟"长度索引列表"。这段代码无法在编译期保证长度，但能展示"类型依赖值"的形态：

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
from typing import Generic, TypeVar, List

T = TypeVar("T")


def make_vec_type(n: int):
    class _Vec(Generic[T]):
        expected_len = n

        def __init__(self, items: List[T]):
            if len(items) != n:
                raise TypeError(f"expected length {n}, got {len(items)}")
            self.items = items

        def __repr__(self):
            return f"Vec[{n}]({self.items})"

    _Vec.__name__ = f"Vec_{n}"
    return _Vec


Vec3 = make_vec_type(3)
v: Vec3[int] = Vec3([10, 20, 30])
print(v)
# v_bad: Vec3[int] = Vec3([10])   # 运行时报错

输出：

1
Vec[3]([10, 20, 30])

Vec3 是由值 3 派生出来的类型——类型依赖值。区别在于 Python 把检查留到运行时，而 Lean / Coq / Agda 把同一件事提前到编译时。

依值类型系统的本质，是把这种"类型工厂"做成编译期一等公民，并与类型检查器配合保证全部约束在编译时成立。

模式提炼

模式 内容
类型依值 类型可以提到值——这是从命题逻辑跨到一阶逻辑的关键
Π 即 ∀ 依值函数是全称命题的证明形态
Σ 即 ∃ 依值积是存在命题的证明形态
不变量编进类型 Vec n α 让长度成为类型的一部分，编译期就守住
表达力换代价 类型相等性需要求值，递归必须良基，宇宙避免悖论

给读者的练习

  1. 在 Lean 4 里写出 Vec 的 map：(α → β) → Vec α n → Vec β n。注意长度类型必须守住。
  2. 用 Σ n : Nat, n > 5 构造一个见证，并思考为什么这条命题在直觉主义下平凡可证。
  3. 想清楚：(n : Nat) → Vec α n 与 Vec α (?n : Nat) 是不是同一件事？为什么不是？
  4. 拓展：Java / Rust / TypeScript 里有没有任何"类型依赖值"的痕迹？它们停在了哪里？

衔接到下一篇

本篇把表达力从命题逻辑拉到一阶逻辑。但日常数学还需要在自然数、列表、树这些归纳数据上做证明，证明往往需要归纳法。

下一篇引入归纳类型：怎样用 inductive 定义一族数据，怎样把模式匹配作为分情况讨论，以及为什么"归纳法"和"递归函数"在依值类型系统里是同一件事。再下一篇就可以开始动 Lean 4 真本地环境，写读者自己的第一条证明。

参考资料