1. 程序设计语言中的类型¶

1.1. 引入示例¶

考虑以下三种不同程序设计语言中的代码片段。

JavaScript 代码片段

var g = function (x, y) {
        return (x ? 1 : y + 13);
};
var add = function (x, y) {
    return x + y;
};
var divide = function (x, y) {
    return x / y;
};
console.log (g( (2 < 1), 6));
console.log (g( (2 < 1), "Hello"));
console.log (g( (2 < 1), [3,2,1]));
console.log (g( (2 < 1), [3,[2,1]]));
console.log (add(6,4));
console.log (add(6,"Green Bay Packers"));
console.log (add("Aaron", "Rodgers"));
console.log (divide(6,4));
console.log (divide(6,"Green Bay Packers"));
console.log (divide("Aaron", "Rodgers"));

当把这段程序交给 JavaScript 时，它会有什么行为？这又告诉我们 JavaScript 是如何处理不同类型的数据的？

Python 3 代码片段

def mult(x, y):
    return x * y

print( mult(4,3) )
print( mult("hello", "goodbye") )

当把这段程序交给 Python 时，它会有什么行为？这又告诉我们 Python 是如何处理不同类型的数据的？

Java 代码片段

// foo program
public class foo {
    static int g (boolean x, int y) {
        return (x ? 1 : y);
    }
    public static void main(String[] args) {
        System.out.println(g( (2 < 1), 6));
    }
}

// foobar program
public class foobar {
    static int g (boolean x, int y) {
        return (x ? 1 : y);
    }
    public static void main(String[] args) {
        System.out.println(g( (2 < 1), "Hello"));
    }
}

// foobaz program
public class foobaz {
    static g (x, y) {
        return (x ? 1 : y);
    }
    public static void main(String[] args) {
        System.out.println(g( (2 < 1), 6));
    }
}

当把这几段程序交给 Java 时，它会有什么行为？这又告诉我们 Java 是如何处理不同类型的数据的？

更准确地说，关于前面这三段 Java 程序，下列说法中哪些是正确的？

foo 能够成功编译。
foo 能够成功运行。
foobar 能够成功编译。
foobar 能够成功运行。
foobaz 能够成功编译。
foobaz 能够成功运行。
foobaz 应当能够成功编译。
foobaz 应当能够成功运行。

1.2. 类型系统：定义¶

每种程序设计语言都有一个 type system ，粗略地说，它是一组规则，这些规则为变量、字面值、复合表达式、函数参数、函数调用等赋予一种类型，并根据这些类型约束上述构造的使用方式，例如，一个函数的返回值能否有意义地赋给某个变量。

在程序中，类型是根据一个表达式所计算或可能代表的值，而赋予该表达式的一种范畴。而 类型系统 则是每种程序设计语言用来帮助程序员避免某些称为 类型错误 的错误所使用的类型集合与定型规则；所谓类型错误，是指对一个（或多个）值施加了在该值上并无意义的操作的情形。

现代程序设计语言通常在什么意义上拥有一个 可扩展的 类型系统？提示： Java 中有哪些可用的类型？

Benjamin Pierce 在他 2002 年出版的名为 Types and Programming Languages 的书中给出了关于类型系统更为精确的定义，值得一读：

类型系统 是一种可处理的（tractable）语法方法，用于证明某些程序行为
不会出现 [...]

那么 Pierce 所说的以下各点分别是什么意思：

方法（method）

类型系统是一种用于推理程序设计语言的工具。
语法（syntactic）

类型系统根据语法来对表达式进行分类，也就是根据程序设计语言构造（变量、运算符、关键字等）的结构或排布来分类。因此，语法是类型系统计算程序中的表达式与语句在运行时的近似行为的基础，这一近似基于这些构造可能计算出的值。
证明（proving）

类型系统的目标是保证它所认定的类型错误永远不会发生；一个良类型（well-typed）的程序不应出现异常行为。
某些程序行为 （certain program behaviors）

坏行为是指 卡住状态 （stuck state）：此时某个表达式没有值，而且没有任何规则允许该值的计算继续进行（即运行时错误）。
可处理 （tractable）

类型检查器内置于编译器、链接器和运行时系统中，必须在没有程序员交互的情况下自动完成工作；因此，我们需要不仅在理论上可处理、而且在实际中高效的类型检查算法。

1.3. 类型系统：静态与动态¶

类型系统的目的始终是防止出现不想要的程序状态，例如上面提到的卡住状态。

在静态类型系统中，类型是在程序执行之前确定并检查的。这通常由编译器完成。在静态类型检查期间标记出的类型错误，通常会阻止程序被执行。
在动态类型系统中，类型是在程序执行期间确定并检查的。类型通过为每个值附加一个标明其类型的标签来跟踪。某段代码中的类型错误只有在该代码实际执行时才会被标记出来。

静态类型与动态类型实际上是两种截然不同的类型系统方法。它们不仅在不同的时间进行处理，而且实现方式也大不相同。

有哪些静态类型程序设计语言的例子？

