史磊

仓颉语言类型推断技术专家

一、一种看待类型系统的方式

一门编程语言一定得包含类型系统吗？

这个问题今天看来可能显而易见，一个程序没有类型的话还能算是个完整、正确的程序吗？但是其实关于类型系统的作用，一直是存在两种针锋相对的看法的。大家普遍习惯的这种把类型作为程序不可分割的一部分的看待方式叫做“内生”（intrinsic）的理解方式，即一个程序如果没有合法的类型就不能算有意义的程序。而与之相对的，也存在一种“外生”（extrinsic）的理解方式，持这种观点的人认为，程序即使没有类型也同样有意义，类型检查只是额外地证明了这个程序的一些性质，与其他的各种程序分析工具应该处于同样的地位。

姑且不论类型检查是否应该作为一个语言之外的的工具这种工程问题，顺着“类型检查是为了证明了程序的一些性质”这个思路，我们可以得到一些很有趣的认知。

不妨想象一下，一个程序如果在没有类型的情况下就执行起来，会发生什么问题呢？我们有可能给一个函数传入一个整数，但是这个函数实际上却是处理字符串用的，于是它错误地把这个整数形式地数据当做字符串来处理了，最后自然是得不到期望的结果。例如下面的伪代码：

func f(s) {     s.replace(...) } ​ let s = f(1)

而在这个过程中加入类型系统的话，如果可以静态地验证这个被调用的函数的形参类型是一个字符串，而每次调用它时实参类型都也是字符串，那么我们就可以保证，在任何情况下执行这个程序，都不会出现把一个整数类型的参数传递给这个处理字符串的函数这种低级错误。

所以这里我们用比较朴素的方式去理解的话，类型系统、尤其是静态类型系统，实际上是一种“程序在运行时处理数据的方式永远不会出错”的证明，如果类型检查可以通过，那么每个数据被传递时，它的提供者和接收者对于这块数据的格式、可以被执行的操作等等的理解总是一致的。实际上，这个性质已经几乎就是一些比较公认的“类型安全”（type safety）的定义了。

另外细心的读者可能会注意到，既然类型系统是一种程序运行时“永远不会出错”的证明，那这个证明完成后，在程序运行时，我们还需要保留“类型”这个东西吗？确实如此，除了为了支持动态派遣等一些动态特性外，大多数静态类型的信息在类型检查完成后对于程序的正确运行就基本没有用处了，理论上是可以被擦除掉的。当然，实际的实现中类型信息对编译优化也有帮助，所以也有语言会选择在后续的编译阶段一直保留它们。

那么我们再回头去看这篇文章最关心的重点问题：类型推断是什么？类型标注又是什么？既然类型检查是一种正确性的证明，那开发者提供的类型标注自然就是手写的部分证明，而类型推断则是一种自动化证明的技术。自动化证明的算法越聪明，必须手写的部分也就越少，能支持的类型特性也就越丰富。实际上，在一些研究性的语言中，类型系统早已超越简单的“处理数据的方式”的正确性证明，还可以包括资源消耗、执行时长、数组长度、值的可空性等等多种方面的正确性证明，其中的类型推断用到的技术与更一般的形式化证明也越来越接近了。

二、仓颉的类型推断需要做什么

在仓颉语言中，类型推断主要起到两个作用，第一是确定每个声明和表达式的类型，这既包括可以省略的变量类型、函数返回类型、泛型实参类型等等，也包括分支、循环、字面量等并不涉及类型标注的各种表达式的类型。第二是帮助确定每个被使用的名字对应的声明，最典型的情况是在调用一个重载的函数时，需要确定调用的具体是哪个定义，另外有些不同种类的定义，如果碰巧名字相同，我们也可能需要借助类型信息来确定使用的究竟是哪个。

三、基于合一（unification）的类型推断

