1.1.2　类型和类型系统的定义

本书讨论的是类型和类型系统，下面就先来定义这两个术语。

类型：类型是对数据做的一种分类，定义了能够对数据执行的操作、数据的意义，以及允许数据接受的值的集合。编译器和运行时会检查类型，以确保数据的完整性，实施访问限制，以及按照开发人员的意图来解释数据。

有时候，我们会简化讨论，忽略操作部分，而只将类型简单地视为集合，代表该类型的实例能够接受的所有可能的值。

类型系统：类型系统是一组规则，为编程语言的元素分配和实施类型。这些元素可以是变量、函数和其他高级结构。类型系统通过两种方式分配类型：程序员在代码中指定类型，或者类型系统根据上下文，隐式推断出某个元素的类型。类型系统允许在类型之间进行某些转换，而阻止其他类型的转换。

定义了类型和类型系统之后，我们接下来看看类型系统的规则是如何实施的。图1.3从更高层面展示了源代码的执行过程。

图1.3　编译器或解释器将源代码转换成可被运行时执行的代码。运行时是一个真实的计算机或者一个虚拟机，例如，Java的JVM或浏览器的JavaScript引擎

在高层面上，编译器或解释器将把我们编写的源代码转换成机器（或运行时）能够理解的指令。当运行时是一台物理计算机时，转换的指令将是CPU指令；当运行时是虚拟机时，则有自己的指令集和工具。

类型检查：类型检查确保程序遵守类型系统的规则。编译器在转换代码时进行类型检查，而运行时在执行代码时进行类型检查。编译器中负责实施类型规则的组件叫作类型检查器。

如果类型检查失败，则意味着程序没有遵守类型系统的规则，此时程序将会编译失败，或者发生运行时错误。1.3节将详细说明编译时类型检查与执行时（或运行时）类型检查的区别。

类型检查和证明

类型系统得到大量形式理论的支持。例如，柯里–霍华德（Curry-Howard）对应，也叫作“证明即程序”，就展示了逻辑与类型理论之间的密切关系。该对应说明，我们可以将类型视为一个逻辑命题，将从一个类型得到另一个类型的函数视为逻辑蕴含。类型的一个值相当于证明命题为真的一个证据。

下面我们以一个接受boolean作为参数并返回一个string的函数为例加以说明。

Boolean到string

这个函数也可以解释为“boolean蕴含string”。给定命题boolean的证据，这个函数（蕴含）能够得到命题string的证据。boolean的证据是该类型的一个值：true或false。有了这个证据后，该函数（蕴含）将得到string的证据：要么是字符串"true"，要么是字符串"false"。

逻辑与类型理论之间的密切关系说明，遵守类型系统规则的程序相当于一个逻辑证明。换句话说，类型系统是一种语言，我们用它来写出这些证明。柯里–霍华德对应很重要，因为它为“程序将正确运行”这种保证带来了逻辑上的严谨性。