有哪些动态类型程序设计语言的例子？

静态类型与动态类型差别如此之大，以至于专家们不愿意对两者使用同一个词。他们通常只把定型（typing）这一术语保留给静态类型系统使用。

例如，Pierce 认为 类型检查 这一说法只适用于静态类型语言。对于所谓的 动态程序设计语言 而言，谈论 动态类型 是一种用词不当；更精确的描述应当是 动态检查 （dynamically checked）。

1.4. 类型系统：安全与不安全¶

所谓类型安全的语言保证良类型的程序具有良好行为。换句话说，如果一个类型系统拒绝所有不正确的程序，那么它就是安全（safe）的（或可靠（sound）的）。更具体地说，如果一种程序设计语言（或者，在更细粒度的分析中，某个程序设计语言构造）禁止对其所操作的类型而言不正确的操作，那么它就是 类型安全 的。

由于类型系统是静态的，它必须是保守的：它只能证明某些坏的程序行为不会出现，而不能证明它们会出现。这是因为一个安全且 可判定 的类型系统总是 不完备 的，也就是说，它必定有时会拒绝那些在运行时表现良好的程序（为什么会这样呢？）。例如，下面的代码片段：

\[\begin{eqnarray*} \mbox{if <complex test> then 5 else <type error>} \end{eqnarray*}\]

即使该测试始终求值为真，也可能被作为类型不良而拒绝。

此外，只有某些不想要的程序行为能够被防止。考虑：

检查除法运算的两个参数都是整数
检查第二个参数不等于 0

这些检查中哪一（几）个可以静态地完成？

1.5. 类型系统：强类型与弱类型¶

在谈论程序设计语言时，你应当避免使用 强类型 （strongly typed）和 弱类型 （weakly typed）这两个说法，因为对于这些术语并不存在普遍公认的定义。

例如，程序设计语言 C 究竟是弱类型还是强类型？

一般来说，这些术语指的是语言所提供的整体类型安全水平。有些程序设计语言或构造可能会阻止不正确的操作，或者使这些操作变得困难，但并不会完全禁止它们。因此，编译器施加的类型限制越多，用来绕过类型系统的漏洞越少，这种程序设计语言就越接近强类型。

注意！许多软件开发人员把静态/动态这一特征，与完全不同的强类型/弱类型这一特征混为一谈。再次强调，请不要使用后者。

1.6. 类型系统：类型化的变量还是值¶

在静态类型系统中，类型通常同时施加于变量和值。

在动态类型系统中，类型由附加在值上的标签来表示。因此，一般来说，在动态类型系统中只有值才有类型。

例如，在下面这个 JavaScript 函数中（它已经作为引入示例的一部分出现在上面）：

var g = function (x, y) {
        return (x ? 1 : y + 13);
};

console.log (g( (2 < 1), 6));
console.log (g( (2 < 1), "Hello"));

函数参数 y 并没有被类型检查器赋予唯一的类型。相反，在函数调用中作为实参传入的值确实有类型：6 是一个整数，而 "Hello" 是一个字符串。正是这个类型标签使得 JavaScript 运行时系统在第一次调用中使用整数加法，而在第二次调用中使用字符串连接。

此外，在动态检查的语言中，容器（如列表）通常没有类型；只有它们的值才有类型。因此，一个列表持有不同类型的值通常没有问题。例如：

var a = [ 1, "2", 3.4, true, [] ];

这是良好行为，并且被 JavaScript 的类型系统所允许。

1.7. 类型系统：显式类型与隐式类型¶

当我们通过在源代码中明确写出某个实体的类型来指定它时，我们是在进行 显式类型 （explicit typing）。C、C++ 和 Java 中变量与函数的类型大多是显式的。对类型的显式指定称为 类型标注 （type annotation）。

当类型没有被显式指定时（例如 Python、JavaScript），我们得到的是 隐式类型 （implicit typing）。

在动态检查的语言中，定型通常大多是隐式的。因此，人们很容易把显式类型与静态类型混为一谈。然而，这两者并不相同。

Haskell 或 ML 编译器会在静态类型检查的过程中执行 类型推断 ，从而根据实体在源代码中的使用方式来确定/推断类型。ML 的类型据说是被推断出来的。虽然在 ML 中通常不需要类型标注，但仍然允许（有时也需要）使用它们。

再举一个例子，自 2011 年起，C++ 标准就允许在该语言中越来越多地使用类型推断。

反过来，一些动态检查且隐式类型的程序设计语言（例如 Python、JavaScript）正朝着可选类型标注的方向发展。

1.8. 类型系统的诸多用途¶

类型系统被用于许多目的，包括：

确定合法的值和操作，从而支持类型安全
强制实施 语言安全 （这与类型安全有何不同？）
确定在多个可能的操作中执行哪一个：

例如，+ 运算符的重载
支持抽象和高层模块化
保护用户自定义抽象的完整性
为程序编写文档
简化程序维护
提高效率
等等

OpenDSA 完整目录

Chapter 32 Type Systems