超越类型推断：Hindley-Milner 类型系统的现代实现与编译器前端设计

引言：类型推断的优雅与力量

在编程语言设计的历史长河中，很少有理论能像 Hindley-Milner（HM）类型系统这样，在学术优雅与工程实用性之间达到如此完美的平衡。从 1969 年 Roger Hindley 的开创性证明，到 1978 年 Robin Milner 在 LCF 中的实际实现，再到今天 Rust、Haskell、OCaml 等现代语言的编译器核心，HM 类型系统经历了半个多世纪的演化，依然保持着强大的生命力。

本文不满足于泛泛而谈"什么是类型推断"，而是深入到算法 W 的每一步实现细节、类型合一（Unification）的occur-check陷阱、泛型实例化的let-polymorphism机制，以及现代编译器如何在此基础上扩展出更高阶的类型系统。我们将亲手实现一个迷你HM类型推断器，理解每个设计决策背后的权衡。

第一部分：λ演算与简单类型基础

1.1 从 Untyped λ-Calculus 到 Simply Typed

类型系统的起点是 Curry-Howard 同构的核心直觉：命题即类型，证明即程序。在简单类型λ演算（STLC）中，我们为每个项赋予一个类型，并通过一组推导规则判断类型是否合法：

x : T ∈ Γ
----------- (T-Var)
Γ ⊢ x : T

Γ, x : T1 ⊢ t2 : T2
-------------------- (T-Abs)
Γ ⊢ λx.t1 : T1 → T2

Γ ⊢ t1 : T1 → T2    Γ ⊢ t2 : T1
------------------------------- (T-App)
Γ ⊢ t1 t2 : T2

STLC 虽然奠定了类型推导的基础，但要求用户为每个参数显式标注类型，这对于实际编程来说过于繁琐。HM 系统的突破在于：通过类型合一推断出最一般的类型，无需任何类型标注。

1.2 Type Scheme 与 Let-Polymorphism

HM 系统的核心创新之一是 let-polymorphism。在 let 绑定中，表达式的类型可以被泛化（Generalize），从而使同一绑定在不同使用点具有不同类型：

let id = λx.x in (id 42, id