类型系统的根本目的是防止程序运行过程中出现执行错误，这个非正式的声明激发了对类型系统的研究。它的准确性首先取决于一个相当微妙的问题 —— 什么是执行错误。然而即使解决了这个问题，没有执行错误也是一个相当不简单的性质。我们必须证明所有可以在编程语言中表达的程序都没有执行错误，才能说该语言是类型安全的。（注：原文是 type soundness，译为类型健全；我们使用了更通俗的术语 type safety，即 “类型安全”。）事实证明，在进行相当多的仔细分析后，才可能避免对编程语言的类型健全性提出错误或令人尴尬的声明。而类型系统的分类、描述和研究也已经成为一门正式的学科。

类型系统的形式化需要精确的符号和定义，以及对形式化性质的详细证明（以使人们相信定义确实是妥当的）。有时，这门学科变得相当抽象；但是我们应该始终记住，实用性仍是这些抽象的基本动机：

抽象是出于需要，并且通常可以与具体的直觉相联系；
形式化，作为一门技术，即便不完整地使用也可以达成相当有用的效果。

了解类型系统的主要原则可以帮助语言设计者避免（明显和不明显的）陷阱，看到语言特性彼此之间的独立性或联系，以此使语言设计得更加规范。

如果发展得当，类型系统还可以作为一门工具，以判断语言定义中的（重要部分）是否已经足够明晰 —— 非正式的语言描述（如自然语言，译者注）往往不能足够清晰和详细地说明语言的类型结构，以保证其实现起来没有歧义 —— 同一语言的不同编译器实现了略有不同的类型系统，这是经常发生的情况。此外，许多语言的定义被发现是类型不安全的，即使程序被类型检查器判定为可以接受，也会导致程序崩溃。理想情况下，形式化类型系统应该是所有带类型的编程语言的定义的一部分。这样一来，就可以根据精确的规范来衡量类型检查算法。而且，如果可能与可行的话，整个语言都可以被证明是类型安全的。

接下来，我们会非形式化地介绍类型、执行错误和其相关概念。我们讨论类型系统的预期性质和好处，并回顾类型系统如何被形式化。我们使用的术语并不是完全标准的；这是由于来自不同来源的标准术语的内在不一致性造成的。在提到运行时概念时，我们用动态检查来代替动态类型，并避免使用强类型这样常见但含糊的术语。

#?类型的基本概念?#

#?类型

在程序的执行过程中，一个程序变量可以承担一定的数值（数据）范围。这种范围的上限被称为该变量的类型。例如，一个布尔类型的变量?x?应该在程序的每次运行中只承担布尔值。如果?x?是布尔类型，那么布尔表达式?not(x)?在程序的每次运行中都有合理的意义；如果?x?承载了布尔以外的值，例如字符串，那么布尔表达式?not(x)?并无合理的意义。

#?类型化语言和非类型化语言

变量可以被赋予非平凡的（即非单一通用类型）类型的语言被称为类型化语言（原文为 typed languages 和 untyped languages，直译为 “类型化的语言” 和“非类型化的语言”，译者注）。

不限制变量范围的语言被称为非类型化语言：它们没有类型，或者说，有一个包含所有值的单一通用类型。在这些语言中，操作可以应用于不适当的参数：其结果可能是一个固定的错误值或一个异常等。

类型系统是类型化语言的组成部分，它记录变量的类型；一般来说，它也记录程序中所有表达式的类型。类型系统被用来确定程序是否表现良好。只有符合类型系统的程序才应该被认为是类型化语言的真正程序；不符合类型系统的程序应该被丢弃而从不运行。

#?显式类型与隐式类型

一种语言由于其类型系统的存在而被类型化，无论类型是否实际出现在程序的语法中。如果类型是语法的一部分，该语言就是显式类型的，否则就是隐式类型的。

没有哪种主流语言是纯粹的隐式类型，但是像 ML 和 Haskell 这样的语言支持编写省略类型信息的大型程序片段；这些语言的类型系统会自动为这些程序片段分配类型。

#?执行错误、安全、行为良好?#

