开始之前：如何使用本教程

本教程面向这样一类读者：你已经写过一些程序，知道变量、函数、条件分支这些基本概念，但还没有系统学习过编程语言理论和类型系统。如果你读过一些函数式编程资料，或者听说过 Lambda 演算（Lambda Calculus）、类型推断（type inference）、子类型（subtyping）、线性类型（linear type）这些词，却总觉得概念零散、彼此之间缺少一条主线，那么这份教程就是为你准备的。

本教程的目标不是把所有高级主题一次讲完，而是建立一条适合自学的入门路径：

先学会用形式化的方式描述语言；
再理解 Lambda 演算这个最小计算模型；
然后在这个基础上引入类型系统；
最后逐步扩展到多态、子类型、类型推断和子结构类型等主题。

主要参考材料是：

Benjamin C. Pierce，《Types and Programming Languages》（TAPL）
Luca Cardelli，《Type Systems》
Pierce 编，《Advanced Topics in Types and Programming Languages》（ATAPL）的相关章节

不过，这份教程并不是这些材料的逐章翻译或摘抄，而是按“先建立直觉，再进入形式化”的思路重新组织的学习材料。

本教程与参考材料的关系

为了帮助你建立稳定主线，本教程对参考材料做了有意识的重组，而不是按原书目录逐章平移：

第 0–6 章主要围绕 TAPL 前半部分的核心路线展开，并吸收 Cardelli 对“类型系统是什么、它在防什么错误”的经典表述；
第 7–10 章继续引入多态、子类型、类型推断和子结构类型系统，但目标仍然是建立可自学的整体框架，而不是完整覆盖 TAPL、ATAPL 或 PFPL 的全部技术细节；
附录部分则承担三类任务：
- 统一术语与记号；
- 提供自检与学习建议；
- 展示若干值得了解、但不必作为正文前置条件的进阶主题。

因此，更准确地说，本教程是：

以经典教材为基础、按“语法 → 语义 → 类型 → 元理论”主线重新组织的一份入门教程。

你需要具备哪些基础？

编程基础

最低要求并不高。你只需要：

用过任意一门编程语言；
能看懂简单的函数定义和函数调用；
知道什么是变量、返回值、条件分支。

如果你完全没有编程经验，建议先补一个非常基础的入门教程。Python、JavaScript、TypeScript、Java、C、OCaml 都可以，语言本身并不重要，重要的是你对“函数接受输入并产生输出”这件事已经不陌生。

数学基础

本教程主要依赖离散数学里最基础的部分：

集合
函数
命题逻辑中的“且 / 或 / 蕴含”
简单的归纳法

不要求你先学完高等数学，也不要求你有逻辑学背景。第一章会把后续真正要用到的数学工具重新梳理一遍。

建议怎样阅读本教程？

本教程大致分成四个层次。

第一层：形式化工具

第零章：为什么需要类型系统
第一章：数学基础
第二章：形式文法与 BNF

这一部分的任务，是让你先接受一种思维方式：

讨论语言和类型系统时，我们不能只靠“差不多能懂”的自然语言描述，而要学会用明确的语法、规则和证明来表达。

第二层：计算模型

第三章：Lambda 演算基础
第四章：Lambda 演算中的计算

这一部分建立“程序如何计算”的最小模型。后面的大多数类型系统，都是在某种 Lambda 演算之上扩展出来的。

第三层：核心类型系统

第五章：类型系统核心概念
第六章：一阶类型系统

这一部分会回答最关键的问题：

什么叫“一个项具有某个类型”？
类型规则究竟在说什么？
为什么类型系统可以排除某些运行时错误？

第四层：重要扩展

第七章：二阶类型系统
第八章：子类型
第九章：类型推断
第十章：子结构类型系统

这里的主题彼此有关，但并不要求你一次完全掌握。第一次阅读时，建议把注意力放在每章的核心动机和最基本规则上；形式细节可以在第二遍阅读时慢慢回看。

阅读时应该重点抓什么？

每一章里通常会同时出现三类内容：

直觉：为什么要引入这个概念？它解决了什么问题？
形式化定义：它的语法、规则、定理是什么？
语言对照：在真实语言里，大概有什么相似做法？

如果你是第一次接触这类内容，建议优先确保自己能回答下面三个问题：

这个概念想解决什么问题？
它的最小形式定义是什么？
我能否手动做一个最基本的例子？

比如：

学 Lambda 演算时，能否自己算自由变量和替换？
学类型规则时，能否自己画一个简单的推导树？
学类型推断时，能否跟着一个例子生成约束并做合一？

和“看懂了”相比，能亲手做一个最小例子往往更重要。

本教程常用的记号与约定

完整的术语说明见附录A，完整的符号表见附录B。建议把这两个附录当作阅读时的常驻参考：

正文中首次引入的重要术语，通常会在括号中给出英文原文；
如果你一时忘了某个术语的边界，优先查附录A；
如果你一时忘了某个记号的读法和语境，优先查附录B；
如果你一时分不清“值 / 范式 / 卡住”“类型检查 / 类型推断”“Church 风格 / Curry 风格”这类术语差别，优先查附录A；
如果你一时忘了 $\Gamma \vdash t : T$ 、 $\longrightarrow$ 、 $\forall$ 、 $S <: T$ 这些记号怎么读、怎么用，优先查附录B。

这里先列出最常见、最值得提前熟悉的几个。

记号	读法	直觉含义
$λ x . t$	“lambda x 点 t”	一个以 `x` 为参数、函数体为 `t` 的函数
$t_{1} t_{2}$	“把 $t_{1}$ 应用于 $t_{2}$ ”	函数调用
$[x \mapsto s] t$	“把 $t$ 中的 `x` 替换成 `s`”	替换
$Γ ⊢ t : T$	“在环境 $Γ$ 下， $t$ 的类型是 $T$ ”	类型判断
$⟶$	“一步归约到”	单步计算
$\forall$	“对所有”	全称量化
$\exists$	“存在”	存在量化

其中要特别注意两点：

$\mapsto$ 的字面意思是“映射到”；在不同上下文里，它可能表示替换、环境中的绑定，或更一般的映射关系。
$\vdash$ 常读作“推出”或“可判断为”；它通常不是普通的逻辑蕴含，而是在某套规则系统内部的可推导关系。

最后一点建议

第一次读这类材料时，遇到公式多、符号多是正常的。不要把目标设成“第一次就完全掌握所有形式细节”，而是先建立下面这条主线：

语法定义了程序长什么样；语义定义了程序怎么计算；类型系统定义了哪些程序被允许；元理论则说明这些规则为什么可靠。

如果你能沿着这条主线把各章串起来，后面的细节就有落脚点了。

接下来，从第零章开始，我们先回答一个最自然的问题：

为什么程序语言需要类型系统？

Keyboard shortcuts

编程语言理论与类型系统入门