本书提出了一种基于类型系统和结构操作语义的编程语言理论。第2版经过全面修订，几乎每章都包含习题，并新增一章讨论类型细化。本书涉及的概念广泛，包括：基本数据类型，多态和抽象类型，动态定型，动态分派，子类型和类型细化，符号和动态分类，并行和成本语义，并发和分布。书中对不同编程语言的特性做了分析、证明和比较，所提供的方法可直接应用于语言的实现、程序推理逻辑的研发以及语言特性的形式化验证，具有较高的实用性。本书不仅可以作为高等学校计算机相关专业的编程语言理论课程教材，也可供相关领域的科研人员和技术人员参考阅读。

CMU教授力作，全新视角阐释语言构造，未来编程语言设计者必读经典

就像构建软件系统的第2版会有风险一样，为教材编写第2版也会带来风险：很难在避免过度修改和不破坏原有基础的情况下做出实质性改进。为了避免“第二系统效应”，我试图通过更正、修订、扩展和删除来提高内容的一致性，删除一些偏离主题的话题，增加一些第1版中遗漏的话题，并为每一章引入习题。
此次修订删除了许多印刷错误，纠正了一些重大错误（特别是并行抽象机和Algol并发性的公式），并改进了全书的表述。一些章节被删除（一般模式匹配和极化、多态的受限形式），一些章节被完全重写（关于高阶种类的章节），一些章节被大幅修改（一般的和参数化归纳定义、并发和分布式 Algol），一些章节被重组（以更好地区分部分类型论和完全类型论），另外还新增了一章（关于类型细化）。本次修订删除了一些章节中对资料来源的不清晰引用，以避免混淆这些话题当前和原有的表述。全书引入了一套新的(可发音的）语言名称系统。习题试图扩展正文中的思想，而其解答往往涉及值得研究的重要技术思想。在课后作业中，尽量不包含按部就班的常规练习。
撰写本书的目的是建立一个全面阐述和分析编程语言中各种思想的框架。语言设计和编程方法要从手工制作发展到严密的学科，首先必须要有正确的定义。只有这样，才能进行有意义的分析和整合。我希望能帮助建立这样的基础。
感谢Stephen Brookes、Evan Cavallo、Karl Crary、Jon Sterling、James R. Wilcox和Todd Wilson对本版书稿的评审，并感谢他们提出的修订建议。感谢我的系主任Frank Pfenning对我完成本版工作的支持。还要感谢编辑Ada Brunstein和Lauren Cowles的指导和协助,感谢Andrew Shulaev对书稿的修正。
无论是作者还是出版商都无法保证本书中的定义、定理和证明没有错误，或者符合任何特定的适销性标准，或者满足任何特定应用的要求。使用本书的人员不应依赖它们来解决可能因不正确的解决方案而招致人身伤害或财产损失的问题。如果你执意按这种方式使用本书，后果自负。作者和出版商不承担因此造成的任何直接或间接损失。

Robert Harper
匹兹堡
2015年7月

计算机\程序设计

本书是关于计算基础理论的综合读本。作者谈到了语言设计中出现的一系列令人惊讶的概念：从简单类型到多态性，从依赖类型到模块，从严格到懒惰到并行计算，从关于可扩展性行为的推理的证明技术到存在垃圾回收情况下的实用组合成本模型。更重要的是，整本书使用类型和类型理论的原理来组织章节，帮助我们发现正交的、可组合的抽象，这些抽象不仅自然地出现在编程语言的设计中，而且自然地出现在逻辑和数学中。这种方法有助于揭示隐藏在当今编程语言内部的基本结构，并为未来的设计提供了一种原则性的方法。
—— Greg Morrisett，康奈尔大学计算与信息科学学院院长
本书从数学上一个简单的框架和组织原则开始，将类型系统作为中心，揭示了编程语言这门兼具广度和优雅性的科学学科所蕴含的理论。作者丰富的经验和精辟的观点使得本书必将成为经典。
—— Andrew Pitts，剑桥大学理论计算机科学教授
本书对编程语言概念的讲解非常到位，全书架构统一，解释细致，使用的技术在分析和实现编程语言的实践中非常有用。本书作者是编程语言类型理论领域杰出的研究人员，本书正是作者多年教学经验的结晶。
—— Lars Birkedal，哥本哈根信息技术大学计算机科学教授
作者简介
罗伯特·哈珀（Robert Harper） 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。
译者简介
张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。
胡明哲　中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。

[美]罗伯特·哈珀(Robert Harper) 著：---作者简介---
罗伯特·哈珀(Robert Harper) 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。

---译者简介---
张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。

胡明哲 中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。

类型是编程语言理论的核心组织原则。在这本创新的书中，作者Robert Harper教授通过使用类型理论对各种编程语言特征的本质提供了全新的诠释。大多数关于该主题的教科书都强调分类学，而Robert Harper 则强调遗传学。他仔细研究构建所有编程语言的语言构造，在书中首先描述包含简单语言特征的基础语言，再在已建立的语言上通过引入新的语言特征得到更多的扩展语言。语言特征通过类型结构来表现，语言的语法由定义其类型的语言构造来控制，而其语义由这些构造之间的交互来决定。随后讨论语言设计的可靠性（soundness），即不存在不良定义的程序。Robert Harper教授以初等数学为基础，简洁、严谨地给出各种语言特征的定义，他概述的“语法-静态语义-动态语义-安全性（safety）”框架可轻松扩展到丰富多样的语言概念，并直接适用于它们的实现。总体上，本书是对涵盖现代编程语言中各种语言特征的编程理论的清晰介绍，相当具有实用性。
本书反映了Robert Harper教授对编程语言领域的深刻理解。Robert Harper是美国卡内基·梅隆大学的计算机科学教授，从事编程语言研究。他对Standard ML 编程语言和 LF 逻辑框架的设计做出了重大贡献，并于 2005 年因其对编程语言类型系统的贡献而当选为 ACM Fellow。
本书的信息非常密集，不仅涉及编程语言的基本语言特征，如函数类型、和类型以及积类型，还涉及很多不同方面的高级语言及其实现特征，如动态定型、子定型、动态分派、控制栈、异常与延续、可赋值对象及引用、并行、并发与分布式、模块化与链接，等等。本书还建立了类型系统与逻辑系统之间的联系。本书在表达思想方面非常简洁，给出的直觉和解释很少，多数情况下只是以非常正式且有时不易理解的方式呈现事实和定义。本书需要读者沉下心来仔细研究，而不是随便翻阅。本书也许更适合作为课堂的补充教科书，以及从事编程语言设计与实现的研发人员的参考书籍。
对于本书的符号体系，Robert Harper教授一直不断改进，以期用更好的表达形式来表述，但这也造成了书稿版本的不稳定以及可能存在少量有相同含义的符号前后不一致的情况。Robert Harper教授每隔一段时间会将该书的修改版本以及勘误更新到其主页http://www.cs.cmu.edu/~rwh/pfpl/。因此，我在译校本书时并不是直接翻译第2版的发行版，而是对照其主页上的最新电子版和勘误进行有选择的修改。
我在2007年开始配合导师陈意云教授在中国科学技术大学开展“程序设计语言理论”的教学，2008年冯新宇老师向我推荐了Robert Harper教授放在其主页上的该书书稿（当时还没有形成第1版）。在阅读之后，为该书对语言特征的实用、简洁、严谨的理论基础描述所吸引，于是在后续讲授“程序设计语言理论”以及面向本科生的专业方向课“程序设计语言基础”（两门课于2020年合并为研究生学科基础课暨本硕贯通课“程序语言设计与程序分析”）时，选取了其中基础的部分作为教学内容。在阅读该书时，针对书中不易理解之处或笔误等问题，我曾与Robert Harper教授通过电子邮件交流，每次总能得到他迅速的回复。一些建议被他采纳，我也因此被列入该书英文版第1版前言的致谢名单中。
本书的翻译起源于2018年春季学期在中国科学技术大学讲授本科生专业方向课“程序设计语言基础”时，选取书中第1~12、14、16、17、19、26、44章让选课的学生阅读并形成翻译初稿，参与的同学包括王若晖、梁聪、宋小牛、康子涵、周宇强、姜也东、郭振江、林鑫、韦清、王嘉男、吴金泽、李嘉豪、陈泳舟、刘伟森、安鸣霄、董仕、隆晋威。2019年到2020年上半年，胡明哲、张宇翔、郭兴、曹艳和我对全书分工进行了翻译。2020年到2021年3月，我对全书进行了多轮校译，并于2021年4月交稿。我和胡明哲对排版后的书稿进行了校对。由于译校者水平有限，难免有错讹之处，敬请广大读者批评指正。

张昱
2021年12月

译者序
第2版前言
第1版前言
第一部分　判断和规则
第1章　抽象语法 2
1.1　抽象语法树 2
1.2　抽象绑定树 4
1.3　注记 8
习题 8
第2章　归纳定义 10
2.1　判断 10
2.2　推理规则 10
2.3　推导 11
2.4　规则归纳 13
2.5　迭代归纳定义和联立归纳定义 14
2.6　用规则定义函数 15
2.7　注记 15
习题 16
第3章　假言判断与一般性判断 17
3.1　假言判断 17
3.1.1　可导性 17
3.1.2　可纳性 18
3.2　假言归纳定义 20
3.3　一般性判断 21
3.4　泛型归纳定义 22
3.5　注记 23
习题 23
第二部分　静态语义和动态语义
第4章　静态语义 28
4.1　语法 28
4.2　类型系统 29
4.3　结构性质 30
4.4　注记 31
习题 31
第5章　动态语义 33
5.1　转换系统 33
5.2　结构化动态语义 34
5.3　上下文动态语义 36
5.4　等式动态语义 37
5.5　注记 39
习题 39
第6章　类型安全 40
6.1　保持性 40
6.2　进展性 41
6.3　运行时错误 42
6.4　注记 43
习题 43
第7章　求值动态语义 44
7.1　求值动态语义 44
7.2　结构化动态语义和求值动态语义
的关系 45
7.3　重温类型安全 45
7.4　成本动态语义 46
7.5　注记 47
习题 47
第三部分　全函数
第8章　函数定义和值 50
8.1　一阶函数 50
8.2　高阶函数 51
8.3　求值动态语义和定义等同 53
8.4　动态作用域 54
8.5　注记 55
习题 55
第9章　高阶递归的系统T 56
9.1　静态语义 56
9.2　动态语义 57
9.3　可定义性 58
9.4　不可定义性 59
9.5　注记 61
习题 61
第四部分　有限数据类型
第10章　积类型 64
10.1　空积与二元积 64
10.2　有限积 65
10.3　原始互递归 66
10.4　注记 67
习题 67
第11章　和类型 69
11.1　空和与二元和 69
11.2　有限和 70
11.3　和类型的应用 71
11.3.1　void和unit 71
11.3.2　布尔类型 72
11.3.3　枚举 72
11.3.4　选择 73
11.4　注记 74
习题 74
第五部分　类型和命题
第12章　构造逻辑 78
12.1　构造语义 78
12.2　构造逻辑 79
12.2.1　可证性 79
12.2.2　证明项 81
12.3　证明的动态语义 82
12.4　命题即类型 83
12.5　注记 83
习题 83
第13章　经典逻辑 85
13.1　经典逻辑 85
13.1.1　可证性和可反驳性 86
13.1.2　证明和反驳 87
13.2　推导消去形式 89
13.3　证明的动态语义 90
13.4　排中律 91
13.5　双重否定翻译 92
13.6　注记 93
习题 94
第六部分　无限数据类型
第14章　泛型编程 96
14.1　引言 96
14.2　多项式类型算子 96
14.3　正类型算子 98
14.4　注记 99
习题 99
第15章　归纳类型与余归纳类型 101
15.1　示例 101
15.2　静态语义 104
15.2.1　类型 104
15.2.2　表达式 105
15.3　动态语义 105
15.4　求解类型等式 106
15.5　注记 107
习题 107
第七部分　变量类型
第16章　多态类型的系统F 110
16.1　多态抽象 110
16.2　多态的可定义性 113
16.2.1　积与和 113
16.2.2　自然数 114
16.3　参数化概述 115
16.4　注记 116
习题 116
第17章　抽象类型 117
17.1　存在类型 117
17.1.1　静态语义 118
17.1.2　动态语义 118
17.1.3　安全性 118
17.2　数据抽象 119
17.3　存在类型的可定义性 120
17.4　表示独立性 120
17.5　注记 122
习题 122
第18章　高阶种类 123
18.1　构造器和种类 123
18.2　构造器等同 125
18.3　表达式和类型 126
18.4　注记 126
习题 127
第八部分　部分性和递归类型
第19章　递归函数的系统PCF 130
19.1　静态语义 131
19.2　动态语义 132
19.3　可定义性 133
19.4　有限数据结构和无限数据结构 135
19.5　完全性与部分性 135
19.6　注记 136
习题 136
第20章　递归类型的系统FPC 138
20.1　求解类型等式 138
20.2　归纳类型和余归纳类型 139
20.3　自指/自引用 141
20.4　状态的起源 142
20.5　注记 143
习题 143
第九部分　动态类型
第21章　无类型的λ演算 146
21.1　λ演算 146
21.2　可定义性 147
21.3　Scott定理 149
21.4　无类型意味着单类型 150
21.5　注记 151
习题 151
第22章　动态定型 153
22.1　动态类型化PCF 153
22.2　变体和扩展 156
22.3　动态定型的批判 158
22.4　注记 158
习题 159
第23章　混合定型 160
23.1　一个混合语言 160
23.2　动态语义作为静态定型 162
23.3　动态定型的优化 162
23.4　静态定型和动态定型的对比 164
23.5　注记 165
习题 165
第十部分　子定型
第24章　结构化子定型 168
24.1　包含规则 168
24.2　各种子定型 169
24.2.1　数值类型 169
24.2.2　积类型 169
24.2.3　和类型 170
24.2.4　动态类型 170
24.3　变体 171
24.3.1　积类型与和类型 171
24.3.2　部分函数类型 171
24.3.3　递归类型 172
24.3.4　量化类型 173
24.4　动态语义和安全性 174
24.5　注记 175
习题 176
第25章　行为定型 177
25.1　静态语义 177
25.2　布尔盲 183
25.3　细化的安全性 184
25.4　注记 185
习题 186
第十一部分　动态分派
第26章　类与方法 188
26.1　分派矩阵 188
26.2　基于类的组织 190
26.3　基于方法的组织 191
26.4　自指 192
26.5　注记 194
习题 194
第27章　继承 196
27.1　类与方法扩展 196
27.2　基于类的继承 197
27.3　基于方法的继承 198
27.4　注记 198
习题 199
第十二部分　控制流
第28章　控制栈 202
28.1　机器定义 202
28.2　安全性 203
28.3　机器K的正确性 204
28.3.1　完备性 205
28.3.2　可靠性 205
28.4　注记 206
习题 207
第29章　异常 208
29.1　失败 208
29.2　异常 209
29.3　异常值 210
29.4　注记 211
习题 211
第30章　延续 213
30.1　概述 213
30.2　延续的动态语义 214
30.3　用延续构造协程 216
30.4　注记 218
习题 218
第十三部分　符号数据
第31章　符号 222
31.1　符号声明 222
31.1.1　有作用域的动态语义 223
31.1.2　无作用域的动态语义 224
31.2　符号引用 224
31.2.1　静态语义 225
31.2.2　动态语义 225
31.2.3　安全性 225
31.3　注记 226
习题 226
第32章　流动绑定 227
32.1 静态语义 227
32.2　动态语义 228
32.3　类型安全 229
32.4　一些微妙之处 229
32.5　流动引用 231
32.6　注记 231
习题 232
第33章　动态分类 233
33.1　动态类 233
33.1.1　静态语义 233
33.1.2　动态语义 234
33.1.3　安全性 234
33.2　类引用 234
33.3　动态类的可定义性 235
33.4　动态分类的应用 236
33.4.1　秘密分类 236
33.4.2　异常值 237
33.5　注记 237
习题 237
第十四部分　可变状态
第34章　现代化的Algol 240
34.1　基本命令 240
34.1.1　静态语义 241
34.1.2　动态语义 241
34.1.3　安全性 243
34.2　一些编程习语 243
34.3　类型化的命令和类型化的可赋值对象 245
34.4　注记 247
习题 247
第35章　可赋值对象的引用 250
35.1　能力 250
35.2　有作用域的可赋值对象 251
35.3　自由的可赋值对象 252
35.4　安全性 254
35.5　良性效应 256
35.6　注记 257
习题 257
第36章　惰性求值 258
36.1　按需的PCF 258
36.2　按需的PCF的安全性 260
36.3　按需的FPC 262
36.4　悬挂类型 263
36.5　注记 264
习题 264
第十五部分　并行
第37章　嵌套并行 268
37.1　二叉fork-join 268
37.2　成本动态语义 270
37.3　多叉fork-join 273
37.4　有界实现 274
37.5　调度 277
37.6　注记 279
习题 279
第38章　未来与投机 280
38.1　未来 280
38.1.1　静态语义 280
38.1.2　顺序动态语义 281
38.2　投机 281
38.2.1　静态语义 281
38.2.2　顺序动态语义 282
38.3　并行动态语义 282
38.4　未来流水线 284
38.5　注记 285
习题 285
第十六部分　并发与分布式
第39章　进程演算 288
39.1　动作与事件 288
39.2　交互 289
39.3　复制 291
39.4　分配通道 292
39.5　通信 294
39.6　通道传递 296
39.7　普适性 297
39.8　注记 299
习题 299
第40章　并发Algol 301
40.1　并发Algol 301
40.2　广播通信 303
40.3　选择性通信 305
40.4　自由的可赋值对象作为进程 307
40.5　注记 308
习题 308
第41章　分布式Algol 309
41.1　静态语义 309
41.2　动态语义 312
41.3　安全性 313
41.4　注记 314
习题 314
第十七部分　模块化
第42章　模块化与链接 316
42.1　简单单元与链接 316
42.2　初始化和效果 317
42.3　注记 318
第43章　单例种类和子种类 319
43.1　概述 319
43.2　单例 320
43.3　依赖种类 322
43.4　高阶单例 324
43.5　注记 325
习题 326
第44章　类型抽象与类型类 327
44.1　类型抽象 328
44.2　类型类 329
44.3　模块语言 331
44.4　一等模块和二等模块 334
44.5　注记 335
习题 335
第45章　层次结构和参数化 337
45.1　层次结构 337
45.2　抽象 339
45.3　层次结构和抽象 341
45.4　应用函子 343
45.5　注记 344
习题 344
第十八部分　等式推理
第46章　系统T的相等性 346
46.1　观测等价 346
46.2　逻辑等价 349
46.3　逻辑等价和观测等价重合 350
46.4　一些相等性定律 352
46.4.1　一般定律 352
46.4.2　相等性定律 353
46.4.3　归纳定律 353
46.5　注记 353
第47章　系统PCF的相等性 354
47.1　观测等价 354
47.2　逻辑等价 354
47.3　逻辑等价和观测等价重合 355
47.4　紧致性 357
47.5　惰性自然数 360
47.6　注记 361
第48章　参数化 362
48.1　概述 362
48.2　观测等价 362
48.3　逻辑等价 364
48.4　参数化性质 368
48.5　重温表示独立性 370
48.6　注记 371
第49章　进程等价 372
49.1　进程演算 372
49.2　强等价 374
49.3　弱等价 376
49.4　注记 377
附录A　有限集的背景 378
参考文献 379