典型的执行错误有非法指令错误或非法内存引用错误。然而，还有一些更微妙的执行错误，它们会导致数据损坏却不会被立刻感知。此外，有一些通常不会被类型系统预防的软件故障，例如除以 0 和对 NIL 解引用；也有些语言虽然缺乏类型系统，但软件故障却不会发生。因此，我们需要仔细定义我们的术语。

#?执行错误和安全

区分两类执行错误是很有用的：

第一类是（在许多计算机架构上）会导致计算立即停止的 trapped?[2]?错误，例如除以零和访问非法地址。（译者注：这里不太好翻译，因此保留了原单词。）
第二类是在发生时没有被注意到而在之后导致程序任意行为的 untrapped 错误，例如在没有运行时边界检查的情况下，访问超过数组末端的（错误）数据。

如果一个程序片段不会导致 untrapped 错误的发生，那么它就是安全的。所有程序片段都是安全的语言被称为安全语言。因此，安全语言排除了那些可能被忽视的最隐蔽的执行错误。非类型化语言可以通过执行运行时检查来实现安全。类型化语言可以通过静态检查来拒绝所有可能不安全的程序来实现安全（但静态检查通常不会特别精确，因此也会拒绝一些安全的程序）。类型化语言也可以使用运行时和静态检查的混合方式。

尽管安全性是程序的一个重要性质，但类型化语言很少只关注和排除 untrapped 错误，即类型化语言通常也致力于排除 trapped 错误。我们接下来讨论这些问题。

#?执行错误和行为良好

对于任何给定的语言，我们可以挑选执行错误的一个子集作为禁止的错误。（译者注：编译器必须能检查出的错误。）禁止的错误应该包括所有 untrapped 错误以及 trapped 错误的一个子集。

如果一个程序片段运行时不会发生任何禁止的错误，那么它就是行为良好的。通过简单推论可知，一个行为良好的程序片段总是安全的。

#?强（类型）检查

一个所有合法程序都有良好行为的语言被称为强（类型）检查的。

因此，对于一个给定的类型系统，以下情况在强检查语言中成立：

没有 untrapped 错误。
被禁止的 trapped 错误不会发生。
其他 trapped 错误可能会发生；避免这些错误是程序员的责任。

类型化语言可以通过执行静态（即编译时）检查来强制保证行为良好（和安全）。这些语言是静态检查的，检查过程被称为类型检查，而执行这种检查的算法被称为类型检查器。一个通过类型检查器的程序被称为类型良好的；否则，它就是类型错误的 —— 但这可能意味着它就是行为不良的，也可能仅仅意味着类型检查器不能保证它是行为良好的。静态检查语言的例子有 ML、Java 和 Pascal（注意，Pascal 有一些不安全的特性）。

非类型化语言可以通过足够详细的运行时检查来排除所有禁止的错误，来强制保证行为良好（和安全）。例如，它们可以检查所有的数组边界和所有的除法操作，当禁止的错误发生时，产生可恢复的异常。这些语言的检查过程被称为动态检查；LISP 就是这种语言的一个例子。注意，这些语言仍然是强检查的，尽管它们既没有静态检查，也没有类型系统。

即使是静态检查的语言通常也需要在运行时进行测试以达到安全的目的。例如，一般来说，数组的边界必须在动态中进行测试。因此一种语言被静态检查的事实并不一定意味着可以完全盲目地执行。

一些语言利用其静态类型结构来进行复杂的动态测试。例如，Simula67 的 INSPECT，Modula-3 的 TYPECASE，以及 Java 的 instanceof 结构，都是对对象的运行时类型进行区分。这些语言仍然被认为是静态检查的（稍有不妥），部分原因是动态类型测试是在静态类型系统的基础上定义的。也就是说，对类型相等的动态测试与类型检查器在编译时用来确定类型相等的算法是兼容的。

也许安全性是一个更原始的、比行为良好更重要的性质，然而大多数类型系统的设计是为了确保更一般的行为良好性质，以及隐含的安全性。因此，类型系统的目标通常是通过区分类型良好和类型错误的程序来确保所有程序行为良好。

#?弱（类型）检查

