渐进类型是什么？

原文地址：What is Gradual Typing
作　　者：Jeremy Siek

渐进类型（Gradual Typing）是 Jeremy Siek 和 Walid Taha 在2006年开发的一套类型系统，它允许程序的一部分使用动态类型(Dynamically typed)而另一部分使用静态类型(Statically typed)。程序员通过移除或添加类型注释(Type Annotations)来控制各部分采用哪种类型。本文给出关于渐进类型的简单介绍。

下诸几点是我们开发渐进类型的动机：

大型软件系统通常由多种语言开发，一定程度上是因为动态类型语言擅长于一些任务，而静态类型语言则擅长于另一些任务。在一个渐进类型的系统中，程序员无需在不同语言中切换，也毋庸处理语言间交互的麻烦，即可在动态类型和静态类型之间做出选择。但愿这会提高程序员的生产力。
为数不多的语言已经支持可选的类型注释，但令人吃惊的是，只有少数关于类型检查器针对这些可选的类型注释应该做何种工作、类型系统应该提供何种类型保证的形式化研究。支持可选类型注释的语言有：Common LISP、Dylan、Cecil、Visual Basic.NET、Bigloo Scheme、Strongtalk。渐进类型旨在为这些语言的语义及它们的可选类型注释提供基础。有一些正在发开的新型语言也会支持可选类型注释，如 Python 3K，下一代 Javascript(ECMAScript 4) 和 Perl 6 。但愿我们关于渐进类型的工作会影响到这些语言。

在描述渐进类型之前，我们先来回顾一下动态类型检查和静态类型检查。

动态类型检查

很大一部分流行的语言，特别是脚本语言，都使用动态类型检查。如 Perl，Python，Javascript，Ruby 和 PHP 。广义地说，一个类型(Type)描述了由值构成的集合和这些值共有的一系列操作。比如，int 类型描述了（通常是32位的）数字构成的集合，这些数支持像加、减等操作。将操作应用在一个具有错误类型的值上则会产生类型错误(Type error)。比如，在串接(Concatenation)操作只支持字符串的系统中，将串接操作应用在整数上就会导致类型错误。类型错误的另一个例子则是调用对象尚未实现的方法，比如 car.fly() 。（都已经过了2000年了，可以飞的汽车却还没成为主流，这难道不是耻辱吗？）关于类型错误的精确定义依赖于程序设计语言。例如，有的语言可能会允许整数的串接，而另外的语言不允许。在动态类型语言中，类型检查在程序执行时进行，每次应用操作前都会立即检查操作数的类型适合于该操作符。

下面的 Python 程序，就是一个求值为类型错误的例子。

def add1(x):
	return x + 1

class A(object):
	pass

a = A()
add1(a)

在标准 Python 解释器中执行上述程序会输出下述结果：

TypeError: unsupported operand type(s) for +: 'A' and ‘int'

静态类型检查

流行语言中仍然存在大量的静态类型语言，如 Java 、 C# 、 C 和 C++ 。在使用静态类型检查的语言中，类型检查器可以在运行程序之前捕获到部分甚至所有类型错误。类型检查器通常是编译器的一部分并且在编译阶段自动运行。

下面的 Java 程序由上述 Python 程序改编：

class A {
	int add1(int x) {
		return x + 1;
	}
	public static void main(String args[]) {
		A a = new A();
		add1(a);
	}
}

当编译这个类时，Java 编译器输出下面的信息：

A.java:9: add1(int) in A cannot be applied to (A) add1(a);
          ^
1 error

你或许会吃惊于类型检查器如何能够预测出一个特定程序运行时会产生类型错误。答案是它不能。构建一个可以预测程序是否会产生类型错误的类型检查器是不可能的（这个问题等价于著名的停机问题）。取而代之的是，所有的类型检查器对程序在执行时可能产生的结果做保守估计，并针对可能导致产生类型错误的东西输出错误信息。比如，即使下面的代码最终不一定产生类型错误，但 Java 编译器还是拒绝这个程序：

class A {
    int add1(int x) {
        return x + 1;
    }
    public static void main(String args[]) {
        A a = new A();
        if (false)
            add1(a);
        else
            System.out.println("Hello World!");
    }
}

