ML语言的背后

众所周知, ML系语言十分强大, 这不仅仅得益于它们丰富的语义(高阶函数, local binding, lambda), 还得益于这套语义背后强大的类型系统. ML语言的类型系统通常支持十分强大类型推导功能, 强大到什么程度呢? 理论上开发者可以忽略所有类型签名, type checker仍然可以推导出所有的类型签名.

类型推导的两个"端点"

但是, 如此强大的类型推导技术居然也不小心带来了一些负面影响:

  1. 重要的类型签名被忽略. 很多情况下, 类型签名并不是开发者的负担而是起到了 “verified document” 的作用, 对可读性有着关键的影响.
  2. 类型系统的复杂度增加(主要是类型推导部分). 直观来看这点是在语言实现上的负面影响, 但是过于复杂的类型推导除了会提升类型检查的复杂度也会带来编程的"负担". 比如说开发者如果不能明确知道哪些类型能推导哪些类型不能推导, 那么考虑"要不要加上类型签名"的这个问题就会给程序员带来心智负担.

对于这些负面的影响, 最极端的做法就是我们要求把所有的类型都加上, 直接抛弃类型推导功能.

你不是说我推导不好吗, 那你自己写上吧.

但是这又带来了新的问题:

  1. 为所有类型写上类型签名实在是太啰嗦了, 维护一个冗长但是又没有意义的类型签名, 反而会带来编程时的心智负担.
  2. 很多类型签名实际上是"噪音". 如果完全抛弃类型推导, 那么在一个程序中, 有可能类型签名比描述程序执行信息的核心部分还要多, 这样的类型噪音甚至反而会影响程序的可读性.

尝试找到类型推导平衡点

那么有没有一种办法设计一个类型系统, 可以在描述ML丰富的语义的同时引入"适量"的类型推导: 当显式写出类型签名的对开发者有益的时候不推导这个类型, 只选择推导"显式写出时无意义"的类型签名.

局部类型推导(Local-Type inference)技术就诞生了

作者总结了3种ML编程中常见的类型推导, 并通过局部类型推导技术完成这三种类型推导:

  1. 函数调用时类型参数的推导是必要的
  2. 匿名函数的类型推导是需要的
  3. local binding的类型推导是需要的

局部类型推导(Local-Type inference)

局部类型推导尝试在保持ML编程的前提下尽可能的减弱类型推导的能力以简化类型推导算法, 局部的含义是类型推导只用到了局部的语法树的类型信息.

通过Local Type Argument Synthesis可以解决第一个问题, 通过双向类型检查(Bidirectional Type Checking)可以解决问题2, 3.

语言定义

先介绍了一个用于展示的简单的语言, 是沿用的一个叫 (Kernel F≤_) 的语言, 这个语言支持subtype, 参数化多态, 匿名函数, 局部绑定.

我觉得很有意思的一点是, 文中把同一个语言区分了两层: 分别是内部语言(internal language)和外部语言(external langauge). 内部语言是full typed language, 外部语言是程序员日常接触的语言是可以省略一些类型签名的. 而类型推导的过程就是把外部语言翻译成内部语言的过程. 这个隔离可以让"推导了什么东西"很清楚的展现.

Figure 1: 内部语言的定义: 类型表达式, 表达式, 类型环境

Figure 1: 内部语言的定义: 类型表达式, 表达式, 类型环境

Bottom Type的引入可以让任意两个类型都有最大下界, 可以让类型推导总有解.

Figure 2: 子类型规则

Figure 2: 子类型规则

需要注意这里是有forall类型的子类型关系的, 之后理解约束生成/求解规则需要用到.

  • note: 参数类型也可以有forall, 那是不是说local type inference并没有rank-2 type的限制呢?

Local Type Argument Synthesis

Figure 3: Declarative Rule

Figure 3: Declarative Rule

