类型系统
作者：Luca Cardelli
英文原文 PDF：Type Systems。
前言
类型系统的根本目的在于防止程序动态运行时发生执行错误。这个不够形式化的陈述推动了类型系统的研究，因此接下来对类型系统进行详细地说明。类型系统的准确性首先取决于一个相当微妙的问题，即什么是执行错误。即便弄清楚了它的定义，我们仍然必须知道判断程序不会发生执行错误不是一件容易的事情。当我们能够证明任何这种程序语言表达的合法程序都不会发生执行错误，我们就说这种程序语言是类型 sound（健全）。事实证明，需要大量的仔细分析，才能避免错误地声称一个程序语言是类型 sound 的。因此，类型系统的分类、描述和研究已经成为了一门正式的学科。
类型系统的形式化需要制定精确的符号和定义，对于形式化属性的详细证明。有时，这门学科会变得十分抽象。但是，我们必须明确，我们最初的动机是实际的，任何抽象的描述总是会和具体的直觉相关联。类型系统的核心原则是帮助避免明显或不明显的陷阱，以推动程序语言设计的发展。
如果类型系统能够充分发展，那么它将提供概念性的工具，用以判断程序语言的关键部分是否充分地定义。非形式化的语言描述往往无法规范地描述类型结构，因此经常发生不同编译器对于同一种程序语言实现了不同的类型系统。此外，许多语言的定义本身就是类型 unsound 的，即使程序已经通过了类型检查，它仍然会在运行时发生错误。在理想情况下，形式化的类型系统应该是所有包含类型的编程语言定义中的一部分。这样一来，就可以根据准确的规范来明确地对程序进行类型检查，如果可能的话，整个语言就可以说是类型 sound 的。
在这个介绍章节，我们提出了一个关于类型、执行错误和相关概念的非形式定义。我们讨论了类型系统的预期的属性和带来的好处，并且回顾了如何将类型系统形式化。在介绍章节中使用的术语并不是完全标准的，这是由于不同来源的标准术语内在并不一致。在第二章节，我们解释了描述类型系统的常用符号。我们还解释了判断，即关于程序类型的形式化断言，类型规则，即判断之间的影响和使用类型规则进行推导。在第三章节，我们回顾了简单类型在程序语言中的深远影响，并且类比了通用语言中的类型规则。在第四章节，我们介绍了一个虽然简单但是完整的命令式编程语言，和它的类型规则。在第五章节，我们讨论了更高级的类型构造的规则，例如堕胎和数据抽象。在第六章节，我们解释了类型系统如何使用子类型来进行扩展。第七章节是关于一些被人们忽略的重要话题。在第八章节，我们讨论了类型推导的问题，并且对于我们之前讨论的语言给出了一个类型推导算法。最后，第九章节是对目前成果的总结和对未来方向的展望。
执行错误
执行错误最明显的症状是程序预期之外故障发生，例如执行了非法的指令，引用了非法的内存地址。
还有一些更微妙的执行错误，导致数据损坏，却没有任何直接的症状。此外，还有一些软件故障，例如除 0 或者空指针，这些故障是类型系统无法防止的。最后，有些语言没有类型系统，但是软件故障却不会发生。因此，我们需要详细定义我们的术语，那么我们从什么是类型开始说起。
类型和无类型程序语言
在程序执行过程中，一个程序变量可以存储一定范围的值。变量的值的范围被称为变量的类型。例如，一个类型为 Bool 的变量 $x$ 在程序每次运行中只能存放 Bool 值。如果在程序每次运行中 $x$ 的类型是 Bool，那么布尔表达式 $not(x)$ 就是有意义的。可以给变量赋予（非平凡）类型的语言被称为类型语言。
不限制变量范围的语言被称为无类型语言，它们没有类型或者只拥有一个泛用的类型来表示所有变量的值。在这种程序语言中，操作可能会被应用不匹配的参数上，得到一个随机的结果，一个运行时异常或者未定义的副作用。纯粹的 $\lambda$ 演算就是一种无类型语言，但是不会有错误发生，因为唯一的操作只有函数应用，并且所有值都是函数，函数应用只是在其作用域中进行替换，因此不会发生错误。
类型系统是类型语言的组成部分，它追踪了变量的类型以及所有程序表达式的类型。类型系统用来判断一个程序的行为是否是行为良好的（well behaved）。只有通过类型系统检查的源程序才能被认为是类型语言的真正程序，其它源程序应该在运行前就被丢弃。
一个语言是凭借类型系统才被称为类型语言，无论类型是否显示出现在程序的语法定义之中。如果类型是语法的一部分，那么类型语言就是显式类型语言，相反就是隐式类型语言。目前，没有任何主流的编程语言是完全隐式的，但是 ML 和 Haskell 等语言支持编写省略类型信息的大型程序，这类语言的类型系统会自动为这些程序推导类型。
执行错误和安全性
我们需要区分两种执行错误：一种是导致程序立刻停止的错误；另一种是，可能没有被发现，但是随后导致任意错误行为的。前者被称为陷阱错误（trapped errors），后者被称为未捕获错误（untrapped errors）。
一个未捕获错误的例子是不合法地访问内存地址。例如，在没有运行时边界检查的情况下，访问超过数组容量的下标；或者是跳转到了错误的地址，这片内存空间可能表示一段其它位置的程序代码或者单纯是程序数据。陷阱错误的例子除 $0$ 或者访问非法内存，在很多计算机架构中，这种错误会立刻终止计算。
如果一个程序片段不会发生未捕获的错误，那么我们称它是安全的。如果这种语言表达的所有程序片段都是安全的，我们称这种语言是安全的语言。因此，安全语言派出了隐含的执行错误。对于无类型语言，可以在运行时动态检查来加强安全性。类型语言可以通过静态分析拒绝执行可能不安全的程序片段。当然，类型语言可以混合静态分析和运行时动态检查。
虽然安全是程序的一个重要属性，但是类型语言很少只关注排除未捕获错误。类型语言的目标是排除尽可能多种类的陷阱错误和未捕获错误。
执行错误和行为良好的程序
对于任何给定的程序语言，我们将可能触发执行错误的一个子集称为禁止错误（forbidden errors）。禁止错误应该包含所有的未捕获错误和陷阱错误的子集。如果一段程序代码不会触发任何禁止错误，那么我们称它为行为良好的程序（well behaved）。一段行为良好的程序是安全的。如果一个程序语言的所有合法程序代码都是行为良好的，那么我们称这个程序语言是强检查的（strongly checked）。
因此，对于一个程序语言的类型系统，以下是强检查的条件：
- 不会发生未捕获错误；
- 没有被指定为禁止错误的陷阱错误发生；
- 其它陷阱错误可能发生，程序员应该尽力避免它们。
类型语言可以通过执行静态检查的方式来强制阻止不安全的程序运行，这类语言被称为是静态检查的语言，检查的过程就被称为类型检查（typechecking），执行类型检查算法的程序就被称为类型检查器。如果一段程序代码通过了类型检查，那么这段代码就是良类型的（well typed），反之就是不良类型（ill typed），即程序是错误的或者没有办法保证其一定行为良好。常见的静态类型语言有 ML，Java 和 Pascal 等（注意 Pascal 有一些不安全的特性）。
无类型的程序语言可以用不同的方式强制使得其运行时是行为良好的，例如使用运行时的详细检查，来排除所有禁止错误。例如，这些语言可能会检查数组越界，除法操作等，当错误发生时产生可以恢复的异常。这些语言的检查阶段被称为动态检查，例如 Lisp。这些语言尽管没有静态检查，甚至也没有类型系统，但它们是强检查的。
即使是静态类型检查的语言，通常也需要在运行时执行某些动态检查，例如数组越界的检查就必须在动态运行时进行。一个程序语言是静态检查的，并不意味着可以随意第执行而不会发生错误。
有几种语言利用它们的静态类型结构来进行复杂的动态测试，以达到安全的目的。例如 Simula67 的 INSPECT，Modula-3 的 TYPECASE，Java 的 instanceof 结构都能对对象运行时类型进行判别。这些仍然被认为是静态检查的，因为它们的动态类型测试时定义在静态类型系统的基础上的。也就是说，类型的相等性动态测试与类型检查器和编译时类型检查的相等性是兼容的。
安全性的缺失
通过我们的定义，一个行为良好的程序是安全的。安全性是一个比行为良好更加本质也更加重要的属性。类型系统的本质是通过指出程序当中的禁止错误来保证程序语言的安全性。但是，大部分类型系统的设计都是为了确保更加普遍的良好行为属性和隐含的安全。因此，类型系统的声明目标通常是保证程序的行为良好，通过指出一个程序是良类型的或是不良类型的。
实际上，某些静态类型检查语言并不能确保安全性。也就是说，它们的禁止错误并没有包括所有未捕获错误，这些语言被委婉地称为弱类型检查语言。这意味着，对于这些语言的程序代码，一些不安全的操作被静态检查到了，而另外一些不安全的操作没有被检查到。这一类程序语言在它们薄弱的地方各有不同。例如，Pascal 语言是不安全，当且仅当使用了未标记的变量类型或者函数形式参数；C 语言是不安全的，指针运算和指针类型转换。有趣的是，在 C 程序员的十条戒律中，前五条都是针对 C 语言的弱类型检查方面的补充，在 C 语言中的弱类型检查在 C++ 中得到了部分的缓解，甚至在 Java 中得到了解决，这印证了远离弱类型检查的发展趋势。Modula-3 中支持不安全的特性，当且仅当这个模块被标记为不安全的，并防止安全模块导入不安全的接口。
大部分的无类型语言在必要时是安全的（例如 Lisp）。否则，使用缺失编译时和运行检查的语言进行编程将会是一件十分痛苦的事情，而汇编语言恰好就属于这一类令人不快的无类型不安全程序语言。
| 类型 | 无类型 | |
|---|---|---|
| 安全 | ML Java | Lisp |
| 不安全 | C | 汇编语言 |