#compilers #语义分析
本页目录

类型系统

类型检查是编译器对程序的静态验证——在运行前证明不会出现类型错误。从简单的等式检查到 Hindley-Milner 推导到子类型与型变,再到泛型的单态化和类型擦除两条路线。

概述

符号表与作用域解决了"这个名字指哪个定义"。类型系统解决下一层:⁠这些名字的类型能不能合法组合⁠——x + y 的 x 和 y 能不能加?f(a) 的参数类型是否匹配?类型检查(type checking)是做判定的过程,类型推导(type inference)是自动补全省略的类型标注。这篇沿着"简单类型检查→HM 推导→子类型→泛型"的难度梯度,把类型的工程实现讲清楚。

类型检查:验证每棵子树

类型检查在 AST 上自底向上做:

typecheck(expr):
    match expr:
        Number(n) → Int
        Binary(op, left, right) →
            t_left = typecheck(left)
            t_right = typecheck(right)
            if op is '+' and t_left == Int and t_right == Int:
                return Int
            else:
                report_type_error("cannot add {t_left} and {t_right}")
        Variable(name) →
            lookup(name).type                 ← 从符号表拿类型
        Call(func, args) →
            t_func = typecheck(func)
            if t_func is not Function:
                error
            for (arg, param_type) in zip(args, t_func.params):
                t_arg = typecheck(arg)
                if t_arg != param_type:
                    error
            return t_func.return_type

骨架极简单:递归遍历 AST,每个节点验证其子节点的类型是否匹配该节点的类型规则。真正的复杂在类型表示⁠(类型的内部结构——函数、泛型、代数类型都怎么存)、⁠类型等价⁠(两个类型"一样"是什么意思——结构性等价 vs 名义等价)和泛型实例化⁠(List<T> 对于 T=Int 时的行为)。

类型表示

类型系统内部用类似 AST 的数据结构表示类型:

enum Type {
    Int,
    Float,
    Bool,
    String,
    Function(Vec<Type>, Box<Type>),    // params → return_type
    Struct(String, Vec<(String, Type)>),  // name + fields
    Enum(String, Vec<(String, Vec<Type>)>),  // name + variants
    TyVar(u32),                        // 类型变量, 用唯一 ID 标识 (O(1) 比较)
    Apply(Box<Type>, Vec<Type>),       // 泛型实例化: List<Int>
}

递归表示——Function 的参数和返回都是 Type, Apply(List, [Box<Type>]) 可以嵌套(如 Map<String, List<Int>>)。

类型等价:结构 vs 命名

两个类型何时"相同"?

  • 结构等价(structural equivalence):"长得一样就一样"。 struct { x: Int, y: Float } 与 struct { x: Int, y: Float } 是同一类型,即使它们在不同模块里定义。Go、TypeScript 用这个。代价:两个碰巧同构但语义完全不同的类型(如 Point{x,y} 和 Vector{x,y})被当作同一类型。
  • 命名等价(nominal equivalence):"名字一样才一样"。Point{x:Int, y:Float} 和 Vector{x:Int, y:Float} 是不同类型。Rust、Java、C++ 用这个。类型检查时比对的是一对类型的"结构化名称"而非字段逐个比对。名义等价更安全(防止语义混淆),但需要额外的机制表达类型约束(如 Rust 的 trait bound、Java 的 extends)来支持泛型推导。

Hindley-Milner 类型推导:不用写类型也能检查

HM 是 ML 系列语言(OCaml, Haskell)的类型推导基础,核心是 unification(合一):给定两个类型表达式,看看是否存在一组类型变量代换使它们相等。

推导过程 (伪代码):
  对 AST 中每个节点生成一个类型变量 (如 t1, t2, ...)
  对节点应用类型规则, 生成约束:
    Number(n)     → t == Int
    x + y         → t_x == Int, t_y == Int, t_result == Int
    if cond a b   → t_cond == Bool, t_a == t_b, t_result == t_a
  解约束集合 — unification:
    对于每个等式 t_i == t_j:
      如果 t_i 是未绑定的类型变量, 绑定 t_i → t_j
      如果 t_j 是未绑定的类型变量, 绑定 t_j → t_i
      如果两边都是具体类型(如 Int 和 Float), 检查相等 — 不等则 type error

Unification 是确定性的——遇到等式就按规则替换,不需要回溯重试。

HM 的限制:⁠多态只以 let 引入⁠(let-polymorphism——let id = fn x => x 里的 id 是多态的,在 let 绑定处引入泛化;而函数参数的多态性通过类型推导自动确定)。这是因为 HM 的 let-polymorphism 规则:只在 let 绑定处 Generalization,lambda 绑定的变量不被泛化。这确保了推导的可判定性⁠——Hindley-Milner 对 HM-valid 程序一定能在有限步骤内推导出主类型(principal type),不会陷入无穷。

子类型:可替代性原则

