类型系统综述2

原书作者：Luca Cardelli，Microsoft Research
本文整理：Koshiba

译者注释使用下划线标注，方便识别。

注

本文全面覆盖了《Type Systems by Luca Cardelli》一书中第三章（一阶类型系统）的主要内容。由于第三章内容较多，并且其中涉及大量数学公式如公式等复杂表达式, 我们将剩余的引用、递归类型以及数组与列表等内容留至下次讨论。
全文未使用\mathit{}标记, 将其交由渲染器自行处理, 希望能够得到良好的呈现效果。

一阶类型系统和有类型 \lambda- 演算

这些常见过程式编程语言中的类型系统都被视为一阶体系。从专门术语的角度来看，在这类语言中可以包含高阶函数；然而，在这类系统的二阶特性方面却存在缺失——这与二阶类型的定义相悖。Pascal 和 Algol 68 的一阶类型系统高度发达；相比之下，Fortran 和 Algol 60 的设计相对落后。

为此目的，我们可以为无类型的 λ 演算构建一个最小的一阶类型系统。其中无类型的 λ 抽象 λx.M 表示接受参数 x 并返回 M 的函数。该系统只需配备函数型别和若干基础型别即可；在后续部分中，我们将探讨如何拓展加入更多常见型别。

该 λ 漼算理论在引入了显式的类型标记后被视为一种高级形式。相较于无类型的 λ 演算而言，在这种体