类型理论在程序设计语言的发展中起着举足轻重的作用，成熟的类型系统可以帮助完善程序设计本身，帮助运行系统检查程序中的语义错误。 要理解类型系统在程序设计语言中发挥的作用，本书将是首选读物。本书内容覆盖基本操作语义及其相关证明技巧、无类型lambda演算、简单类型系统、全称多态和存在多态、类型重构、子类型化、囿界量词、递归类型、类型算子等内容。本书既注重内容的广度，也注重内容的深度，实用性强。在引入语言的语法对象时先举例，然后给出形式定义及基本证明，在对理论的进一步研究后给出了类型检查算法，并对每种算法都给出了OCaml程序的具体实现。本书对类型理论中的概念都有详细的阐述，为读者提供了一个进一步理论学习的基础。本书内容广泛，读者可以根据自己的需要有选择地深入阅读。 本书适合从事程序设计的研究人员和开发人员，以及程序设计语言和类型理论的研究人员阅读。可作为计算机专业高年级学生、研究生的学习教材。 第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.3 类型检查 74 10.2 项和类型 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.9 含self类 158 18.8 调用超类方法 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.7 let多态 223 22.6 隐含的类型注释 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.1 引言 245 第24章 存在类型 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.1 简单对象 322 第32章 实例学习：纯函数对象 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 本书适合从事程序设计的研究人员和开发人员，以及程序设计语言和类型理论的研究人员阅读。可作为计算机专业高年级学生、研究生的学习教材。 第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.3 类型检查 74 10.2 项和类型 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.9 含self类 158 18.8 调用超类方法 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.7 let多态 223 22.6 隐含的类型注释 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.1 引言 245 第24章 存在类型 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.1 简单对象 322 第32章 实例学习：纯函数对象 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