第1章 引论 1
1.1 计算机科学中的类型 1
1.2 类型系统的优点 3
1.3 类型系统和语言设计 6
1.4 历史概要 6
1.5 相关阅读 7
第2章 数学基础 9
2.1 集合、关系和函数 9
2.2 有序集合 10
2.3 序列 11
2.4 归纳 11
2.5 背景知识阅读 12
第一部分 无类型系统 13
第3章 无类型算术表达式 14
3.1 导论 14
3.2 语法 15
3.3 对项的归纳 17
3.4 语义形式 20
3.5 求值 21
3.6 注释 27
第4章 算术表达式的一个ML实现 28
4.1 语法 28
4.2 求值 29
4.3 其余部分 31
第5章 无类型lambda演算 32
5.1 基础 32
5.2 lambda演算中的程序设计 36
5.3 形式性 43
5.4 注释 46
第6章 项的无名称表示 48
6.1 项和上下文 48
6.2 移位和代换 50
6.3 求值 51
第7章 lambda演算的一个ML实现 53
7.1 项和上下文 53
7.2 移位和代换 54
7.3 求值 55
7.4 注释 56
第二部分 简单类型 57
第8章 类型算术表达式 58
8.1 类型 58
8.2 类型关系 59
8.3 安全性＝进展＋保持 61
第9章 简单类型的lambda演算 64
9.1 函数类型 64
9.2 类型关系 65
9.3 类型的性质 67
9.4 Curry-Howard对应 70
9.5 抹除和类型性 71
9.6 Curry形式和Church形式 72
9.7 注释 72
第10章 简单类型的ML实现 73
10.1 上下文 73
10.2 项和类型 74
10.3 类型检查 74
第11章 简单扩展 76
11.1 基本类型 76
11.2 单位类型 77
11.3 导出形式：序列和通配符 77
11.4 归属 79
11.5 let绑定 80
11.6 序对 81
11.7 元组 83
11.8 记录 84
11.9 和 86
11.10 变式 88
11.11 一般递归 93
11.12 列表 95
第12章 规范化 97
12.1 简单类型的规范化 97
12.2 注释 99
第13章 引用 100
13.1 引言 100
13.2 类型化 104
13.3 求值 104
13.4 存储类型 106
13.5 安全性 108
13.6 注释 111
第14章 异常 112
14.1 提升异常 112
14.2 处理异常 113
14.3 带值的异常 114
第三部分 子类型化 119
第15章 子类型 120
15.1 包含 120
15.2 子类型关系 121
15.3 子类型化和类型化的性质 125
15.4 Top类型和Bottom类型 128
15.5 子类型化及其他特征 129
15.6 子类型化的强制语义 134
15.7 交叉类型和联合类型 138
15.8 注释 139
第16章 子类型的元理论 140
16.1 算法子类型化 141
16.2 算法类型化 143
16.3 合类型和交类型 146
16.4 算法类型化和Bottom类型 148
第17章 子类型化的ML语言实现 149
17.1 语法 149
17.2 子类型化 149
17.3 类型化 150
第18章 实例分析：命令式对象 152
18.1 什么是面向对象编程 152
18.2 对象 153
18.3 对象生成器 154
18.4 子类型化 155
18.5 聚集实例变量 155
18.6 简单类 155
18.7 添加实例变量 157
18.8 调用超类方法 158
18.9 含self类 158
18.10 使用self的开放递归 159
18.11 开放递归及求值顺序 160
18.12 更高效的实现 163
18.13 小结 165
18.14 注释 165
第19章 实例分析：轻量级的Java 167
19.1 引言 167
19.2 概要 168
19.3 规范化和结构化的类型系统 170
19.4 定义 172
19.5 性质 176
19.6 编码及初始对象 177
19.7 注释 178
第四部分 递归类型 179
第20章 递归类型简介 180
20.1 实例 181
20.2 形式 186
20.3 子类型化 188
20.4 注释 188
第21章 递归类型元理论 189
21.1 归纳和共归纳 189
21.2 有限类型和无穷类型 191
21.3 子类型 192
21.4 传递性的偏离 194
21.5 成员检查 195
21.6 更高效算法 198
21.7 正则树 201
21.8 μ类型 202
21.9 计算子表达式 205
21.10 关于指数级算法的闲话 209
21.11 子类型化同构递归类型 210
21.12 注释 211
第五部分 多态 213
第22章 类型重构 214
22.1 类型变量和代换 214
22.2 类型变量的两个观点 215
22.3 基于约束的类型化 216
22.4 合 220
22.5 主类型 222
22.6 隐含的类型注释 223
22.7 let多态 223
22.8 注释 227
第23章 全称类型 229
23.1 动机 229
23.2 各种多态 229
23.3 系统F 230
23.4 实例 231
23.5 基本性质 238
23.6 抹除，可类型化，类型重构 239
23.7 抹除和求值顺序 241
23.8 系统F片断 242
23.9 参数性 243
23.10 不可预言性 244
23.11 注释 244
第24章 存在类型 245
24.1 引言 245
24.2 带存在量词的数据抽象 248
24.3 存在量词编码 255
24.4 注释 256
第25章 系统F的ML实现 257
25.1 类型的无名表示 257
25.2 类型移位和代换 257
25.3 项 258
25.4 求值 260
25.5 类型化 260
第26章 囿量词 263
26.1 引言 263
26.2 定义 264
26.3 实例 268
26.4 安全 271
26.5 囿存在量词类型 275
26.6 注释 277
第27章 实例分析：命令性对象，约式 279
第28章 囿量词的元理论 283
28.1 揭示 283
28.2 最小化类型 284
28.3 核心F<：系统的子类型化 286
28.4 全F<：系统中的子类型化 288
28.5 全F<：系统的不可判定性 290
28.6 合类型和交类型 293
28.7 囿存在量词 295
28.8 囿量词和最小类型 296
第六部分 高阶系统 297
第29章 类型算子和分类 298
29.1 直觉 298
29.2 定义 302
第30章 高阶多态 304
30.1 定义 304
30.2 实例 305
30.3 性质 306
30.4 Fω系统片断 312
30.5 进一步讨论：依赖类型 313
第31章 高阶子类型化 317
31.1 直觉 317
31.2 定义 318
31.3 性质 320
31.4 注释 321
第32章 实例学习：纯函数对象 322
32.1 简单对象 322
32.2 子类型化 323
32.3 囿量词 323
32.4 接口类型 325
32.5 向对象发送消息 326
32.6 简单的类 326
32.7 多态更新 327
32.8 添加实例变量 329
32.9 含self的类 330
32.10 注释 332
附录A 部分习题解答 333
附录B 标记约定 389
参考文献 391