01 / 导读
导读
引用
Pierce, B. C. (2002). Types and Programming Languages. The MIT Press.
章节概要
全书分六个部分，共三十二章，前有引言（第 1 章）和一章简短的数学预备知识（第 2 章），后有两个附录：部分习题解答（约 70 页）和记号约定。若干章是实现章节，标题均为“An ML Implementation of ……”（某某的 ML 实现），各自配合其前面的理论章节。
第1–2章：引言；数学预备知识
第 1 章讨论计算机科学中的类型是什么、类型系统有什么用、它们与语言设计的关系，并附简史和延伸阅读。第 2 章回顾集合、关系与函数、有序集、序列和归纳。
第一部分：无类型系统（第3–7章）
第 3 章“无类型算术表达式”以一个极小的语言介绍语法、对项的归纳、语义风格和求值。第 4 章是它的 ML 实现。第 5 章“无类型 λ 演算”讲基础、用 λ 演算编程和形式定义；第 6 章给出项的无名表示，涉及平移与代换；第 7 章用 ML 实现 λ 演算。
第二部分：简单类型（第8–14章）
第 8 章“有类型算术表达式”引入类型和类型关系，并把安全性表述为进展性加保持性。第 9 章“简单类型 λ 演算”加入函数类型，讨论类型关系的性质、Curry–Howard 对应、擦除与可类型性，以及 Curry 式与 Church 式两种表述；第 10 章实现类型检查器。第 11 章“简单扩展”加入基本类型、unit、顺序执行、类型标注、let 绑定、对、元组、记录、和类型、变体类型、一般递归与列表。第 12 章“规范化”证明简单类型的规范化。第 13 章“引用”和第 14 章“异常”分别为语言加入可变状态（含存储类型和安全性证明）以及异常的抛出与处理。
第三部分：子类型（第15–19章）
第 15 章“子类型”讲包容、子类型关系、它与类型规则的相互作用、顶类型与底类型、与其他特性的结合、强制转换语义，以及交类型与并类型。第 16 章给出元理论（算法性子类型与类型判定、join 与 meet）；第 17 章是 ML 实现。第 18、19 章是案例研究：“命令式对象”由该演算构造类、self 和开放递归等面向对象特性；“Featherweight Java”是一个核心演算，也用来讨论名义类型系统与结构类型系统。
第四部分：递归类型（第20–21章）
第 20 章通过例子、形式化和子类型引入递归类型。第 21 章“递归类型的元理论”展开归纳与余归纳、有限与无限类型、成员检查、正则树、μ 类型以及 iso-递归类型的子类型。
第五部分：多态（第22–28章）
第 22 章“类型重构”讲类型变量与代换、基于约束的类型判定、合一、主类型和 let 多态。第 23 章“全称类型”介绍 System F、其例子与性质、擦除、片段、参数性和非直谓性。第 24 章“存在类型”讲用存在类型做数据抽象及其编码；第 25 章实现 System F。第 26 章“有界量化”给出定义、例子和安全性证明；第 27 章用新工具重访命令式对象；第 28 章讨论其元理论，包括完整 F<: 的不可判定性。
第六部分：高阶系统（第29–32章）
第 29 章“类型算子与种类”引入种类（kind）；第 30 章“高阶多态”研究由此得到的系统，并以关于依赖类型的一节收尾；第 31 章讲高阶子类型。第 32 章“案例研究：纯函数式对象”用这些要素构造一种对象编码。
核心概念
第一、二部分
- 操作语义与对项的归纳：用规则定义求值，并对语法做归纳来证明性质。
- 安全性即进展性加保持性：证明良类型程序不会卡住的标准方法。
- Curry–Howard 对应：类型与命题、程序与证明之间的联系。
- 规范化：简单类型演算中每个良类型项都会求值到一个值。
第三、四部分
- 包容与子类型关系：在期望超类型的地方使用子类型的项。
- 算法性子类型：把声明式规则变成可判定的过程。
- 归纳与余归纳：处理递归类型所需的证明原理。
第五、六部分
- 类型重构与 let 多态：通过约束和合一推断类型。
- System F 与参数性：对类型的全称量化。
- 有界量化（F<:）：把多态与子类型结合起来。
- 种类与类型算子：对类型本身分类，是高阶系统的基础。
评析
优点
- 务实、有动机的讲法。 作者自己的介绍是：每个新概念都由编程示例引出，较偏理论的部分则由实现的需要推动。关于对象的案例研究展示了真实语言的特性如何通过形式系统得到解释。
- 理论与实现并行。 第 4、7、10、17、25 章是实现章节，作者网站还提供了书中大部分演算的可运行类型检查器（用 OCaml 编写），可供实验以及检验习题解答。
- 依赖关系明确。 介绍中说明章节之间的依赖关系有明确标示，读者可以选择不同的阅读路径。
- 习题附解答。 每章都有习题，附录 A 用约 70 页给出部分习题的解答。作者主页上 Robin Milner、Robert Harper、John Reynolds 和 Henk Barendregt 的推荐语称本书清晰、组织良好，兼顾理论与实现，习题由易到难。
局限
- 数学要求。 全书由定义、归纳证明和元理论构成，读者需要习惯这种风格，而第 2 章只是回顾预备知识。
- 范围止于 21 世纪初。 依赖类型只占一节（30.5），目录中也没有渐进类型、亚结构系统等章节。
- 节奏不均。 后面的章节，如第 21 章（递归类型的元理论，共十二节）和第 28 章（有界量化），比前面的章节技术性强得多；正是依赖结构使得跳过它们成为可行。
在课程中的定位
本课程中的多数书籍讲的是如何构建语言处理器。Nystrom 的 Crafting Interpreters 带读者为一种小型动态类型语言写出两个完整的解释器。龙书、Cooper 与 Torczon 的 Engineering a Compiler，以及 Thain 的精简本科编译器教材，讲的是从语法分析到代码生成的各个阶段。它们都不以类型论为主；Pierce 这本书则解释类型系统是什么，并证明它能保证什么。
宜在写过解释器或编译器的课程之后阅读，或与逻辑、语义学课程同步阅读。它面向的是想了解其他书所实现的语言之形式视角的读者。
如何使用本书
本书适合程序设计语言方向的研究生和高年级本科生，需要精确了解标准类型系统的研究者，以及希望不局限于某一个编译器来理解类型检查的实现者。它需要主动阅读：请做习题。
实用读法：
- 核心： 第 1–3、5、8–9、11 和 13–14 章，打好无类型和简单类型的基础。
- 其次： 第 15–16 章（子类型）以及第 22–23 章（类型重构与 System F）。
- 可选路径： 第 18–19 章（对象）、第 20–21 章（递归类型）、第 24 章（存在类型）、第 26–28 章（有界量化）和第 29–32 章（高阶系统），根据兴趣并参照章节依赖关系选择。
每引入一个系统，就运行并扩展对应的 OCaml 实现，并用附录 A 的解答检查证明。作者网站上的勘误表持续更新。