类型推论

在大多数的编程语言中，所有值都有一个类型，它描述特定值的数据种类。在一些语言中，表达式的类型只在运行时才知道；这些语言被称作动态类型语言。而另一些语言中，表达式的类型在编译时就知道，这些语言叫做静态类型语言。在静态类型语言中，函数的输入和输出与局部变量的类型一般必须用类型标注明确的提供。例如，在 C 语言中:

 int addone(int x)
 {
     int result; /*声明整数 result (C 语言)*/
 
     result = x+1;
     return result;
 }

这个函数定义开始处，int addone(int x) 声明了 addone 是函数，接受一个整数类型的参数，并返回一个整数。int result; 声明了局部变量 result 是个整数。在支持类型推论的建议的语言中，代码可写为如下:

 addone(x) {
     var result;  /*推论类型 result (在建议的语言中)*/
     var result2; /*推论类型 result #2 */
 
     result = x+1;
     result2 = x+1.;  /* 此行不工作 */
     return result;
 }

这看起来非常像在动态类型语言中写出的代码，但是提供了一些额外的约束（见下）使得能够在编译时推断出所有变量的类型。在上面的例子中，因为+ 总是接受两个整数并返回一个整数。编译器可以推论出 x+1 的值是个整数，因此 result 是个整数，addone 的返回值是个整数。类似的，因为 + 要求它的两个实际参数都是整数，x 必须是整数，因此 addone 接受一个整数实际参数。

但是在随后一行中 result2 加上了一个浮点数 "1."，导致了 x 同时用于整数和浮点数的冲突。这种情况将生成编译时间错误消息。在老语言中，result2 可以被隐含的声明为浮点变量，通过隐含的转换表达式中的整数 x，简单的因为小数点意外的被放到了整数 1 的后面。这种情况说明了二者之间的区别，“类型推论”不涉及类型转换，而“隐含类型转换”经常没有限制的把数据强制成高精度的数据类型。

类型推论指的是要么部分要么完全自动演绎的能力，把值的类型从表达式的最终计算中推导出来。因为这个过程在编译时间系统性的进行，编译器经常能推出变量的类型或函数的类型标署，而不用给出明确的类型标注。在很多情况下，如果推论系统足够强壮或程序足够简单，有可能完全从程序中省略类型标注。

要获得正确推导出缺乏类型标注的一个表达式的类型所必要的信息，编译器要么随着给它的子表达式(它们自身可以是变量或函数)的类型标注的聚集(aggregate)和后续简约来收集这种信息，要么通过各种原子值的类型的隐含理解(比如 () : 单位; true : 布尔; 42 : 整数; 3.14159 : 实数; 等等)。通过表达式的最终简约到隐含类型原子值的识别，类型推论语言的编译器有能力编译完全没有类型标注的程序。在高阶编程和多态性的高度复杂的情况下，编译器不能总是如此推论，偶尔需要类型标注来去除歧义。

例如，考虑 Haskell 函数 map，它把一个函数应用于一个列表的每个元素上，它可定义为:

map f [] = []
map f (first:rest) = f first : map f rest

明显的函数 map 接受一个列表作为第二个实际参数，它的第一个实际参数 f 是可以应用于这个列表的元素的类型上函数，而 map 的结果被构造为其元素是 f 的结果的一列表。所以假定列表包含同样类型的元素，我们能可靠的构造出类型标署

map :: (a -> b) -> [a] -> [b]

这里的语法 "a->b" 指示接受 a 作为它的形式参数并生成 b 的一个过程。 "a->b->c" 等价于 "a->(b->c)"。

注意 map 的推论类型是参数化多态的: 实际参数和 f 的结果的类型是不推出的，而是留作类型变量，所以 map 可以应用于各种类型的函数和列表，只要在每次调用中实际类型是匹配的。

进行类型推论的常用算法是 Hindley–Milner 或 Damas–Milner 算法。

这个算法的起源是 Haskell B. Curry 和 Robert Feys 在1958年为简单类型lambda演算设计的类型推论算法。在 1969 年 Roger Hindley 扩展了这项工作并证明他们的算法总能推出最一般的类型。在 1978 年 Robin Milner，独立于 Hindley 的工作，提供了等价的算法。在 1985 年 Luis Damas 最终证明了 Milner 的算法是完备的并扩展它来支持带有多态引用的系统。

算法

算法过程分两个步骤。首先需要生成一些要解的方程，接着解它们。

生成方程

用来生成方程的算法类似与正规的类型检查器，所以我们首先如下有类型lambda演算的正规类型检查器:

${\displaystyle e\,::=E\mid v\mid (\lambda v:\tau .e)\mid (e\,e)}$ 

和

${\displaystyle \tau \,::=T\mid \tau \to \tau }$ 

这里的 ${\displaystyle E}$  是原始表达式 (比如 "3") 而 ${\displaystyle T}$  是原始类型 (比如 "Integer")。

我们希望构造有类型 ${\displaystyle (\epsilon ,t)\to \tau }$  的一个函数 ${\displaystyle f}$ ，这里的 ${\displaystyle \epsilon }$  是类型环境而 ${\displaystyle t}$  是一个项。我们假定这个函数已经定义在原始表达式上。其他情况有:

• ${\displaystyle f(\epsilon ,v)=\tau }$  这里的 ${\displaystyle (v,\tau )}$  在 ${\displaystyle \epsilon }$  中
• ${\displaystyle f(\epsilon ,g\,e)=\tau }$  这里的 ${\displaystyle f(\epsilon ,g)=\tau _{1}\to \tau }$  且 ${\displaystyle f(\epsilon ,e)=\tau _{1}}$ 
• ${\displaystyle f(\epsilon ,\lambda v:\tau .e)=\tau \to f(\epsilon _{1},e)}$  这里的 ${\displaystyle \epsilon _{1}=\epsilon \cup (v,\tau )}$ 

注意我们至今没有指定在不能满足各种条件的时候做什么。这是因为，在简单类型检查算法中，检查在任何事情出错的时候都失败。

现在，我们开发一个更复杂的算法来处理类型变量和在它们上的约束。所以，我们扩展原始类型的集合 T 来包括变量的无限补给，指示为小写希腊字母 ${\displaystyle \alpha ,\beta ,...}$ 。详情参见 ^[3]。

解方程

解方程通过合一进行。这是个意外简单的算法。函数 ${\displaystyle u}$  运算在类型方式上并返回叫做“代换”的一个结构。代换简单是一从类型变量到类型的一个映射。代换可以用明显的方式组成和扩展。

合一方程的空集是足够容易的: ${\displaystyle u\,\emptyset =\mathbf {i} }$ ，这里的 ${\displaystyle \mathbf {i} }$  是同一代换。

合一变量与类型以如下方式进行: ${\displaystyle u\,([\alpha =T]\cup C)=u\,(C')\cdot (\alpha \mapsto T)}$ ，这里的 ${\displaystyle \cdot }$  是代换合成算子，而 ${\displaystyle C'}$  是保持约束 ${\displaystyle C}$  于应用到它的新代换 ${\displaystyle \alpha \mapsto T}$  的集合。

当然 ${\displaystyle u\,([T=\alpha ]\cup C)=u([\alpha =T]\cup C)}$ 。

有趣的情况保持为 ${\displaystyle u\,([S\to S'=T\to T']\cup C)=u\,(\{[S=T],[S'=T']\}\cup C)}$ 。