在现实中，某些静态检查的语言并不能确保安全。也就是说，他们所禁止的错误集并不包括所有 untrapped 错误。这些语言可以被委婉地称为弱（类型）检查（或弱类型，在文献中），意味着一些不安全的操作不会被检测出来。这类语言在弱点的表现上差异很大。例如，Pascal 语言只有在使用未标记的变体类型和函数参数时才是不安全的；而 C 语言有许多不安全的、广泛使用的特性，如指针运算和强制类型转换（casting）。有趣的是，C 语言程序员的十条命令中的前五条?[3]?都是为了弥补 C 语言的弱检查方面的问题。C 语言的弱检查所造成的一些问题在 C++ 中得到了缓解，而更多的问题在 Java 中得到了解决，（这或许）证实了脱离弱检查是一种趋势。Modula-3 支持不安全的特性，但只在明确标记为不安全的模块中，并防止安全模块导入不安全的接口。

大多数非类型化语言都是完全安全的（例如 LISP）。原因也很简单，如果不是这样的话，编程就会变得非常困难和令人沮丧 —— 程序随时可能崩溃，并且难以发现直接原因。例如汇编语言就是一种 “令人不快的” 无类型的不安全语言。（译者注：相信没有人会享受用它去编写大规模的应用程序。）

#?对语言和类型系统的若干讨论?#

#?语言应该是安全的吗？

实现安全所需的运行时检查有时被认为太昂贵（例如即使在有大量静态分析的语言中，数组越界等检查通常也不能在编译时完全消除），因此出于性能考虑，有些语言被故意做成不安全的，例如 C 语言。尽管如此，仍有许多人在努力设计安全的 C 语言子集，并制作开发工具，试图通过引入各种（相对昂贵的）运行时检查来安全地执行 C 程序。这些努力来自两个主要的原因：

C 语言也被广泛使用在那些对性能要求不高的应用中
不安全的 C 语言程序所带来安全问题，例如缓冲区溢出和算术下溢，可能导致覆盖任意的内存区域，并可被利用进行攻击。

根据不同的衡量标准，安全相对于性能提升或许是更加经济、有效的。

例如安全的程序在执行错误时下会立即停止，这减少了调试的时间。
安全性保证了运行时结构的完整性，因此可以进行垃圾收集，而垃圾收集大大减少了代码的大小和代码的开发时间。（但牺牲了一些性能。）
安全已经成为系统安全的必要基础，特别是对于加载和运行外来代码的系统（如操作系统内核和网络浏览器）。系统安全正在成为程序开发和维护中最昂贵的方面之一，而安全可以降低这种成本。

因此，安全语言和不安全语言之间的选择最终可能与开发和维护时间以及代码执行时间之间的权衡有关。近年来，安全语言有成为主流的趋势。

#?语言应该类型化吗？

关于编程语言是否应该类型化的问题仍然存在一些争议。毋庸置疑，用无类型的语言编写的代码很难被维护。从可维护性的角度来看，即使是弱检查的不安全语言（例如 C）也要优于安全但非类型化的语言（例如 LISP）。下面是从工程的角度提出的支持非类型化语言的论据。

##?程序执行的经济性

一般来说，编译时准确的类型信息使运行时的一些操作无需昂贵的检查。例如类型信息首先被引入到编程中，以提高代码生成和数值计算的运行效率，FORTRAN 便是一例。例如在 ML 中，准确的类型信息使得指针解引用时无需做 NIL 检查。

##?小规模开发的经济性

当一个类型系统设计精良时，类型检查可以捕获很大一部分常见的编程错误，从而减少大量的调试时间。因为大量的其他错误已经被排除，这也使我们更容易观测和调试真正发生的错误。此外，有经验的程序员还可以采用特定的编码风格来使一些（隐式的）逻辑错误成为（显式的）类型错误：他们把类型检查器作为一种开发工具。

##?编译的经济性

类型信息可以被组织成程序模块的接口。然后，模块可以相互独立地进行编译，每个模块只依赖于其他模块的接口。这使得编译大型系统更加高效，因为在接口稳定的情况下，对一个模块的修改不会导致其他模块的重新编译。例如 Modula-2 和 Ada 便是这样。

##?大规模开发的经济性