当 Dog <: Animal(Dog 是 Animal 的子类型)时,一个需要 Animal 的位置能接受 Dog。子类型给类型检查增加了"类型不是非黑即白的比较":

  • 协变(covariant):List<Dog> <: List<Animal> 如果 Dog <: Animal。只对只读结构安全——Java 的 List<? extends Animal>。
  • 逆变(contravariant):Fn(Animal) <: Fn(Dog)。函数参数是逆变的——一个能吃 Animal 的函数一定能吃 Dog(因为 Dog <: Animal,Animal 的集合涵盖 Dog)。反过来,Fn(Dog) 不能代替 Fn(Animal)——一个只能吃 Dog 的函数不能吃 Cat,而 Fn(Animal) 的位置可能传入 Cat。
  • 不变(invariant):Array<Dog> 和 Array<Animal> 无关。对可读写结构(数组是读写)必须不变——否则 arr: Array<Animal> 里放一个 Cat 后,已存在的 Array<Dog> 引用会认为所有元素都是 Dog,类型安全打破。

Rust 在实际的子类型使用中非常克制:⁠只有生命周期是子类型关系⁠('static <: 'a),其他类型全部是命名等价,没有结构子类型。

泛型:多态的不同实现

泛型(List<T>)在编译后如何生成代码?

单态化(monomorphization)

Rust、C++、Swift 用这个:为每种实际类型参数生成一份独立的机器码:

fn identity<T>(x: T) → T           // 泛型定义 (IR 中保留)
identity::<i32>(42)                 // 生成 identity_i32 的函数体
identity::<String>("hello")         // 生成 identity_String 的函数体

优点:零运行时开销(直接调用,无间接),对每种 T 可以独立优化(编译器看到 T=i32 时可以内联、常量折叠)。缺点:代码膨胀——每种 T 一份。Rust 在实践中对此限制不大,因为有充分的去重(同一 Option<i32> 只生成一次)。

类型擦除(type erasure)

Java、Scala、Kotlin 用这个:泛型只在编译时存在——运行时所有 List<T> 都是 List<Object>:

List<String> xs = ...;
String s = xs.get(0);     ← 编译器插入一个隐式 cast: (String) xs.get(0)

优点:只有一份代码,没有膨胀。缺点:原始类型不能做泛型(List<int> 不合法,必须用装箱的 List<Integer>);运行时有 cast 和装箱开销。

Trait/Typeclass:约束多态

泛型的参数需要被约束:说 T 必须是"能加的""能比较的""能打印的"。Rust 的 trait、Haskell 的 typeclass 是这种约束的表达。编译器的处理:

  • Rust:对 fn sum<T: Add>(xs: &[T]) → T,单态化时对每种 T 生成一份 sum,参数里的 Add::add 调用被静态分派——编译时已确定跳转到 T::add 的哪个实现。没有虚表查找。
  • 但当 trait 对象 dyn Add 出现时,编译器用 vtable(虚表)——一个存了函数指针的结构,运行时查找。

Trait solver 是 Rust 编译器中最复杂的组件之一。它的工作:给定 T: Add<Output = T> 和 Vec<T>,验证所有约束可满足——这本质上是一种 Prolog 式的逻辑编程(Chalk 库就是把 Rust 的 trait 规则翻译成 Prolog 规则求解)。

权衡与失败模式

  • 类型推导失败时的错误信息烂⁠:HM 的 unification 在失败时只知道"某两个类型不匹配",不知道"为什么"——产生"expected Foo, found Bar"但不说"你这里调的函数期望 Foo,你传的 x 是 Bar 因为三行前你赋了 Bar"。→ 现代编译器(如 Rustc)在推导过程中记录"约束来源",推导失败后沿着约束链回溯,生成消息诊断。
  • 推导不可判定⁠:如果在 HM 之外加入特性(如 GADT、type family、rank-N 多态),类型推导可能变得不可判定⁠——编译器可能永远推导下去。→ 加限制(Haskell 对 GADT 和 type family 要求类型标注;Rust 把推导限制在函数体内,不跨函数推导)。
  • 单态化导致的编译时间长⁠:C++ 模板和 Rust 泛型都可能引发编译时间爆炸 → 按需单态化(不生成所有理论上可能的实例)、去重(同一组合只生成一次)。

参考

  • Pierce: "Types and Programming Languages"(TAPL) — 类型理论的标准教材, 涵盖简单类型→子类型→多态→HM
  • Dragon Book: Chapter 6, Type Checking — 编译器里的类型检查实现
  • Rust Chalk: https://github.com/rust-lang/chalk — Rust trait solver 的逻辑编程实现

Keywords: type checking, type inference, Hindley-Milner, unification, type variable, principal type, subtyping, covariance, contravariance, invariance, monomorphization, type erasure, generic, trait, typeclass, vtable, static dispatch, dynamic dispatch, trait solver, nominal equivalence, structural equivalence, let-polymorphism

相关页面

© 2026 liz's doc