开始阅读

类型系统论文难读，通常不是因为某一个概念特别神秘，而是因为论文会同时压缩三层内容：

1. 对象语言：被检查的程序长什么样；
2. 元语言：我们用什么数学记号描述检查过程；
3. 算法：编译器实际上维护哪些状态、按什么顺序运行。

例如下面只有一行：

$$\frac{\Gamma, x : \tau_1 \vdash e : \tau_2} {\Gamma \vdash \lambda x.e : \tau_1 \to \tau_2} \;(\mathrm{T-Abs})$$

论文作者看到的是一个熟悉的“函数规则”。第一次接触的人却要同时回答：

• $\Gamma$ 是什么？
• 逗号是在拼列表、集合，还是逻辑上的“并且”？
• 冒号是不是变量声明？
• $\vdash$ 为什么不是普通箭头？
• 横线表示除法吗？
• $\lambda x.e$ 是哪种语言的代码？
• $\tau_1 \to \tau_2$ 为什么有两个类型？

本教程的任务就是把这些被论文省略的步骤重新展开。

我们最终想理解什么

先看两个程序员熟悉的问题。

问题一：完全不写类型，编译器能知道多少？

let id = fn x => x
let answer = id(42)
let flag = id(true)

id 同时被用在 Int 和 Bool 上。HM 要解释：

• 怎样得到 id 的类型 forall a. a -> a；
• 为什么 a 在两次调用中可以分别变成 Int 和 Bool；
• 为什么这个类型是“最一般”的，而不是碰巧猜出来的。

问题二：上下文已经知道类型时，为什么还要重新猜？

let inc: Int -> Int = fn x => x + 1

右侧匿名函数单独出现时，参数 x 没有类型标注；但左侧已经告诉我们整个表达式应当是 Int -> Int。双向类型检查会把 Int 从外向内传给 x，而不是先为所有东西生成未知量，再全局求解。

这两种方法不是简单的竞争关系：

• HM 擅长在 rank-1 let 多态范围内做完整的全局推断；
• 双向检查擅长让信息沿语法树的合适方向流动，用少量标注控制更丰富的类型特性；
• 实际语言经常把二者的思想组合起来。

阅读路线

如果你从未读过类型规则，请顺序阅读：

1. 从 TypeScript 与 Rust 已知经验出发：先把熟悉语法映射到理论问题；
2. 类型理论发展路线：知道每一种关键理论试图解决什么；
3. 先学会读公式：掌握全文的“标点符号”；
4. Lambda 演算与简单类型：补齐绑定、替换、求值与 STLC 地基；
5. 类型系统的基本任务：建立声明式规则与算法的区别；
6. 和、积与代数数据类型：从 Rust enum 与 TypeScript 联合看数据规则；
7. 多态地图：区分参数多态、重载、子类型、System F 与 rank；
8. 子类型与型变：理解结构兼容、协变与函数参数逆变；
9. Hindley–Milner 类型系统：理解 let 多态与主类型；
10. 替换、约束与合一：理解推断引擎的核心工具；
11. Algorithm W：把前面的概念组装成算法；
12. 双向类型检查：理解两种判断方向；
13. HM 与双向系统怎样配合：建立全景图；
14. System F：把类型抽象、类型应用写进核心语言；
15. GADT 与存在类型：理解构造器索引、分支精化与表示隐藏；
16. 精化类型：把路径事实变成逻辑谓词和验证条件；
17. 依赖类型：学习 Π、Σ、等式与类型中的计算；
18. 渐进类型：理解动态未知、cast、blame 与渐进保证；
19. 线性与仿射类型：从 Rust move/borrow 走到资源上下文；
20. 效果系统：让函数类型同时描述返回值与计算行为；
21. 实现指南：把纸面规则翻译成代码。

前 13 章构成主线，已经足够建立 HM 与双向类型检查的完整入门理解。第 14–20 章是“HM 之后”的分支路线：每章顶部都会列出前置知识；第一次阅读可以按兴趣选择，不需要一次学完。

若主要背景是 TypeScript，建议主线后先读渐进类型与精化类型；若主要背景是 Rust，建议先读线性/仿射类型、GADT 与效果系统；若目标是证明助手，再走 System F → GADT → 依赖类型。

正文中带虚线的关键词可以点击，解释会在右侧术语栏展开，不会把当前章节顶走。如果你正在读论文，也可以打开完整的术语与符号速查。

每个新增抽象都会尽量经过四步：

1. 先给 TypeScript 或 Rust 代码；
2. 再删掉工程细节，留下最小语言；
3. 再介绍判断式与推导规则；
4. 最后回到编译器实现和语言边界。

三个重要提醒

“类型系统”不等于“类型推断算法”

类型系统通常先用规则描述：哪些程序可以被赋予哪些类型。算法则决定如何机械地找到推导或报告失败。两者可能使用相似公式，但目的不同。

同一个符号在不同论文里可能有不同含义

例如 $\Gamma$ 通常是上下文，但上下文里究竟只放变量类型，还是还放类型变量、存在变量、作用域标记，要看论文定义。读规则前永远先读语法和判断式定义。

本教程先用小语言隔离核心问题

真实语言还有子类型、重载、可变引用、类型类、效果、GADT、模块系统等机制。它们会改变推断边界。先理解小系统，之后才能判断复杂规则究竟增加了哪一层能力。