这条规则的有2个要点:

  1. 如果调用目标的类型是 \( All(X)T \rightarrow R \), 并且调用的时候没有显式的给出类型参数, 那么需要通过推导 类型实参;
  2. 类型实参需要满足: 应用该类型实参后可以得到最小的函数返回类型.

但是这条规则是声明式的, 为了能够得到一个可用的类型推导算法, 我们还要知道如何得到这个"可以让返回值最小的类型实参".

于是就有了算法式规则.

Figure 4: Algorithmic Rule

Figure 4: Algorithmic Rule

该规则的算法含义是: 当需要infer \(f(\bar e)\) 的类型时, 我们需要做以下几件事情:

  1. 先infer \(f\) 的类型;
  2. infer 函数调用参数 \(e\) 的类型 \(\bar S\) ;
  3. 如果 \(f\) 的类型是一个需要类型参数的函数(即 \(|X| > 0\)), 那么就需要类型推导推导出函数的类型参数;
  4. 把空集 \(\emptyset\), 类型 \(\bar S\), 形参类型 \(\bar S\), 类型形参 \(\bar X\), 喂给由关系 \(\vdash \Rightarrow\) 定义的函数, 从而生成类型变量 \(\bar X\) 上的约束集合 \(\bar D\) ;
  5. 通过运算符 \(\wedge\) 合并 \(\bar D\) 得到 \(\bar C\) ;
  6. 求解约束 \(\bar C\) 得到能够让 \(R\) 最小的 unifier \(\sigma\)
  7. 将 \(\sigma\) 再apply到 \(\bar X\), 返回在internal term中填补空缺的类型实参.

可以看到, 相比与声明式规则, 算法式规则中多了 \(C\) 和 \(\sigma\) . 其中 \(C\) 是在检查函数调用表达式时收集到的约束结合, \(\sigma\) 是对这些约束求解的结果.

  • 疑惑: 这里是不是有遗漏? 应该要像声明式规则一样把 f 翻译成 f' 的过程.

很清晰对吧!

约束生成

约束生成规则关系 \(V \vdash_{\bar X} S <: T \Rightarrow D \), 描述了对于包含类型变量\(\bar X\)的子类型关系 \(S <: T\) 和可以替换成任意类型的类型变量集合\(V\), 需要生成的关于 \(\bar X\) 类型约束集合 \(D\). 对于任意的 \(V\) 的替换都能满足 \(S <: T\), 当且仅当 \(\bar X\) 满足类型约束 \(D\).

为什么要有一个 \(V\) 呢? 因为文章中用于展示的语言的类型并没有rank-2的限制, 当我们尝试为一个子类型关系生成约束时, 类型中有的变量是free的(我们需要生成约束的变量), 有的变量是被 \(ALL\) capture 的. 而对于这些captrured变量, 我们不知道关于它们的任何信息, 所以需要按照这个目标来生成free变量约束: 对于所有被capture的变量的替换, 子类型关系都能成立.

Figure 5: 约束生成的关系

Figure 5: 约束生成的关系

这个关系中用到了两个辅助的关系 \(\Uparrow\) 和 \(\Downarrow\), 叫做 Variable Elimination. 这两个关系就不复杂了, 而且是完全对称的.

Figure 6: Variable Elimination关系

Figure 6: Variable Elimination关系

\(S \Uparrow^V T\) 表示对于类型 \(S\), \(T\) 是满足以下条件的最小上界类型: \(T\) 大于\(S’\), \(S’\)为任意把 \(S\) 中的 \(V\) 替换为任意类型后得到的类型.

原文中的描述更加简单, 就说要eliminate掉这些变量.

In the constraint generation algorithm that we present in the next section, it will sometimes be necessary to eliminate all occurrences of a certain set of variables from a given type by promoting (or demoting) the type until we reach a supertype (or subtype) in which these variables do not occur.

约束求解

约束生成将为\(\bar X\)中的每个变量生成一个上限和下限, 约束求解将给每个\(X\)一个具体的类型, 具体来说就是取能让返回类型最小的边界条件.

