---
title: 类型系统
url: https://doc.liz6.com/compilers/03-semantic-analysis/02-type-systems
locale: zh
area: compilers
tags:
- compilers
- 语义分析
date: 2026-06-30
modified: 2026-07-16
description: 类型检查是编译器对程序的静态验证——在运行前证明不会出现类型错误。从简单的等式检查到 Hindley-Milner 推导到子类型与型变,再到泛型的单态化和类型擦除两条路线。
---

# 类型系统

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

## 概述

[符号表与作用域](/compilers/03-semantic-analysis/01-symbol-tables-and-scopes.md)解决了"这个名字指哪个定义"。类型系统解决下一层:**这些名字的类型能不能合法组合**——`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 的数据结构表示类型:

```rust
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*