Java 语言的类型检查器不会尝试去指出在一条 if 语句的哪条分支会在运行时被选中。相反，它保守地假设两条分支都会被选中，因此会检查所有分支。

动态类型检查与静态类型检查的比较

动态类型检查和静态类型检查的拥护者之间有一场宗教战争。我认为这场战争旷日持久的原因之一就是两个阵营都有很好的观点（虽然之中也有不太好的观点）。不幸的是，两个阵营互不认可对方所认为的“好观点”。下面是我关于这些观点的评估，这可能会同时惹恼动态类型检查和静态类型检查的支持者们。当然，我们也必须给出支持或反对这些观点的理由，下面这些评估显示了我在考虑这些理由后的看法。

静态类型检查可以尽早地发现 BUG，也就极大地消除了开发周期后期甚至软件投入运行后修复 BUG 的代价。 好的观点！。动态类型的支持者反驳说可以通过一个全面彻底的测试套件检测出程序中更多的 BUG 。尽管如此，我还是认为静态类型检查提供了一种捕获类型错误方便且低耗的方法。
动态类型检查不会挡你的道：你可以立即运行你的程序，而不需要首先修改程序使类型检查器接受。好的观点！。静态类型的支持者反驳说：①我们无需大量修改程序；②通过修改程序以通过类型检查器，程序结构会变得更清晰。部分程序员觉得①成立，是因为他所使用的语言改变了他的思维方式，这些语言在无形之中引导你编写会被类型检查器接受的程序。同时，你已经习惯了类型系统带来的轻微的麻烦以至于你忘记了那是麻烦，甚至变得以能在类型系统中变通为荣。至于②，实际上并不缺乏类型系统阻碍代码以更清晰、更能复用的形式表达的例子。著名的表达式问题就是一个例子。设计并实现一个有足够表达力、能够上所有程序像我们所期望地那样直白地写出来的类型系统是恨困难的，这是类型系统继续蓬勃发展的原因之一。
静态类型检查使得程序更快地运行，这是因为类型检查不是在运行时才进行的，并且值可以用一种更加高效地方式表示。好的观点！
动态类型检查可以方便地处理依赖于运行时信息的值的类型。好的观点！
静态类型增强了模块性(Modularity)。 好的观点！例如，在一个动态语言中，不正确地调用库程序，只会在该调用深处得到一个类型错误。静态类型检查在你调用子程序处就捕获到类型错误。
静态类型检查让你更严肃地审视你的程序，这会帮助减少BUG。不好的观点。类型检查器智慧检查程序的一些简单属性。无论是用静态还是动态类型检查的语言编写的程序，确保程序正确性的大部分工作，最后都会落到开发全面的测试上。
在动态类型检查中，不必花时间写类型注释。不好的观点。编写类型注释所耗费的时间是非常之少的，当然也有一些被称作类型推测(Type Inferences)的程序可以不用类型注释就能完成类型检查。

无论是静态类型检查还是动态类型检查，都并不能压倒性地比另一方更好，因此使程序员不用切换至另一种语言并且能够自行选择（类型系统），这是说得通的。这样就为我们引入了渐进类型。

渐进类型检查器

渐进类型检查器是这样的一种类型检查器，它在编译时检查由类型注释标注的部分程序中的类型错误，但不检查没有标注的。例如，我们为 Python 所建立的渐进类型检查器的原型就不会捕获上面程序中的错误，该程序代码如下所示：

def add1(x):
    return x + 1

class A:
    pass

a = A()
add1(a)

然而，如果程序员像下面这样为形式参数 x 添加一个类型声明的话，类型检查器会抛出一个错误，因为变量 a 的类型是 A ，这跟 add1 函数的形式参数 x 的类型 int 是不一致的(Inconsistent)。

def add1(x : int)
    return x + 1

class A:
    pass

a = A()
add1(a)

（在我们的规则中，将一个静态类型赋值给像 a 这样的局部变量有点复杂，这是因为 Python 没有局部变量声明。但是在大多数情况下，我们让变量具有和赋值号右边的表达式相同的类型。）