类型变量\(X\)在类型\(T\)中出现的位置可以分为4类covariant, invariant, contravariant和constant. 个人通俗的解释是:

  1. Covariant: 表示类型X增长, 类型T也会随之增长(如\(T = (…) \rightarrow X\));
  2. Contravariant: 表示类型X增长, 类型T也法内容会随之下降 (如\(T = (… X …) \rightarrow …\));
  3. Invariant: X发生变化为X’后, 只要X与X’不同, T’与之前的T是不存在子类型关系的;
  4. Constant: X随便替换成什么, 替换后的类型均有子类型关系.

严谨的定义如下:

Figure 7: covariant, invariant, contravariant和constant

Figure 7: covariant, invariant, contravariant和constant

Figure 8: 约束求解

Figure 8: 约束求解

因为有subtype的存在, 这里的约束求解与let polymorphism中的unification稍微有些不同, unification基于 \(=\) 约束得到unifier, 此处基于 \(\le\) 约束和类型变量在返回类型中所处的位置得到unifier.

双向类型检查(Bidirectional Checking)

双向类型检查更像是一种类型检查的风格, 把类型检查分为了两个过程: check和infer.

check过程是: “已经有一个term出现在了一个需要类型T的上下文中, 我们需要check这个term是否真的为类型T”;
infer过程是: “对于一个term, 不知道这个term所在的上下文需要什么类型, 我们需要在上下文中infer这个term的类型”.

这也是Bidirectional名称的由来: 我们既可以通过check把类型信息传递给子节点, 也可以通过infer把类型信息传递给父节点.

Figure 9: Bidirectional Checking的规则

Figure 9: Bidirectional Checking的规则

从规则中可以看到, 每一个term分别有两条规则, 一类是C开头的check, 另一类是S开头的Synthesis(就是Infer).

比较复杂的是Application节点的check&infer:

  1. 只有在Application节点, check会调用infer推导调用目标的类型, 然后根据该类型再check调用参数的类型是否兼容, 并生成类型兼容需要满足的约束条件:
    1. 类型信息就是这样被带到了函数调用的实际参数;
    2. 类型实参也是在这个时候被上一节描述的算法被推导出来.
  2. Abstraction的check过程就是利用了1的类型信息以推导函数的参数类型.

从规则中我们也能看到相比与let-polymorphism的不足, 在Abstraction的infer中, 我们必须写出类型参数, local-type-inference是不支持自动推导泛型参数的.

Bidirectional?

相比与原版的let polymorphism, 对于推导let binding type annotation的能力是要弱很多的, 虽然Bidirectional checking这个词是被local type inference提出的, 但是我觉得类型推导算法实际上都有类似 “bidirectional” 的过程.

类型推导还是一个收集约束然后求解约束的过程,

比如说在HM类型系统中, 我们需要不断的基于类型约束更新类型环境(环境如果关联了语法树上的类型信息的话, 那么语法树上的类型信息也会被更新). 这不也可以算是 environment <-> term 之间的bidirectional吗: 在environment中检查term; 在检查的过程中将收集到的约束"反馈"给environment.

HM type system在类型检查的过程中无时无刻不在基于新发现的约束更新环境; 而local type inference不会在类型检查过程中更新类型环境, 只允许利用局部的类型信息进行推导.

现实世界的编程语言

目前看到的编程语言, 要么采用像Haskell和OCaml这样的全局类型推导, 要么采用局部类型推导(Java, Scala), 并且都没有超过rank-2的限制(也就是说从理论上来说, local type inference还可以做更多). 然而局部类型推导是没有像let-polymorphism这样 泛化(generalize) 一个函数的能力的,

最近出的MoonBit采用了一种以前从来没见过的方案, 我觉得挺机智:

  1. 模块级别的函数必须手动标注类型;
  2. 局部函数可以具有类似let-polymorphism的能力

这样即可以限制类型推导的实际开销(只要\(O(n^2)\)的n足够小, 那就和常量差不多), 又具有let-polymorphism.