在一些早期的编程语言中，类型之间并没有子类关系，只有相等或不等。时至今日，多数函数式编程语言仍然继承了这个设计思路，包括 Rust 语言如果不考虑生命周期的话，类型之间也没有子类关系。在这些语言中，类型推断普遍是基于合一（unification）过程来完成的。简单来说，即是每当我们遇到一个暂不确定的类型，那就为它引入一个待解的变元，然后在遍历程序的过程中，不断建立起类型变元之间的方程组（如一个函数的形参类型和实参类型必须相等，由此就可以得到一个新的方程），并不断简化这些方程，直到所有类型变元都可以求解出来（或者缺乏足够的信息来求解，此时就会将这样的类型变元泛化，不过这超出本文的讨论范围了），类型推断的过程十分类似于数学上解方程的过程。

这种做法的好处是，这些方程组是从整个程序里所有信息中建立起来的，所以每个未知类型都可以利用全局信息去求解，解出的结果也可以保证是全局正确的。

例如下面这个程序在 Rust 中是可以编译通过的，它可以根据第 5 行的函数调用解出变量 v 需要有 u16 类型。但是等价的程序在一些没有全局的类型推断的语言中则无法通过编译，因为在第 4 行中 v 的类型就已经被推断为整数字面量的默认类型了，这通常是 u64。

fn f(x:u16) {} ​ fn main() {     let v = 1;     f(v); }

那么为什么不是所有语言都用这种基于合一（unification）的类型推断方式呢？主要问题就出在子类关系上。

如果类型间不存在子类关系，那么所有类型实际上是一些离散的点，两个类型要么相等，要么不等，几乎没有歧义的空间。这样求解方程非常简单直接，结果也很容易保证完备性和可靠性。

但是有了子类关系，类型之间就不再是一些毫无关系的点了，而是形成了一个偏序集。从程序中可以建立起的也不再是基于类型相等的方程组，而是基于子类关系的不等式组。求解一个偏序集上的不等式组则是一个复杂得多的问题，很多时候我们甚至无法在可接受的时间内求得一个完全精确的解，只能退而求其次做一些近似。这就导致基于合一（unification）的类型推断在有子类关系的语言中非常难以使用，而仓颉语言是有子类关系的，所以也暂时没有采用这种类型推断方式。

四、局部类型推断

上面讲的的子类关系会导致的问题，曾一度导致在有子类关系的语言中做类型推断的研究非常稀少。对于注重实用的工业语言来说，比较重要的一篇研究论文是 Benjamin. C. Pierce 等人著的 《Local Type Inference》1。它不再纠结于全局的完全性和完备性，退而求其次只追求每个表达式的类型在相邻表达式能提供的信息中保证正确。仓颉的类型推断基本上是基于这篇论文的框架在实现。

更准确地来说，《Local Type Inference》这篇论文实际上包含了两个类型推断的思想，一个是仅依据局部信息做类型推断，也就是“局部类型推断”，另一个是类型信息应该在表达式中自底向上和自顶向下双向传播，也叫“双向类型推断”。这两者在仓颉的类型推断实现中都有所体现，下面就具体来介绍一下仓颉的类型推断方式：

局部元素

在一个块内部，编译器会按从上到下的顺序依次处理各个表达式和局部声明。

在一个表达式或局部声明的内部，编译器依据可获得的类型信息，会做自顶向下或者自底向上的推断。

自顶向下的推断是指，父表达式如果对子表达式有期望的类型，则我们会借助这个期望类型的信息去推断子表达式的类型。一个典型的情形是，在一个函数调用表达式中，我们总是期望实参的类型是对应位置形参的子类，因而可以用形参类型作为期望类型去帮助推断实参类型。其他还包括 if 表达式的条件需要是 Bool 类型的子类，变量的初始化表达式的类型需要是变量类型的子类等等。

下面举一些例子：