接口和模块对代码开发有方法上的优势。大型的程序员团队可以协商要实现的接口，然后分别去实现相应的代码片段。代码片断之间的依赖性被最小化，代码可以被局部地重新安排，而不用担心全局的影响。(这些好处也可以通过非正式的接口规范来实现，但在实践中，类型检查对验证对规范的遵守有很大帮助）。

##?安全领域的开发和维护的经济性

正如安全对于消除缓冲区溢出等安全漏洞是必要的，类型化对于消除其他灾难性的安全漏洞也是必要的。这里有一个典型的例子：如果有任何方法（不管多么复杂）可以将一个整数转换成一个指针类型（或对象类型）的值，那么整个系统就会面临风险 —— 攻击者可以在系统中的任何地方访问任何数据。另一个有用的（但不是必须的）技术是将一个给定的类型的指针转换成一个整数，然后再转换成上述不同类型的指针。从维护和整体执行效率的角度来看，消除这些安全问题的最经济有效的方法是采用类型化语言。不过，安全问题在系统的各个层面都是一个问题，因此类型化语言是一个很好的基础但仍不是一个完整的解决方案。

##?语言特性的经济性

类型结构天然以正交的方式组成。例如，在 Pascal 中，二维数组其实是数组的数组；在 ML 中，有 n 个参数的函数其实是一个具有单个 n - 元组参数的函数。因此，类型系统可以促进语言特性间的正交性，让人们思考和质疑（语言中）人为做出的一些限制，从而倾向于降低编程语言的复杂性。

#?类型系统的预期性质

在本章的其余部分，我们假设语言应该既安全又类型化，因此应该采用类型系统。在对类型系统的研究中，我们并不区分 trapped 或 untrapped 错误，也不区分安全和行为良好：我们专注于行为良好，并将安全作为一个隐含的性质。

在编程语言中，类型通常具有实用性特征，这些特征将其与其他种类的程序标注区分开来。一般来说，关于程序行为的标注可以是非正式的注释，也可以是需要经过验证的正式的规格描述。类型位于这个范围中间：它们比注释更精确，比规格描述更容易机械化（自动化）。以下是任何类型系统都被期望具有的基本性质：

类型系统应该是可验证的：应该有一种算法（类型检查算法）可以确保程序的行为良好。类型系统的目的不是简单地说明程序员的意图，而是在执行错误发生之前主动捕捉它们。(任意的形式化规范不具备这些性质。）
类型系统应该是透明的：程序员应该能够轻松地预测一段代码是否可以通过类型检查。如果它不能通过类型检查，那么失败的原因也应当是不言而喻的。(自动定理证明不具备这些特性。）
类型系统应该是强制的：应该尽可能地静态检查关于类型的声明，并动态检查无法静态检查的部分。程序与其类型之间的一致性应该被例行验证。(程序注释不具有这些性质。)

#?类型系统是如何被形式化的?#

我们怎样才能保证类型良好的程序是真正行为良好的呢？或者说，我们怎样才能确保语言的类型规则不会意外地放过行为不良的程序呢？

一般的程序语言手册都会或多或少地描述它们的类型系统，而形式化的类型系统?是正是那些非正式类型系统的数学特征。一旦一个类型系统被形式化，我们就可以尝试证明一个正确性定理（soundness theorem，似乎一般称为健全性定理），说明类型良好的程序一定也是行为良好的。如果这样的正确性定理成立，我们就说该类型系统是正确的。(即 “类型化语言中的所有程序都行为良好”。）

为了使一个类型系统正规化，并证明其正确性定理，我们必须对整个语言进行规范化，正如下文描述的那样。

第一步是描述它的语法。对于大多数语言来说，这可以简化为描述类型和项（terms，一般为语句、表达式和其他程序片段）的语法。类型表达关于程序的静态知识，而项则表达算法行为。
第二步是定义语言的作用域规则，将标识符的每次出现与它们的声明位置（无歧义地）地绑定起来。类型化语言所需的作用域绑定总是静态的，也就是说，所有标识符的绑定必须在运行前唯一确定。绑定关系通常可以纯粹从语言的语法中确定，而不需要任何进一步的分析。静态作用域也被被称为词法作用域（lexical scoping），缺乏静态作用域的情形被称为动态作用域（dynamic scoping）。正式的作用域绑定规则可以通过定义程序片段的自由变量集来给出，之后就可以定义如何去替换类型或项中的自由变量（substitution）。
当这些都解决后，我们可以继续定义语言的类型规则 “has-type”。这些规则描述了项 M 和类型 A 之间的形式为 M:A 的关系（即 M 有类型 A）。一些语言还会定义类型上的形式为 A<:B 的子类型关系以及形式为 A=B 的等价关系。语言的类型规则的集合即为它的类型系统，具有类型系统的语言被称为类型化语言。
除此之外，我们还需要引入一个不反映在语言语法中的基本要素 ——?静态类型环境?—— 否则类型规则就不能被形式化，因为类型规则总是针对被类型检查的片段的静态环境而制定。在程序片段的处理过程中，这个静态环境被用来记录自由变量的类型。在类型检查阶段，它与编译器的符号表紧密相关。例如，前文中的类型关系 M:A 与静态类型环境? $\Gamma$ ?相关联，该环境包含了 M 和 A 中的自由变量的信息。（译者注：例如有?bool?类型的全局变量?x，那么在检查全局函数?int main() { x + 1;}?的函数体时，类型环境?? $\Gamma$ ?将包含类型关系 x:bool，其中?x?是函数体中的自由变量。）
形式化语言的最后一步是将其语义定义为项和项的计算结果之间的 “has-value” 关系。这种关系的形式在很大程度上取决于所采用的语义风格（译者注：例如小步语义，大步语义）。在任何情况下，语言的语义和类型系统都是相互关联的：项的类型和其计算结果的类型应该是相同的（或有其他适当形式的关联）—— 这就是正确性定理的本质。

类型系统的基本概念几乎适用于所有编程范式（函数式、命令式、并发式等等）；对于不同的范式，一些类型规则往往可以不加改变地使用。例如，无论编程范式是命令式还是函数式，无论语义是按名调用（call-by-name）还是按值调用（call-by-value），函数的基本类型规则都是一样的。

关于类型等价：如上所述，大多数非平凡的类型系统需要定义一个类型上的等价关系。这是定义编程语言时的一个重要问题：什么时候独立给出的类型表达式是等价的？例如，

type?X?=?Bool
type?Y?=?Bool

如果上述类型名 X 和 Y 由于相等，我们就有了结构等价。如果它们不相等，我们就有按名等价。

在实践中，大多数语言都既使用了结构等价又使用了按名等价。单纯的结构等价可以通过类型规则轻松而精确地定义，而按名等价则更难确定，而且往往有一种算法的味道。当类型化的数据需要在网络上存储或传输时，结构等价具有独特的优势；相比之下，按名等价不容易处理那些在时间或空间上分别开发和编译的交互程序。

在本章中，我们讨论了独立于语义的类型系统。不过，我们应该知道，最终一个类型系统必须与语义相关，而且正确性理论应该对该语义成立。

#?用以描述类型系统的语言?#

类型系统指定了编程语言的类型规则，但它又独立于特定的类型检查算法；正如形式化的语法可以描述编程语言的语法，但它又独立于特定的语义解析算法。

将类型系统与类型检查算法脱钩既方便又有用：类型系统属于语言定义，而特定算法则属于编译器。用类型系统来解释语言的类型方面 —— 相比于用某个编译器所使用的算法来解释 —— 总是较为容易的。此外，不同的编译器可能对同一个类型系统使用不同的类型检查算法。（作为一个小问题，从技术上讲，可以定出只存在实际不可行的类型检查算法或者根本就不存在类型检查算法的类型系统；然而，通常的意图是允许有效的类型检查算法。）

#?断言

对一个类型系统的描述始于对断言（judgements）的形式化描述。一个典型的断言形式如下（其中? $\vdash$ ?意为蕴含（英文为 entails）：

$\Gamma \vdash \mathfrak{J} \qquad$

$\mathfrak{J}$ ?是断言，其中自由出现的类型变元在? $\Gamma$ ?中声明

这里? $\Gamma$ ?是一个静态类型环境；例如，它可以是一个由（不同）变量及其类型组成的有序列表? $\phi, x_1 : A_1, \dots, x_n : A_n$ 。空环境用? $\phi$ ?表示， $\Gamma$ ?中声明的变量? $x_1 \dots x_n$ ?的集合用? $\mathit{dom}(\Gamma)$ ?表示，它即为? $\Gamma$ ?的定义域。 $\mathfrak{J}$ ?的形式因断言而异，其中的所有自由变量都必须在? $\Gamma$ ?中声明。

就我们目前的目的而言，最重要的断言是关于类型关系的断言，它表明一个项 M 在静态类型环境下具有类型 A：

$\Gamma \vdash M : A \qquad$

M 在? $\Gamma$ ?下有类型 A

示例：

$\phi \vdash \mathit{true} : \mathit{Bool} \qquad$ ? ? ? ??true 在空环境下有类型 Bool

$x : \mathit{Nat} \vdash x + 1 : \mathit{Nat}$ ? ? ?x+1?在环境 x:Nat 下有类型 Nat

其他的断言形式往往也是必要的。一个常见的断言形式是指明一个环境是构造良好的（well-formed）：

$\Gamma \vdash \diamond$

任何给定的判断都可以被看作是有效的（如? $\Gamma \vdash \mathit{true} : \mathit{Bool}$ ）或无效的（如? $\Gamma \vdash \mathit{true} : \mathit{Nat}$ ）。有效性形式化地描述了类型良好这一的概念。有效断言和无效断言之间的区别可以用多种方式表达，但这种描述合法断言的方式已经成为主流。此外，类型规则是高度模块化的：不同语言要素的规则可以单独编写（这与单一、巨大、复杂的类型检查算法相反）。因此，类型规则相对来说更容易阅读和理解。

#?类型规则

类型规则在其他已知的有效的断言的基础上说明某一断言的有效性。这个过程通常由一些本质上一定有效的判断（通常是? $\phi \vdash \diamond$ ?，它表示空环境是构造良好的）开始。类型规则的一般形式：

$\frac{\Gamma_1 \vdash \mathfrak{J}_1 \quad ... \quad \Gamma_n \vdash \mathfrak{J}_n}{\Gamma \vdash \mathfrak{J}} (rule-name)$

每条类型规则都写成横线之上的若干前提判断? $\Gamma_i \vdash \mathfrak{J}_i$ ，横线之下是单一的结论判断? $\Gamma \vdash \mathfrak{J}$ 。当所有的前提得到满足时（前提的数量可以是零），结论必须成立。每条规则都有一个名称。(按照惯例，名称的第一个字由结论中的断言决定；例如，"(Val ...)" 形式的规则名称是指其结论为关于值（译者注：即项的计算结果）的类型断言的规则。) 当需要时，限制规则适用性的条件，以及规则中使用的缩写，都会在规则名称或前提旁边加以注释。

例如，下面两条规则中的第一条指出，在任何结构良好的环境? $\Gamma$ ?中，任何数字都是一个 Nat 类型的表达式。第二条规则指出，表示自然数的两个表达式 M 和 N 可以组合成一个更大的表达式 M+N，它也表示自然数。此外，M 和 N 的环境? $\Gamma$ ?声明了 M 和 N 中的所有自由变量的类型，并且也对 M+N 有效。

$\begin{aligned} &(\text{Val}\,n) \; (n = 0, 1, ...)\\ &\frac{\Gamma \vdash \diamond}{\Gamma \vdash n : \mathit{Nat}} \quad \end{aligned}$

$\begin{aligned} &(\text{Val}\,+)\\ &\frac{\Gamma \vdash M : \mathit{Nat} \quad \Gamma \vdash N : \mathit{Nat}}{\Gamma \vdash M+N : \mathit{Nat}} \quad \end{aligned}$

类型规则的集合被称为（形式化的）类型系统。从技术上讲，类型系统符合形式化证明系统的一般框架：用于进行逐步演绎的规则的集合。在类型系统中进行的演绎关注程序的类型化。

#类型的推导

在一个给定的类型系统中，一个推导过程（derivation）是一棵断言树，上面是叶子，下面是根，其中每个断言都是通过系统的一些规则由紧挨着它的断言得到的。对类型系统的一个基本要求是，必须能够检查一个推导是否被正确地构造。

在一个给定的类型系统中，一个有效的断言是通过正确地使用类型规则得到的，因此它一定是作为某个推导的根得到的断言。例如，使用前面给出的三条规则，我们可以建立下面的推导，从而确定? $1+2 : \mathit{Nat}$ ?是一个有效的判断。每一步应用的规则都显示在每个结论的右边。

#?类型良好和类型推断

在一个给定的类型系统中，如果在环境? $\Gamma$ ?下，存在一个类型 A，使得? $\Gamma \vdash M : A$ ?是一个有效的断言，那么项 M 就是类型良好的。

探索一个项的推导过程（也就是类型）被称为类型推断问题（type inference problem）。在上述简单类型系统中，可以在空环境下为项 1+2 推断出一个类型。通过前面的推导，这个类型是 Nat。

假设我们现在添加一个类型规则，其前提为? $\Gamma \vdash \diamond$ ，结论为? $\Gamma \vdash \mathit{true} : \mathit{Bool}$ 。在该类型系统中，因为不存在自然数与布尔数相加的规则，所以我们无法推断出项 1+true?的任何类型。由于?1+true?没有任何推导过程，我们说?1+true?是不可类型化的，或者说它是类型错误的，或者说类型化过程有错。

我们可以进一步增加一个类型规则，其前提是? $\Gamma \vdash M : \mathit{Nat}$ ?和? $\Gamma \vdash N : \mathit{Bool}$ ，结论是? $\Gamma \vdash M+N : \mathit{Nat}$ （例如，意图是将 true 解释为 1）。在这样一个类型系统中，可以为术语?1+true?推断出一个类型，它是类型良好的。

因此，一个给定项的类型推断问题对有关的类型系统非常敏感。根据类型系统的不同，类型推断的算法可能非常容易，也可能非常困难，甚至不可能找到。如果找到了，最好的算法可能是非常有效的，也可能是慢得无可救药的。尽管类型系统被表达出来，并且经常被抽象地设计出来，但它们的实际效用取决于是否有好的类型推断算法。

像 Pascal 这样的显式类型的程序性语言的类型推断问题是相当容易解决的，隐式类型语言如 ML 的类型推断问题要微妙得多：而在多态（polymorphism）存在的情况下，类型推断问题变得特别困难。Ada 和 Standard ML 的显式类型多态结构的类型推断问题在实践中是可以处理的；然而，这些问题基本上是由算法解决的，而没有描述它们的类型系统。适用于多态的最纯粹和一般的类型系统是由 λ- 演算给出的（之后介绍）。

#?类型正确

现在我们已经建立了所有关于类型系统的一般概念，可以开始研究特定的类型系统了。之后我们会回顾一些非常强大但又比较理论化的类型系统：我们首先了解这些特定的类型系统，这样就可以更容易地为编程语言中可能遇到的各种复杂的特性编写类型规则。

当我们沉浸在类型规则中时，我们应该记住，一个合理的类型系统不仅仅是一个任意的规则集合。类型良好是为了对应于行为良好这一语义概念。人们习惯于通过证明类型正确性定理来检查类型系统的内部一致性，这就是类型系统与语义交汇的地方。对于指称语义（denotational semantics），我们期望如果? $\phi \vdash M : A$ ?是有效的，那么? $[[M]] \in [[A]]$ ?就成立（M 的值属于类型 A 所表示的值的集合）。对于操作语义，我们期望如果? $\phi \vdash M : A$ ?以及 M 归约（*译者注：reduce，可以简单理解为计算）为?M'，那么? $\phi \vdash M' : A$ ?也成立。在这两种情况下，类型正确性定理都断言了类型良好的程序在计算时不会出现执行错误（这里忽略证明）。

在下一篇文章中，我们会介绍一些主流编程语言中常见的类型系统和其中的类型规则。

参考

[1] Type systems. Luca Cardelli. Allen B. Tucker (Ed.): Computer Science Handbook, 2nd ed. Chapman & Hall/CRC Press, 2004. Chapter 97. http://lucacardelli.name/Papers/TypeSystems.pdf

[2] Trap - Wikipedia https://en.wikipedia.org/wiki/Trap_(computing)

[3] Spencer, H., The ten commandments for C programmers (annotated edition). Available on the World Wide Web.