对于没有标注的变量，渐进类型检查器通过给它们一个未知类型(Unknow Type)来处理(字面上也叫做动态类型(Dynamic Type))，我们可以将其缩写为 "?"，并允许从任何类型隐式地(Implict)转换为 ? 并且能从 ? 转换为任何类型。为了简单起见，假设 + 操作符接受整形参数。下面这个版本中的 add1 会被渐进类型检查器所接受，因为我们允许隐式地从 ? （x 的类型）转换为 int（ + 操作符所期望的类型）。

def add1(x):
	return x + 1;

允许从 ? 到 int 的隐式转换是不安全的，这也使得渐进类型有了动态类型的味道。正式因为有了动态类型，参数 x 所绑定的值会在运行时、执行加法操作之前被检查，以确保它是一个整数。

正如我们上面所提到的那样，渐进类型也允许由任何类型到 ? 类型的隐式转换。例如，渐进类型检查器接收下面的 add1 调用，因为它允许从 int（3的类型）隐式地转换为 ?（形式参数 x 所隐含的类型）。

add1(3)

渐进类型检查器也允许在一些更加复杂的类型中隐式地转换。例如，在下面的程序中，我们在不同的元组类型中转换，从 ? * int 到 int * int。

def g(p : int * int):
	return p[0]

def f(x, y : int):
	p = (x, y)
	g(p)

通常来说，渐进类型检查器允许在一致的(Consistent)类型间相互隐式转换。我们用记法S ~ T来表示类型 S 与类型 T 一致。可以通过下面的规则来判定两个类型是否一致：

对任意的类型 T，我们都有 ? ~ T 和 T ~ ? 成立。
对基本的类型 B，比如 int，我们有 B ~ B 成立。
当 T1 ~ S1 和 T2 ~ S2 成立时，元组类型 T1 * T2 与 S1 * S2 一致。这个规则可以自然地泛化为针对任意大小的元组。
当 T1 ~ S1...Tn ~ Sn 且 R ~ U 成立时，函数类型 fun(T1,...,Tn,R) （其中 T1,...,Tn 是形式参数的类型而 R 是返回值的类型）与函数类型 fun(S1,...,Sn,U) 一致。

我们把 S 与 T 不一致记为 S !~ T。

因此，我们有：

int ~ int
int !~ bool
? ~ int
bool ~ ?
int * int ~ ?
fun(?,?) ~ fun(int,int)
? ~ fun(int,int)
int * int !~ ? * bool

为什么只使用子类型不顶用？

渐进类型允许隐式地从任何类型向上强制转换(Up-cast)为 ? ，这有点像面向对象类型系统中 Object 是子类型塔的顶端。然而，渐进类型区别于其是因为它也允许向下强制转换(Down-cast)。这是渐进类型与众不同之处，也使得它有了动态类型的味道。在先前对于混合动、静态类型的尝试中，比如 Thatte 在准静态类型中就尝试使用子类型，但必须得处理下述问题。如果动态类型被同时当作子类型塔的顶和底（也就是允许同时隐式地向上强制转换和向下强制转换），那么子类型塔就会崩塌为一点，因为子类型是传递的(Transitive)。换句话说，每个类型都是其它类型的子类型，而类型系统也不再拒接任何程序，即使该程序中有明显的类型错误。

考虑下面的程序：

def add1(x : int) -> int:
	return x + 1

add1(true)

使用 true 作为函数 add1 的参数显然是一个类型错误，但我们由 bool <: ? 和 ? <: int 可以得到 bool <: int。因此，基于子类型的类型系统会接受这个程序。Thatte 通过在类型检查之后增加一个被称作 plausbility checking 的处理来部分地解决这个问题。但是 Oliart 指出即使如此，这样的类型系统也不能检查出完全标注的代码中所有的类型错误。我不会深入介绍 Thatte 的 plausibility checking ，因为它相当复杂，但我会举一个例子。plausibility checking 不会检查出下面程序中一个明显的静态类型错误。

def inc(x : number):
	return x + 1

inc(True)

在将 inc 应用到 True 时，inc 和 True 都可以隐式地向上强制转换为动态类型 ? 。这样，inc 就隐式地向下强制转换为 ? -> ?。plausibility检查器查找 number -> number 与 ? -> ? 最低层绑定，也就是 ? -> number，这样就使得程序没有收到警告就通过了。