func handleByte(b: Byte) { } ​ func f() {     let v: Int32 = 1 // 1 inferred to Int32     handleByte(2)    // 2 inferred to Byte ​     let v2 = 3       // 3 inferred to Int64 }

上面的程序中，第5行的变量 v 有类型标注 Int32，因此对其初始化表达式存在期望类型 Int32，所以整数字面量 1 被推断为类型 Int32。

第6行的 handleByte 函数有形参类型 Byte，因此这里的调用表达式对它的实参就有期望类型 Byte，所以整数字面量 2 被推断为类型 Byte。

以上都是自顶向下的推断发生的场景，而第8行中则没有发生自顶向下的推断。变量 v2 没有标注类型，所以字面量 3 就不具有任何从父表达式得到的期望类型，只能被推断为整数字面量的默认类型 Int64。

需要注意的是，自顶向下的期望类型在一些表达式中是可以向下传递的。例如，一个 if 表达式如果本身有期望类型，那么我们会认为它的各个分支同样有这个期望类型。

下面是一个例子：

func narrow(x: Int64):Byte {     let v: Byte = if (x >= 0) {         1       // 1 inferred to Byte     } else {         -1      // -1 inferred to Byte     }     return v }

其中变量 v 标注了类型 Byte，因此其初始化表达式、即 if 表达式会具有期望类型 Byte。然后 if 的两个分支也都会传递地具有期望类型 Byte。因而，第3行的 1 和第5行的 -1 字面量都将被推断为 Byte 类型。

除了 if 表达式以外，一个表达式的返回值如果可能来源于它的某个子表达式，那么对这个表达式的期望类型通常就可以传递给这个子表达式，如从 match 表达式到它的各个 case，从 try-catch 表达式到它的 try 分支和各个 catch 分支等等。

而自底向上的推断是指，如果父表达式对子表达式没有期望的类型，我们会先推断出子表达式的类型，并反过来用这个信息帮助推断父表达式的类型。一个典型的场景是调用泛型函数时，如果没有写出泛型参数，则通常需要先推断出实参的类型，然后才能依此求解出整个函数调用表达式的泛型参数，进而得到整个表达式的类型。

以下是一个简单的例子：

func id(x: T): T {     x } ​ let s = id("hello")     // will infer id

其中定义了一个接受一个任意类型的参数并返回其自身的泛型函数 id。第5行代码中，我们既不知道变量 s 的类型，也不知道调用的 id 函数的类型参数，所以只能先从最里层的表达式 "hello" 开始推断，得到它的类型为 String。然后向上，利用实参类型为 String，求解出此处调用 id 的泛型实参是 String，进而确定它的返回类型也是 String，最后再向上推断出变量 s 的类型是 String。

泛型参数求解

在调用泛型函数、或者构造泛型类型时，我们需要知道本次调用的泛型实参。函数调用的泛型实参通常可以省略，此时编译器会尝试从上下文中推断出泛型实参的类型。在局部类型推断中，这是最为复杂的步骤，也是唯一实际上用了合一（unification）的步骤。

上文介绍过，在有子类关系的类型系统上合一（unification）需要求解不等式组。那么我们需要首先建立这些不等式。因为局部类型推断并不考虑全局信息，所以针对一个特定的泛型函数的调用，我们只会考虑下面几个不等式的来源：

• 函数的形参类型需要是实参类型的父类

• 函数的返回类型需要是本次调用的期望返回类型的子类

• 函数的泛型约束需要被满足

具体求解的过程略为复杂，本文不会详细介绍。大致上来说，对于一个泛型参数，编译器会尝试寻找能满足以上所有约束的唯一最具体类型、或唯一最抽象类型，来作为这个泛型参数的解。如果这样的类型无法找到，则会编译失败。另外，如果找到的类型只能是 Any 或者 Nothing，则编译也会失败。

以下是一个简单的情形：

func tryPrint(x: Option) where T <: ToString {     if (let Some(v) <- x) {         println("Has value: ${v}")     } } ​ main() {     tryPrint(Some(1))   // will infer tryPrint }

第8行代码中 tryPrint 函数的泛型参数需要推断。它的形参类型和实参类型间的对应关系为 Option <: Option，此外它有泛型约束 T <: ToString。结合两者，我们发现类型 Int64可以作为 T 的解，所以此处 tryPrint 的泛型实参就被推断为 Int64。

另外在一些较为复杂的情形下，泛型函数的实参之间可能有类型信息的依赖，无法用一次简单的自底向上或者自顶向下推断完成泛型参数的求解。这种情形在原版的《Local Type Inference》中并没有解决，一个比较有名的后续工作叫做《Colored Local Type Inference》2，它通过一个十分重量级的方法 -- 给类型中每个类型参数再更详细地标上需要自底向上还是自顶向下推断出来 -- 来实现对这种情形的支持。

仓颉参考了这种思路，但是并没有引入那么重量级的标记，只是会在泛型函数调用时尝试多次迭代求解泛型参数。以经典的 map 函数为例：

import std.collection.ArrayList ​ func map(f: (T)->R, arg: ArrayList): ArrayList {     let res = ArrayList()     for (v in arg) {         res.append(f(v))     }     res } ​ main(){     let input: ArrayList = ArrayList([1, 2, 3])     let output = map({ x => x.toString() }, input)      // will infer map }

map 函数接受一个转换函数和一个列表，将列表中的元素逐一转换后输出新的列表。因为有转换前后两种不同类型，所以它需要2个泛型参数 T 和 R。

在第13行对 map 的调用中，泛型参数 T 可以很显然地从 input 参数的类型推断出来为 Int64，但是对它的另一个参数，即作为转换函数的 lambda，在没有期望类型的情况下，我们无法简单确定这个 lambda 的参数和返回类型，因而也就无法解出 R 的类型。

但同时我们又可以观察到，这个 lambda 的参数类型和 input 的类型都对应着泛型参数 T，因此他们应该相等。而知道lambda的参数类型后，他的返回类型就可以推断出来了。进而，R 的类型也可以求解出来。

所以总的来说，这种情形仍然是有足够的信息进行泛型参数的求解的，只不过需要跨越参数进行一些类型信息的传递。

对于这种参数之间有类型信息的依赖的泛型函数调用，我们的处理流程是这样的：

1. 首先，推断出所有不需要期望类型就可以推断成功的实参的类型

2. 然后用推断出的实参类型尽可能地求解泛型参数的类型

3. 将可以求解出的泛型参数代入形参类型中，将这些（可能没有完全实例化的）形参作为期望类型去推断对应的实参类型，这个过程中，我们会忽略掉类型中没有完全实例化的部分

4. 重复 2、3 步，直到没有新的泛型参数可以被求解（即失败），或者所有泛型参数都可以被求解（即成功）

最后还有一种较为特殊的场景，有些函数可能定义成柯里化的形式，即每次接收一个参数，返回接收下一个参数的函数。

例如，仓颉标准库中的 map 函数就提供了柯里化方式定义的版本：

public func map(transform: (T) -> R): (Iterable) -> Iterator {     return {it: Iterable => it.iterator().map(transform) } }

柯里化的函数调用时，会分为多次函数调用：

let it = map({x=>x.toString()})([1,2,3])

当然，通常我们写成管道操作符的语法糖形式：

let it = [1, 2, 3] |> map{x=>x.toString()}

这种情形下，柯里化的泛型函数的多次调用是连续发生的，它泛型参数仍然可以被推断出来，编译器会将后面的调用中的实参类型信息以期望的返回类型的形式向前传播，帮助推断泛型参数。

也就是说，对于第一次对 map 的调用 map({x=>x.toString()})，我们可以知道它的返回类型需要满足： (Iterable) -> Iterator <: (Array) -> Any。然后使用上面描述过的求解步骤，就可以解出 T 和 R 分别为 Int64 和 String。

重载决议

仓颉语言支持函数和操作符的重载，在编译时，需要静态地做重载决议，以确定每个重载函数的调用究竟用了哪个定义。

仓颉做重载决议的过程大致上可以分为3步：

1. 找出当前（调用）位置可见的候选定义

2. 检查每个候选定义是否能通过调用处局部的类型检查

3. 在所有可以通过类型检查的定义中，选取最匹配的一个

更具体的规则可以在用户手册或者语言规约中找到，这里就不再赘述。这里主要讨论2个在重载决议过程中值得一提的点。

第一点是，如果被调用函数的某些候选定义是泛型函数，且需要求解泛型参数，那么对每个候选定义会分别进行泛型参数的求解。

例如在下面的程序中，第8行对 f 的调用，若选取第1行的定义，则可以求解出泛型参数 T 为 String，若选取第4行的定义，则可以求解出泛型参数 T 为 Int64。两者皆可类型检查通过，所以会报错无法决议。

func f(x: Int64, y: T) { }  func f(x: T, y: String) { }  main() {     f(1, "c") // Error, both candidates match, ambiguous }

第二点则是因为上面提到的双向类型推断而衍生出的问题。

因为我们采用的双向类型推断策略，一个函数调用期望的返回类型对一个候选定义能否通过“局部的类型检查”会产生影响，因而可能改变重载决议的结果。也就是说，一个重载函数的调用，在不同上下文下，决议的结果是可能不同的。

例如下面的程序中，第10行的 f 会考虑到期望的返回类型是 Int32 而选择第5行的定义，而第11行的 f 会考虑到期望的返回类型是 Int64 而选择第1行的定义。

func f(x: Int64):Int64 {     x }  func f(x: Int32):Int32 {     x }  main() {     let v1: Int32 = f(1)     // will use definition of line 5     let v2: Int64 = f(1)     // will use definition of line 1 }

那么我们再考虑一种特殊的情况，如果有多层重载函数的调用嵌套起来，会发生什么事呢？因为外层函数的形参会被视为内层函数调用的期望类型，而外层函数的形参类型会依候选定义的选取而有所变化，所以外层对候选定义的选取同样会影响内层的重载决议。

例如下面的程序中，第10行外层的 widen 会考虑到期望的返回类型是 Int32 而选择第5行的定义，而内层的 widen 会考虑到外层期望的参数类型是 Int16 而选择第1行的定义，最后，字面量 1 会因为第一行的 widen 定义期望一个 Int8 类型的参数而被推断为 Int8 类型。程序整体可以通过类型检查。

func widen(x: Int8):Int16 {     Int16(x) }  func widen(x: Int16):Int32 {     Int32(x) }  main() {     let v: Int32 = widen(widen(1))      // 1 inferred to Int8 }

这就产生了一个问题，重载函数嵌套层数较多的情形下（如比较大的UI组件、复杂的算术表达式等），我们做决议可能需要搜索各层的候选组合，而需要搜索的组合数可能随着嵌套层数而指数增长，这就可能让编译时间长到无法接受。实际上同样的问题也可以在 Swift 语言中观察到，例如至少在撰写本文时，Swift 的编译器仍然会因为如下的程序编译超时：

let a: Double = -(1 + 2) + -(3 + 4) + -(5)

这和 Swift 同样使用了双向类型推断不无关系。

那么仓颉是如何解决这个问题的呢？让我们回忆一下，一个函数的重载决议总共需要哪些信息？

1. 当前的表达式

2. 对当前表达式的期望类型

3. 当前上下文中的符号表

其中对于源程序中同一个位置的表达式， 1 是完全不变的，3 可以近似认为不变，事实上会导致指数的搜索量的是 2 在不同上下文中会有所不同。看到这里，经常刷算法题的朋友可能可以敏锐地发现，在双向类型推断下做重载决议实际上几乎是一个动态规划问题。对于给定的程序位置和期望类型，只要上下文中的符号表不发生改变，那么当前位置的表达式能否通过类型检查就是一个具有最优子结构的问题。而所有可能的期望类型并不是很多，它最多等于父表达式调用的函数的候选定义的总数。

因此，我们可以在重载决议时做一个记忆化搜索，对同一个函数调用，如果用同样的期望类型已经做过类型检查，直接复用前一次检查时缓存的结果就好了。而在一些特殊情形下，如果符号表确实发生了变化，只要将受影响的缓存清除掉即可。如此一来，对于绝大多数程序，重载决议都可以在接近多项式的时间复杂度内完成。

六、小结

本文简单介绍了业界对类型系统和类型推断相关的讨论和已有工作，并介绍了在仓颉的实践中类型推断遇到的问题和解决的方式。仓颉使用了基于局部类型推断的算法框架，并针对一些常见的使用场景做了专门的优化，在推断能力、算法复杂度、以及支持的语言特性间达到了一个不错的平衡点。

七、参考文献

• [1] Pierce B C, Turner D N. Local type inference[J]. ACM Transactions on Programming Languages and Systems (TOPLAS), 2000, 22(1): 1-44.

• [2] Odersky M, Zenger C, Zenger M. Colored local type inference[J]. ACM SIGPLAN Notices, 2001, 36(3): 41-53.