依值类型

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

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

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

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

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

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

前面见过的归纳版本更常用：

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

Pi 类型：依值函数

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

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

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

写法上：

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

→ 是 Pi 类型的特例。 α → β 只是 (_ : α) → β 的简写——参数没被用到，所以名字可以省。

同样，∀ 与 → 在 Lean 里是同一个东西。写 ∀ x, P x 与写 (x : α) → P x 完全等价，只是习惯上命题用 ∀、数据用 →。这个统一是「命题即类型」的直接后果，下一章展开。

Sigma 类型：依值对

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

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

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

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

Subtype：带性质的值

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

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，证明部分在运行时被完全擦除——PosNat 的运行时表示就是一个 Nat，零开销。

Mathlib 里到处都是这个模式：

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

三种典型用法

1. 把不变量编码进类型

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

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

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

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

2. 让长度参与运算

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

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

3. 按值决定类型

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

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

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

依值模式匹配

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

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 知道这一点，不要求你处理。

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

「绿色黏液」问题

依值类型的经典困难：

-- 想证明 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）

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

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

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

这是依值类型的核心权衡，也是初学者最容易过度使用的地方。

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

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

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

依值类型与代码生成

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

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

这与 proof irrelevance 是同一套机制的两面：用于验证的信息不进入运行时。

一个完整例子

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

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 式的依值类型：

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

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

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。这是依值类型最有说服力的应用场景。

下一篇：命题即类型——全书的转折点。

本页目录