原文链接：Efficient and Insightful Generalization
作者：Oleg Kiselyov
摘要
Hindley-Milner 类型推导的实现并非只有 W 算法一种。1988 年，Didier Rémy 在研究如何加快 Caml 的类型推导速度时发明了一种优雅的类型泛化算法。这种算法无需扫描类型上下文，因而速度奇快。这种算法还能顺利扩展以捕获逃逸出作用域的局部类型声明，以及应用到支持全称量化类型以及存在量化类型的系统，甚至是 MLꟳ 系统中。
遗憾的是，算法本身以及算法在 OCaml 类型检查器的实现都鲜为人知，而且缺乏文档。本文旨在解释和普及 Rémy 算法，并解密 OCaml 检查器的一部分实现代码。本文还旨在保存 Rémy 算法的发明史。
Rémy 算法的魅力在于：它洞见到了类型泛化与依赖追踪的内在关联——即自动内存管理系统（如区域或分代垃圾收集）中所使用的追踪内存的方式。类型泛化可以视作在「给带有类型注释的抽象语法树中共享类型的节点加上连接边」所组成的图中寻找支配节点的过程。在 Fluet 和 Morrisett 的区域演算中，他们通过「类型变量能否泛化」判断区域中是否包含某资源。无独有偶，Rémy 的算法则通过测试「区域是否包含某类型变量」，从而决定该变量是否可被泛化。
导言
本文最初是为了了解 OCaml 类型检查代码而做的笔记，OCaml 类型检查器的代码庞大、复杂，而且几乎完全没有文档。在挖掘这些代码的过程中，我们发现了真正的宝藏，其中之一就是一种高效而优雅的类型泛化［type generalization］算法，下面将重点介绍。
OCaml 类型检查代码使用的泛化算法基于对类型的所谓等级［level］的追踪。这些「等级」也能避免模块中定义的类型逃逸到更大的范围——对于局部引入的类型构造函数而言，等级机制强制执行了区域封锁。令人感兴趣的一点在于如何统一处理泛化和区域。此外，OCaml 类型检查程序中等级还有更多的应用——如检查多态记录类型和存在量化记录类型。MetaOCaml 也间接依赖等级来跟踪未来阶段的变量绑定范围。
所有这些应用都有一个共同点：需要跟踪依赖关系，或者说需要计算数据依赖关系图中的区域范围或支配节点［dominator］。这令人回想起 Tofte 和 Talpin 提出的基于区域的内存管理技术。正如 Fluet 和 Morrisett 所展示的：我们可以利用全称量化类型［universal type］来静态地防止已分配的数据逃离其区域，因此可以在 F 系统［System F］中编码 Tofte 和 Talpin 提出的区域类型系统。同理，基于等级的类型泛化通过检测类型变量的逃逸位置来确定其区域，以及泛化引入的全称量化的具体位置。
OCaml 中的类型泛化程序（部分）实现了 Didier Rémy 于 1988 年发现的算法。其理念在于：在有类型标注的抽象语法树中显式表达类型共享。类型变量只能在「支配了该变量所有出现过的节点」的节点上量化。类型泛化相当于在增量式计算依赖图的支配节点。Rémy 的 MLꟳ 系统就是这一理念的自然发展。
令人遗憾的是，Rémy 的泛化算法及其基本思想鲜为人知。在 OCaml 类型检查器这样的实现中，除了源代码里几条简短且令人费解的注释以外，几乎没有文档。这一算法应当被人所了解，为了实现这一目标，本文首先将详细阐述算法的动机和实现，希望以此解明算法背后的直觉，并给出一个草稿实现；然后将部分解析 OCaml 所使用的类型检查器。
本文的第二部分则是对 OCaml 类型检查程序中部分代码的评注，因此具有相当的技术性。这些评注具体参考了 OCaml 4.00.1 版本的类型检查代码，它们位于 OCaml 发行文件的 typing/ 目录中。其中，typecore.ml 文件是类型检查程序的核心部分：它为抽象语法树中的节点标注类型和类型环境。具体来说，它将 Parsetree（定义于 parsing/parsetree.mli 中）转换为 Typedtree。文件 ctype.ml 则实现了统合函数与等级的相关操作。
我要感谢 Didier Rémy 的评论、解释、见解，以及他对算法发明过程的回忆。Jacques Garrigue 在「OCaml 类型检查程序如何利用等级实现各种功能」这一点提出了有益的意见和解释，在此一并感谢。此外，还要感谢 Matthew Fluet 和 Baris Aktemur 提供的其他参考资料。
版本
当前版本为二〇一三年二月版
引用文献
出自 Research Report 1766, Institut National de Recherche en Informatique et Automatique, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992。
- Matthew Fluet and J. Gregory Morrisett: Monadic Regions
该论文表明，实现关于内存区域管理的健全类型系统只需使用参数性多态［parametric polymorphism］，出自 J. Functional Programming, 2006, v16, N4-5, pp. 485-545。
类型泛化
本节将回顾 Hindley-Milner（下称 HM）类型系统的类型泛化规则，强调朴素泛化实现的微妙及低效之处。正是这些低效之处促使 Rémy 发明了基于等级的类型泛化算法。
回顾 HM 系统中的类型泛化规则：给定类型 $τ$ 以及类型环境 $Γ$，设 $α_{n}$ 为所有在 $τ$ 中且不在 $Γ$ 中的自由类型变量，$\mathsf{GEN}\left(Γ,τ\right)$ 表示对于 $τ$ 中所有变量 $α_{n}$ 进行全称量化。这句话也可以用奇怪的数学符号表述如下
$\begin{equation} \mathsf{GEN}\left(Γ,τ\right)=∀α_{1}…α_{n}. τ\; \mathbf{where} \left\{α_{1}…α_{n}\right\}=\mathsf{FV}\left(τ\right)-\mathsf{FV}\left(Γ\right) \end{equation}\tag*{}$
用 HM 类型系统的术语描述：量化会将类型转换为所谓「类型模板」。类型泛化在 HM 系统中用于检查 let 表达式的类型：
$\begin{equation} \dfrac{Γ⊢e\colon τ\quad{}Γ,\left(x:\mathsf{GEN}\left(Γ,τ\right)\right)⊢e_{2}\colon τ_{2}}{Γ⊢\mathbf{let}\; x=e\; \mathbf{in}\; e_{2}\colon τ_{2}} \end{equation}\tag*{}$
这意味着：在对 let 表达式的主体进行类型检查前，类型检查器会先泛化 let 所绑定的变量的类型。ML 对这种泛化添加了额外的条件，即值限制［value restriction］：let 所绑定的表达式 e 不能有可被观察到的副作用——技术上说，e 必须在语法上满足非扩张［non-expansive］性。OCaml 放宽了这种限制，详情参考本文后面的内容。
下面一个简单的例子展示了何为类型泛化：
fun x -> let y = fun z -> z in y
(* 'a -> ('b -> 'b) *)
对于表达式 fun z -> z，类型检查器推导出类型 β -> β，β 是一个全新（因此独一无二）的类型变量。fun z -> z 在语法上是一个值，所以类型检查器会泛化类型变量 β，并赋予变量 y 类型 ∀β. β -> β。由于 y 已经是多态类型，所以它可以出现在不同类型的上下文中，并应用于不同类型的参数，如：
fun x ->
let y = fun z -> z in
(y 1, y true)
(* 'a -> int * bool *)
$\mathsf{GEN}\left(Γ,τ\right)$ 只对在类型 $τ$ 中出现，但不在 $Γ$ 中出现的自由类型变量进行量化。这个条件虽然微妙，但是至关重要：如果没有这个条件，下面的函数就会被推导为不健全的类型 α -> β
fun x -> let y = x in y
为了推导出这个函数的类型，我们要先推出其函数体 let y = x in y 在类型环境 x:α 中的类型，这里的 α 代表一个全新的类型变量。根据上文关于 let 的推导规则，可推变量 y 的类型为：Gen(x:α, α)。显然，α 在环境 x:α 中。然而如果我们对其量化，y 的类型就会变成多态类型 ∀α. α。结果就是，函数名义上可以将其实例化为任何类型的值，并导致我们最开头所展示的不健全的结果。
因此，我们必须确保所有需要量化的类型变量都不在类型环境中。一个朴素的想法是：通过查询每个 let 绑定的变量的类型，从而扫描整个类型环境——事实上，Caml 实现最初就是这么做的。然而类型环境可能会很大：典型的 ML 函数包含了非常长的 let 表达式序列。非递归 let 会包含之前的所有 let 绑定，而递归 let 除此之外还会包含自己的 let 绑定，扫描单个 let 的类型环境的复杂度与函数大小成线性关系，那么整个程序的类型检查的时间复杂度将与程序大小成四次方关系（除了极端情况以外，HM 类型推导几乎只与程序大小成线性关系）。Didier Rémy 如此回忆道：
The inefficient generalization was one of the main reasons for the slow speed of Caml compilation. Bootstrapping the compiler and type checking two mutually recursive functions for compiling patterns and expressions took 20 minutes.
译：类型泛化的低效是 Caml 编译速度慢的主要原因之一。当自举编译器时，对用于编译匹配模式和表达式的两个相互递归函数进行类型检查需要 20 分钟。
一定有方法可以避免扫描类型环境。下一节将介绍这种方法。
不健全的泛化就如同错误管理的内存
本节开始介绍 Rémy 算法背后的思想，并将这一思想与基于区域［region］的内存管理方法建立联系。为了具体说明，我们使用一个玩具级 HM 类型推导器。在本节中，这个类型推导器对自由类型变量进行全称量化时没有考虑其类型环境，并导出不健全的结果。
通过详细检查三个简单例子的类型，我们可以将不健全的类型推导和手动内存管理一个常见的问题联系起来：释放仍在使用的内存。而下一节则从已有的防止过早释放资源的方法中汲取灵感，从而解决类型泛化不健全这一问题。
虽然我们使用的 HM 推导器是一个玩具实现，但它与真正的 OCaml 类型检查器有着相同的实现决策（甚至函数名称也相同）。理解它有助于理解本文的稍后部分讨论的 OCaml 内部结构。
我们的玩具语言是带有 let 的标准纯 $λ$-演算。其具体表达式为：
type exp =
| Var of varname (* 变量 *)
| App of exp * exp (* 函数应用: e1 e2 *)
| Lam of varname * exp (* 函数抽象: fun x -> e *)
| Let of varname * exp * exp (* let x = e in e2 *)
该演算的类型由以下部分组成：类型变量（可以是自由的也可以是已绑定的），已量化的类型变量以及函数类型。
type qname = string
type typ =
| TVar of tv ref (* 类型（模板）变量 *)
| QVar of qname (* 量化后的类型变量 *)
| TArrow of typ * typ
and tv = Unbound of string | Link of typ
带有 QVar 标签的是类型模板，反之为简单类型。在 HM 系统中，类型模板（或量化类型）是逻辑学中的前束范式［prenex form］（即全称量词只能在最外侧），因此不需要显式标出量词。
我们遵循 Prolog 传统，用引用单元［reference cell］来表示这些类型变量。一个未绑定的类型变量内可能包含 null 或 self 指针——在我们的例子中，为了方便打印，其包含的是变量本身的名字。当某自由类型变量与类型 t' 统合［unification］后，算法会把该变量对应引用单元的内容更新为指向 t' 的指针。为了防止出现循环（对我们的例子来说是不健全的）类型，首先需要检查其是否已经出现过：occurs tv t' 会遍历 t'，若遍历时遇到了类型变量 tv，那么就抛出异常。
let rec unify : typ -> typ -> unit = fun t1 t2 ->
if t1 == t2 then () (* t1 与 t2 是同一个类型变量 *)
else match (t1,t2) with
| (TVar {contents = Link t1},t2)
| (t1,TVar {contents = Link t2}) ->
unify t1 t2
| (TVar ({contents = Unbound _} as tv),t')
| (t',TVar ({contents = Unbound _} as tv)) ->
occurs tv t'; tv := Link t'
| (TArrow (tyl1,tyl2), TArrow (tyr1,tyr2)) ->
unify tyl1 tyr1;
unify tyl2 tyr2
(* 其他情况都会抛错 *)
类型检查器本身则中规中矩，它负责推导出表达式 exp 在类型环境 env 下的类型：
type env = (varname * typ) list
let rec typeof : env -> exp -> typ = fun env -> function
| Var x -> inst (List.assoc x env)
| Lam (x,e) ->
let ty_x = newvar () in
let ty_e = typeof ((x,ty_x)::env) e in
TArrow(ty_x,ty_e)
| App (e1,e2) ->
let ty_fun = typeof env e1 in
let ty_arg = typeof env e2 in
let ty_res = newvar () in
unify ty_fun (TArrow (ty_arg,ty_res));
ty_res
| Let (x,e,e2) ->
let ty_e = typeof env e in
typeof ((x,gen ty_e)::env) e2
检查器中的函数 newvar 分配一个全新的 TVar 值，并赋予其独一无二的名字；函数 inst 负责实例化一个类型模板：如果其参数是 QVar 值，则用一个全新的 TVar 值替换之。但下面的泛化函数 gen 是不健全的，它无视类型环境，全称量化了类型中所有的自由类型变量：
let rec gen : typ -> typ = function (* 不健全的量化！ *)
| TVar {contents = Unbound name} -> QVar name
| TVar {contents = Link ty} -> gen ty
| TArrow (ty1,ty2) -> TArrow (gen ty1, gen ty2)
| ty -> ty
量化过程就是将所有的 TVar 替换成相应的 QVar。原来的 TVar 被隐式「释放」了：每当一个自由类型变量被绑定后，该自由变量就会「消失」，取而代之的是一个指向已绑定变量的「指针」。
函数 typeof 所做的就是分配自由类型变量，对这些变量进行统合，在量化之后释放这些变量。下面用一些简单的例子来展示这三个函数是如何操纵自由类型变量的，第一个例子应该不会出错：
fun x -> let y = fun z -> z in y
通过追踪类型检查的过程，可以将类型变量有关的操作序列展示如下：
1 ty_x = newvar () (* fun x -> … *)
2 ty_e = (* let y = fun z -> z in y *)
3 ty_z = newvar (); (* fun z -> … *)
3 TArrow(ty_z,ty_z) (* fun z -> z 推导为左侧类型 *)
2 ty_y = gen ty_e (* ty_z 仍为自由变量，量化之 *)
2 deallocate ty_z (* 已被量化，释放 *)
1 TArrow(ty_x, inst ty_y) (* fun x -> … 推导为左侧类型 *)
第一列的数字代表递归调用 typeof 函数的深度。由于 typeof 只在抽象语法树［Abstract Syntax Tree, AST］的每个非叶子节点上递归调用自己，因此该函数的递归深度就是被类型检查的节点在 AST 中的深度。推导出的类型为 'a -> 'b -> 'b，符合我们的预期。一切都没错。
而第二个例子就是我们之前所提到过的，不健全的泛化函数导致推导出不健全的 'a -> 'b 类型：
fun x -> let y = x in y
按照上述方法制图便可发现问题所在：
1 ty_x = newvar () (* fun x -> … *)
2 ty_e = (* let y = x in y *)
3 inst ty_x (* x 推导为左侧类型，与 ty_x 一致 *)
2 ty_y = gen ty_e (* ty_x 仍为自由变量，量化之 *)
2 deallocate ty_x (* 已被量化，释放 *)
1 TArrow(ty_x, inst ty_y) (* fun x -> … 推导为左侧类型 *)
类型变量 ty_x 是返回类型的一部分，在深度 1 时仍被使用；但它却在深度 2 时就被量化且释放了。程序错误释放了仍在使用的资源。
第三个例子也有问题，不健全的类型泛化再次导致推导出不健全的类型 ('a -> 'b) -> ('c -> 'd)：
fun x -> let y = fun z -> x z in y
重施故技即可再次发现问题：
1 ty_x = newvar () (* fun x -> … *)
2 ty_e = (* let y = … *)
3 ty_z = newvar () (* fun z -> … *)
4 ty_res = newvar () (* 类型检查表达式：x z *)
4 ty_x := (* ty_x 合一后类型如下 *)
4 TArrow (ty_z,ty_res)
4 ty_res (* x z 推导为左侧类型 *)
3 TArrow(ty_z,ty_res) (* fun z -> x z 推导为左侧类型 *)
2 ty_y = gen ty_e (* ty_z, ty_res 仍为自由变量，量化之 *)
2 deallocate ty_z (* 已被量化，释放 *)
2 deallocate ty_res (* 已被量化，释放 *)
1 TArrow(ty_x, inst ty_y) (* fun x -> … 推导为左侧类型 *)
类型变量 ty_z 以及 ty_res 在深度 2 处就被量化并释放，但这两个变量又是 ty_x 的类型 TArrow (ty_z, ty_res) 的一部分，而 ty_x 又是返回类型的一部分。
上述所有推导出不健全类型的例子都存在所谓「内存管理问题」：程序过早释放了仍在使用的内存（TVar）。这并非偶然，一个被量化的类型变量可以实例化成任意类型，但是仍处于类型环境中的变量则不能被随意实例化，否则会影响其他部分的表达式的类型检查。同理，当我们释放一块内存后，语言运行时就可以用任意数据覆盖这块内存，或者重新将这块内存分配出去。程序的剩余部分不应该依赖被释放的内存——因为我们已经认定剩下的程序里不再需要这块内存。事实上，我们可以将「不再被使用的内存」这一概念定义为：任意修改这块内存都不会对剩余的程序造成影响。释放仍在被剩余程序所使用的内存通常会导致程序崩溃，同理，上述例子中推导出的不健全类型也往往会导致同样的结果。
引用文献
玩具类型推导器的完整代码，会造成不健全的泛化，内附带更多推导出不健全类型的示例。
基于「等级」的高效泛化
本节继续阐释 Rémy 算法的中心思想。现在我们已经认识到不健全的类型泛化如何与「释放仍被使用的内存」这一概念形成关联，那么我们就可以运用所有权［ownership］追踪或区域［region］内存管理等标准内存管理手段， 在不产生太大开销的情况下解决过早释放内存的问题。我们开发了两种算法，本节将展示更简单的 sound_eager 算法的动机与实现。而下一节将介绍最优的算法 sound_lazy，该算法凝练了 Rémy 的算法的主要特点。
显然，在释放内存之前必须检查内存是否仍被使用。一个朴素的想法是：我们可以扫描所有已知且正在被使用的内存，找出所有对将被释放内存的引用。换言之，我们可以先进行一次完整垃圾收集的标记，然后观察候选对象是否被标记。但这样的检查似乎太昂贵了，应该等垃圾积累到一定程度后再大规模收集。遗憾的是，在 HM 类型系统中全称量化类型可能会在定义之后立刻被使用，不能随意推迟量化的时机。
更靠谱的方案是所有权追踪：将每个分配出来的资源与一个「资源所有者」相关联。所有者可以是对象，也可以是函数调用，只有资源的所有者能释放其拥有的资源。区域内存管理也是一种类似的技术：「区域」是由所谓 letregion 原语所创建，具有词法作用域的堆内存区域。当程序离开某 letregion 的作用域时，就会立即释放该原语分配的整片内存。
这一想法正合类型泛化的心意，在 HM 系统中，类型泛化始终与 let 关联：试想表达式 let x = e in e2，在推导 e 的类型时会分配一些类型变量，而 let 表达式自然就是这些类型变量的所有者。当我们找到 e 的类型后，就可以释放掉该 let 表达式所拥有的所有类型变量，即量化之。
上述直觉为健全且高效的泛化算法奠定了基础。本节的剩余部分将介绍第一个算法：sound_eager，它与上一节所展示的玩具 HM 类型推导器只有一些微小的细节不同，但这些细节至关重要。这里仅解释这些不同之处，完整代码请参阅附件。
sound_eager 与最开始的实现主要区别在于：每个自由类型变量（尽管可能是未绑定的）都有一个「所有者」，并指向了该所有者，「所有者」必定是 let 表达式，这些所有者被一个称为等级［level］的正整数标记——即所谓 de Bruijn 等级［de Bruijn level］或 「let 表达式的嵌套深度」。等级 1 代表（隐式）顶层的 let（顺带一提，尽管表达式 let x = e1 in eb1 和 let y = e2 in eb2 等级都为 2，但是它们之间不会互相混淆。两个 let 都不在对方的作用域内，因而互相独立）。let 嵌套深度等同于检查 let 表达式的函数递归深度，只需使用一个简单的可变计数器就很容易确定这些深度。
type level = int
let current_level = ref 1
let enter_level () = incr current_level
let leave_level () = decr current_level
类型推导函数会维护 let 的类型检查深度：
let rec typeof : env -> exp -> typ = fun env -> function
... (* 代码的其他分支同上 *)
| Let (x,e,e2) ->
enter_level ();
let ty_e = typeof env e in
leave_level ();
typeof ((x,gen ty_e)::env) e2
我们这里唯一修改的地方就是添加了 enter_level 和 leave_level 来追踪 let 等级。typeof 的其余部分与最初的玩具版本完全相同。
现在自由类型变量会带有其所有者的等级。新分配的类型变量默认赋予 current_level 等级，表示其所有者是正在进行检查的 let 表达式——在基于区域的内存管理中，所有新内存都分配在最内层的有效区域中。
type typ =
| TVar of tv ref (* 类型（模板）变量 *)
| QVar of qname (* 量化后的类型变量 *)
| TArrow of typ * typ
and tv = Unbound of string * level | Link of typ
let newvar : unit -> typ =
fun () -> TVar (ref (Unbound (gensym (),!current_level)))
正如同赋值可以改变某片已被分配的内存的所有者，统合也可能改变某自由变量的等级。举个例子：类型变量 ty_x（等级 1）与类型变量 ty_y（等级 2）都是自由变量，在 ty_x 与类型 TArrow(ty_y,ty_y) 进行统合后，对应的 TArrow 类型就会被导出到区域 1，因而 ty_y 的等级也会变为 1。读者可以将上面的例子中的统合视为：把 ty_x 所有出现的地方都替换成 TArrow(ty_y, ty_y)。
由于 t_x 的等级较小，可以出现在等级 2 的 let 之外的地方。那么在检查完等级 2 的 let 表达式的类型后，不应该释放 ty_y。只需适当更新 ty_y 的等级，就可以避免被错误释放。总之，在将自由变量 ty_x 与类型 t 统合后，必须将 t 中的每个自由变量 ty_y 的等级更新为 ty_y 与 ty_x 中较小的等级。
此外，将自由类型变量 ty_x 与类型 t 统合后，还需进行 occurs 检查避免引入循环——这也需要遍历类型，而这两次遍历可以合并成一次。新的 occurs 函数会一边执行检查一边更新等级：
let rec occurs : tv ref -> typ -> unit = fun tvr -> function
| TVar tvr' when tvr == tvr' -> failwith "occurs check"
| TVar ({contents = Unbound (name,l')} as tv) ->
let min_level =
(match !tvr with Unbound (_,l) -> min l l' | _ -> l') in
tv := Unbound (name,min_level)
| TVar {contents = Link ty} -> occurs tvr ty
| TArrow (t1,t2) -> occurs tvr t1; occurs tvr t2
| _ -> ()
只有模式匹配的第二个子句与原始 occurs 代码有所不同，统合代码本身根本毋须修改。最后，我们修改类型泛化程序，使其进行健全的泛化：
let rec gen : typ -> typ = function
| TVar {contents = Unbound (name,l)}
when l > !current_level -> QVar name
| TVar {contents = Link ty} -> gen ty
| TArrow (ty1,ty2) -> TArrow (gen ty1, gen ty2)
| ty -> ty
变化微乎其微，只是添加了 when l > !current_level 条件判断。回顾新的 typeof 代码：
let rec typeof : env -> exp -> typ = fun env -> function
... (* 其他分支不变 *)
| Let (x,e,e2) ->
enter_level ();
let ty_e = typeof env e in
leave_level ();
typeof ((x,gen ty_e)::env) e2
当检查器退出为类型检查而建立的区域 e 时，程序会调用 gen。这种情况下，仍属于上述区域的自由类型变量的等级比当前等级大。由于程序已经退出了该区域，那么任何此类类型变量都可以释放，即量化。
上面就是 sound_eager 对不健全的玩具推导程序所做的全部更改，这些更改修复了类型推导。这个在旧程序中有问题的示例
fun x -> let y = x in y
作图后显示没有问题了：
1 1 ty_x/1 = newvar () (* fun x -> ... *)
2 2 ty_e = (* let y = x in y *)
3 2 inst ty_x/1 (* x 推导为左侧类型，与 ty_x 相同 *)
2 1 ty_y = gen ty_e (* ty_x/1 仍自由，但其 *)
(* level = current，不得量化， *)
(* 不得丢弃 *)
1 1 TArrow(ty_x/1, inst ty_y) (* fun x -> ... 推导为左侧类型 *)
第一列数字代表 typeof 递归深度，或正在进行类型检查的 AST 节点的深度；第二列数字是 current_level，即 let 嵌套的深度。我们在斜线后标注自由类型变量的等级：如 ty_x/1。由于 ty_x/1 属于当前仍活跃的区域 1，因此在深度 2 执行的 gen 不会量化该变量。最终推倒出类型 'a->'a，符合预期。
再举一个稍复杂一点的例子，
fun x -> let y = fun z -> x in y
x 的类型变量 ty_x 分配在等级 1 处，而 ty_z 分配在等级 2 出。在内侧，即区域 2 的 let 结束后，ty_z/2 会被量化和处理，但是 ty_x/1 不会，因此推出的类型是 'a->'b->'a。这里鼓励读者自行绘制其他案例的图表，以检查推导出的类型是否合理。
这种等级跟踪技术看起来就像一种引用计数［reference counting］。不过，我们并没有记录自由类型变量被多少个用户所使用，而是只跟踪了一个，范围最广的用户。等级跟踪技术看起来也像一种分代垃圾回收［generational garbage collection］：新生代分配的内存会在（最年轻代的） minor GC 时回收，除非这块内存被调用栈引用，或者挂靠到了某个老生代对象上。分代垃圾回收器（像 OCaml 使用的 GC）的 minor GC 本身不会扫描老生代中是否存在对新生代内存的引用，因为默认不应该有这样的引用——除非有某些赋值指令把年轻代内存（的指针）赋值给老生代数据结构的字段。而是维护一个「把新生代挂靠到老生代」的赋值构成的列表，并在 minor GC 时把这些有挂靠的新生代内存升级成老生代。类型泛化事实上看起来与 minor GC 非常相似。
引用文献
加入了 sound_eager 泛化的玩具类型推导器完整代码，内附更多的现在能推理出健全类型的示例。
更高效的，基于等级的类型泛化
本节继续阐释 Rémy 算法背后的思想，并介绍 sound_lazy：上一节中 sound_eager 的优化版本。sound_lazy 算法避免了在统合、泛化以及实例化过程中重复且不必要地遍历类型。
为了继续优化，我们先要改变类型的语法。回顾 sound_eager 中，类型由自由的或被绑定的类型变量 TVar、（隐式全称）量化类型变量 QVar 以及函数类型 TArrow 组成。第一个看似无理的变化是：不再将 QVar 视为单独的选项，而是设定一个非常大，大到无法被正常访问的正整数 $ω$ 作为 generic_level，这样，等级与 generic_level 相同的 TVar 就被视为量化类型变量。
更重要的一点是，现在所有的类型都有等级，不仅仅是自由类型变量独有。复合类型（如 TArrow）的等级是其组成部分的等级的最大值，不需要特别精确。换言之，若某个类型属于活区域，那么它所有的组件都应该存活。若某（复合）类型不属于 generic_level，它就不可能包含任何量化变量，在实例化这样的类型时，只需原样返回即可，无需遍历；同理，若某类型的等级大于当前等级，那么它就可能包含可被泛化的自由类型变量。另一方面，类型泛化函数甚至不应该试图遍历那些等级小于等于当前等级的类型。这是第一点改进，说明了等级是如何帮助消除检查过程中对类型的过度遍历和重建，从而提升共享程度。
当统合类型与自由类型变量时，若后者的等级较小，那么应将类型的等级更新为类型变量的等级——对于复合类型，需要递归更新该类型所有组件的等级。为了推迟代价高昂的遍历，我们为复合类型赋予两个等级：level_old 代表类型组件的最大等级；level_new 小于等于 level_old，代表了更新之后的等级；若 level_new < level_old，表示该类型需要更新等级。sound_lezy 中类型的语法如下
type level = int
let generic_level = 100000000 (* 等同于 OCaml 的 typing/btype.ml *)
let marked_level = -1 (* 用于标记节点，检查循环 *)
type typ =
| TVar of tv ref
| TArrow of typ * typ * levels
and tv = Unbound of string * level | Link of typ
and levels = {mutable level_old : level; mutable level_new : level}
上面还没解释 marked_level：每次与自由类型变量进行统合时进行的 occurs 检查很昂贵，会提升统合与类型检查的算法复杂度，因此我们把这一检查延迟到整个表达式都被类型检查后再进行；但是，统合可能会在类型中产生循环，遍历类型必须先检查循环，否则就会有不停机的风险。
那么，我们在检查复合类型时先给复合类型的 level_new 临时赋值为 marked_level，表示该类型正在被遍历，而遍历过程中遇到 marked_level 则意味着检测到循环，应该报错。顺带一提，OCaml 中的类型往往带有循环：在检查对象［object］和多态变体类型［polymorphic variant type］的类型时，以及设置了 -rectypes 编译器选项时会出现递归类型或等递归［equi-recursive］类型。OCaml 类型检查器也使用了类似的技巧来检测循环从而避免不停机。
sound_lazy 的统合与 sound_eager 中的有若干重要区别：
let rec unify : typ -> typ -> unit = fun t1 t2 ->
if t1 == t2 then () (* t1 与 t2 是相同类型 *)
else match (repr t1,repr t2) with
| (TVar ({contents = Unbound (_,l1)} as tv1) as t1, (* 统合两个自由变量 *)
(TVar ({contents = Unbound (_,l2)} as tv2) as t2)) ->
if tv1 == tv2 then () (* 同一个变量 *)
else
if l1 > l2 then tv1 := Link t2 else tv2 := Link t1 (* 取两者中较高的等级 *)
| (TVar ({contents = Unbound (_,l)} as tv),t')
| (t',TVar ({contents = Unbound (_,l)} as tv)) ->
update_level l t';
tv := Link t'
| (TArrow (tyl1,tyl2,ll), TArrow (tyr1,tyr2,lr)) ->
if ll.level_new = marked_level || lr.level_new = marked_level then
failwith "cycle: occurs check";
let min_level = min ll.level_new lr.level_new in
ll.level_new <- marked_level; lr.level_new <- marked_level;
unify_lev min_level tyl1 tyr1;
unify_lev min_level tyl2 tyr2;
ll.level_new <- min_level; lr.level_new <- min_level
(* 其他情况都代表出现了统合错误 *)
and unify_lev l ty1 ty2 =
let ty1 = repr ty1 in
update_level l ty1;
unify ty1 ty2
其中的辅助函数 repr 与 OCaml 中的 Btype.repr 一样：它通过一路查询绑定类型变量构成的链接，最终返回自由类型变量或构造好的类型。与 OCaml 不同的一点在于我们执行了路径压缩。因为统合函数本身不再执行 occurs 检查，所以它必须尝试检测被意外创建的循环。现在对自由变量进行统合只需常数时间，
函数 update_level 是优化算法的关键部分之一，它「承诺」将类型的等级更新为给定等级。它只需消耗常数时间，并维持了算法中「类型等级只能降低」的不变性质。对于类型变量，update_level 会立刻更新其等级；而对于复合类型，若 level_new 较小，就将其设置为对应的新等级；此外，如果之前的 level_new 和 level_old 相同，update_level 还会将其放入 to_be_level_adjusted 队列，以便稍后更新其各个组成部分的等级。这个工作队列类似于分代垃圾收集器（如 OCaml 中的垃圾收集器）所维护的「把新生代挂靠到老生代」的赋值列表。
let update_level : level -> typ -> unit = fun l -> function
| TVar ({contents = Unbound (n,l')} as tvr) ->
assert (not (l' = generic_level));
if l < l' then
tvr := Unbound (n,l)
| TArrow (_,_,ls) as ty ->
assert (not (ls.level_new = generic_level));
if ls.level_new = marked_level then failwith "occurs check";
if l < ls.level_new then begin
if ls.level_new = ls.level_old then
to_be_level_adjusted := ty :: !to_be_level_adjusted;
ls.level_new <- l
end
| _ -> assert false
我们必须在泛化前更新这些待更新节点：毕竟，潜在的更新可能会降低某个类型变量的等级，将其提升到更广的区域，从而免于量化。然而，这里并非需要强制更新所有节点：只有那些 level_old > current_level 的类型才需要强制更新。若一个类型在当前点不包含可被泛化的变量时，等级更新可能会被进一步推迟。我们在附件代码的 force_delayed_adjustments 函数中实现了所描述的强制更新算法。顺带一提，如果必须真正更新复合类型（TArrow）的等级，那么就必须要遍历该类型。此外，统合两个 TArrow 的类型也需要遍历它们。因此，统合原则上也可以顺带更新等级。不过，我们还尚未实现这种优化。
类型泛化函数会搜索隶属于「已死亡」区域的自由 TVar 变量，将其等级设置为 generic_level， 从而量化该变量。该函数只遍历类型中可能包含需要泛化的类型变量的部分。若某个类型的等级（或其 level_new）小于等于 current_level，那么它所有的组件都属于存活区域，这个类型就没什么可泛化的；而泛化后，若某复合类型包含量化类型变量，它就会变为 generic_level。因此，对应的实例化函数将只查看等级为 generic_level 的类型。
let gen : typ -> unit = fun ty ->
force_delayed_adjustments ();
let rec loop ty =
match repr ty with
| TVar ({contents = Unbound (name,l)} as tvr)
when l > !current_level ->
tvr := Unbound (name,generic_level)
| TArrow (ty1,ty2,ls) when ls.level_new > !current_level ->
let ty1 = repr ty1 and ty2 = repr ty2 in
loop ty1; loop ty2;
let l = max (get_level ty1) (get_level ty2) in
ls.level_old <- l; ls.level_new <- l (* set the exact level upper bound *)
| _ -> ()
in loop ty
类型检查程序 typeof 保持不变，在对 let 表达式进行类型检查时会进入一个新区域，详情请查看源代码。
我们现在提出了一种优化过的 sound_lazy 类型泛化算法，它避免了在每次泛化时都需要扫描整个类型环境，还避免了每次在与自由类型变量统合时都进行 occurs 检查。因此，统合可以在常数时间内完成。该算法消除了不必要的类型遍历和复制，节省了时间和内存。除了为自由类型变量赋予类型等级外，优化还依赖于两个想法：首先是为复合类型指定等级，这样在无需查看其类型的前提就知道它可能包含的内容；其次是尽可能延迟昂贵的操作（类型遍历），希望它们将来能和其他操作一起完成。换言之，如果处理问题的时间拖得足够长，问题可能就会消失：拖延有时会有所帮助。
引用文献
优化后的玩具类型推导器的完整代码，同样附带了许多示例。
在 OCaml 中使用等级进行类型泛化
本节介绍了 OCaml 类型检查器内部是如何实现类型等级，并用其实现高效的类型泛化。下一节将介绍类型等级如何防止本地类型逃逸，以及如何检查存在量化类型。
前两节中，我们在 sound_eager 和 sound_lazy 中展示了 OCaml 类型检查器背后的关于类型泛化的思想。我们有意仿造 OCaml 检查器的代码来实现我们的教学算法，并经常使用相似的函数名。OCaml 类型检查器实现了 sound_eager 算法，并借用了 sound_lazy 算法中的一部分优化。
OCaml 比我们的玩具代码要复杂得多：玩具代码中的统合只需几行代码，而 OCaml 的 ctype.ml 中的统合代码则需要 1634 行。不过，理解玩具实现也应该有助于我们解密 OCaml 类型检查器。
通过观察 Ctype.unify_var 的代码可以发现：OCaml 类型检查器会在每次与自由变量统合时进行 occurs 检查和更新等级，这一点类似于 sound_eager 算法。而另一方面，OCaml 类型检查器为所有类型，而非只对类型变量分配等级，这一点又类似于 sound_lazy 算法 ——这么做的一个原因是为了检测逃逸出作用域的局部类型构造函数（下节中详细解释）。另一个和 sound_lazy 相同的点是，generic_level 区分了「量化后的类型变量」以及「可能包含量化类型变量的类型」（即所谓泛型［generic type］类型）。因此，负责实例化模板的函数 Ctype.instance 以及 Ctype.copy 就不会遍历和拷贝类型中不存在泛型的部分，而是将其原样返回，因此提升了类型变量之间的共享程度。为作区分，在 generic_level 等级中的类型变量打印为 'a，而其他等级的则打印为 '_a。
与我们的玩具实现中相同的一点是，OCaml 也使用可变的全局 Ctype.current_level 变量来追踪当前等级，并在创建类型或类型变量时，将该变量的值赋予新创建的对象（参见 Ctype.newty 及 Ctype.newvar）。调用 enter_def() 会递增 current_level，而 end_def() 则会递减之。除了 current_level 之外，还有用于检查 class 定义的 nongen_level，以及用于类型声明中的类型变量的 global_level。
我们简化 OCaml 中用于类型检查 let x = e 的主体的代码，并展示如下。
let e_typed =
enter_def ();
let r = type_check env e_source in
end_def ();
r
in
generalize e_typed.exp_type;
let new_env = bind env x e_typed.exp_type in
type_check new_env body_source
e_source 代表抽象语法树，即对于表达式 e 的 Parsetree.expression 类型的值；e_typed 则是 Typedtree.expression 类型值，表示每个节点都带有推断出的类型注释的（即 exp_type 字段）抽象语法树。
因此可以经常发现 OCaml 类型检查器中所有的类型泛化处都有类似的代码模式：
let ty =
enter_def ();
let r = ... let tv = newvar() in ... (... tv ...)
end_def ();
r in
generalize ty
如果算法发现在 end_def() 之后，tv 也没有和在 enter_def() 之前就已存在的类型变量进行统合，那么算法将泛化该变量。这段代码和我们的玩具实现中的代码非常相似。
有趣的是，等级还有另外一个用途：确保局部类型声明不能逃逸出其作用区域外。
类型区域
OCaml 类型检查器也利用类型等级来检查类型是否在其被声明之前就被使用，以及局部定义的类型是否逃逸到了更大的范围。
类型统合类似于「对可变变量赋值」，是滋生这两种错误的温床。我们已经看到了类型等级如何与基于区域的内存管理相关联。因此就不难理解为什么类型等级有助于控制统合过程，从而防止错误管理资源——这次与类型变量无关，而是与类型常量有关。
与 SML 不同的一点是，OCaml 支持通过 let module 形式定义局部模块。局部模块内可以定义类型，甚至可以让它所定义的类型逃逸出模块。举个例子
let y =
let module M = struct
type t = Foo
let x = Foo
end
in M.x
(* ^^^
Error: This expression has type M.t but an expression was expected of type 'a
The type constructor M.t would escape its scope *)
如果编译器不对这种类型逃逸报错，y 就会被赋予 M.t 类型，但其作用域里根本没有模块 M。这个问题类似于在 C 语言的函数中返回其局部变量的地址。
char * esc_res(void)
{
char str [] = "local string";
return str;
}
局部定义的类型不但可以通过返回值类型逃逸，还可以通过与已有的类型变量进行统合从而逃逸
fun y ->
let module M = struct
type t = Foo
let r = y Foo
end
in ()
(* ^^^
Error: This expression has type t but an expression was expected of type 'a
The type constructor t would escape its scope *)
C 程序员对这种错误同样很熟悉：
char * y = (char*)0;
void esc_ext(void)
{
char str [] = "local string";
y = str;
}
即便是在顶层定义的模块也可能存在这种类型逃逸问题。下面是一个引自 OCaml 类型检查器源码注释中的例子：
let x = ref []
module M = struct
type t
let _ = (x : t list ref)
end
变量 x 的类型 '_a list ref 不是泛型。模块 M 定义了局部类型 t。导致了在 t 之前定义的 x 获得了类型 x : t list ref，即 t 在被定义之前就被使用到了。这种类型逃逸甚至在没有模块时也会发生，Jacques Garrigue 展示了一个例子：
let r = ref []
type t = Foo
let () = r := [Foo]
(* ^^^
Error: This expression has type t but an expression was expected of type 'weak1
The type constructor t would escape its scope *)
OCaml 不能容忍代码出现这种类型逃逸。在任何情况下，类型构造函数都不能在其声明的作用域之外使用。而类型等级则对类型构造函数进行了区域化管理。
为了实现类型泛化，OCaml 类型检查器已经有了「区域」这种设施：其中包含开启/进入新区域的 begin_def 以及销毁/退出区域的 end_def，以及把类型关联到其所有者的区域，并在统合过程中跟踪所有权的变化。那么剩下的工作就是把类型声明放入一个全新的区域，并将所声明的类型构造函数与这里区域关联起来。任何包含了这一类型构造函数的类型都必须在类型声明的区域内：类型构造函数的声明侧必须支配它的所有使用侧。
如前所述，类型区域是由一个正整数来标识的，即类型等级，它代表了区域的嵌套深度。每个类型有个一个 level 字段，表示其所有者的区域等级。类型构造函数也需要类似的等级注释——事实证明，OCaml 中的另一种工具恰好可以实现这一目的。
在 OCaml 程序中，无论是类型构造函数、数据构造函数、项变量都可以被重新定义：类型可以重新声明，变量可以被多次重新绑定。OCaml 依赖标识符［identifier］来区分统一名称的不同声明或绑定情况（参见 ident.ml）。标识符包含了名称和时间戳；其中时间戳是一个正整数，有一个全局可变的 Ident.currentstamp 变量保存了「当前时间」，每次程序通过声明或绑定创建新标识符时，就会递增这个变量；因此，标识符上的时间戳就是其绑定时间。
「绑定时间」是把标识符和类型区域相关联的一种自然方式：若把 currentstamp 设置为 current_level，那么新创建的标识符的时间戳必定大于等于 current_level——它们将被视为当前类型区域中的标识符。因此，若某类型的等级大于等于该类型中所有类型构造函数的绑定时间，就说明该类型没有逃逸。
统合，特别是与自由类型变量的统合——类似于赋值，可能会改变类型的所有权，因此必须相应地更新类型等级。与此同时，统合还可以检查上述的逃逸判据是否生效：参见 Ctype.update_level。
现在我们可以理解 OCaml 是如何对形如 let module name = modl in body 的局部模块表达式类型检查的了，下列代码摘自 typecore.ml
| Pexp_letmodule(name, smodl, sbody) ->
let ty = newvar() in
(* 记住当前等级 *)
begin_def ();
Ident.set_current_time ty.level;
let context = Typetexp.narrow () in
let modl = !type_module env smodl in
let (id, new_env) = Env.enter_module name.txt modl.mod_type env in
Ctype.init_def(Ident.current_time());
Typetexp.widen context;
let body = type_expect new_env sbody ty_expected in
(* 返回原始等级 *)
end_def ();
(* 检查 modl 中定义的局部类型是否通过 body 的返回类型逃逸 *)
begin try
Ctype.unify_var new_env ty body.exp_type
with Unify _ ->
raise(Error(loc, Scoping_let_module(name.txt, body.exp_type)))
end;
re {
exp_desc = Texp_letmodule(id, name, modl, body);
exp_loc = loc; exp_extra = [];
exp_type = ty;
exp_env = env }
代码先创建了一个类型变量 ty，用于接受表达式被推导出来的类型，这一变量是在当前区域创建的。之后，代码调用 begin_def() 进入新类型区域，然后把标识符时间戳时钟设置为与新的 current_level 对应（时间戳时钟会在创建标识符之前先递增一次，这就是为何 Ident.set_current_type 以 ty.level 为参数，而不以递增后的 current_level 为参数）。因此，任何局部模块中定义的类型构造函数的绑定时间戳都将大于等于 current_level。
Ctype.init_def(Ident.current_time()) 将类型等级设置为局部模块中最后一个标识符的时间戳。因此，在检查 body 的类型时创建的所有新类型的等级都将大于或等于任意局部模块内定义的类型构造函数的绑定时间戳。统合应当避免任何等级更新破坏这一不变性质。最后，在 ty 的最末端（其区域在 let module 的区域之外）进行统合确保了局部的类型构造函数不会通过返回值类型逃逸出区域。
顺带一提，上述代码中的 Typetexp.narrow () 和 Typetexp.widen context 为局部模块中的类型变量建立了新的上下文，这就是为何下列表达式
fun (x:'a) -> let module M = struct let g (x:'a) = x end in M.g
推导出来的类型是 'a -> 'b -> 'b 而非 'a -> 'a -> 'a。上述代码中出现的两个 'a 是不同的类型变量——局部模块不与周围的模块共享任何类型变量。
存在量化类型［existential type］实际类似于「在局部模块中声明的类型」：事实上，存在量化类型可以用头等模块实现。检查通过「模式匹配」（或用模块的术语，「打开」）某个存在量化类型所产生的类型，和检查模块的类型使用的是相同的技术：具体请参阅 Typecore.type_cases。
「等级」的发明史
Didier Rémy 的博士研究方向是关于记录［record］类型和变体［variant］类型推导的，他在攻读博士学位时发明了我们上面所展示的，基于等级的类型泛化算法（顺带一提，他将「等级」这一概念称为阶［rank］，遗憾的是现在 OCaml 类型检查器中却使用了「等级」作为核心术语）。Didier Rémy 最初在 Caml（Categorical Abstract Machine Language）中实现了记录类型推导的原型。Caml 用 Caml 自举实现，运行于 Le Lisp 语言上。这一实现的历史比 Caml Light 更为久远，遑论 OCaml 了。Didier Rémy 需要频繁重新编译 Caml，但每次编译都会花费很多时间。正如他所说，Caml 的类型推理正是速度的瓶颈所在：
The heart of the compiler code were two mutually recursive functions for compiling expressions and patterns, a few hundred lines of code together, but taking around 20 minutes to type check! This file alone was taking an abnormal proportion of the bootstrap cycle. This was at the time when recompiling fonts in $ \mathrm{\LaTeX} $ would also take forever, so I think we were used to scheduling such heavy tasks before coffee breaks – or the other way round.
译：编译器代码的核心部分是两个互相递归的函数，用于编译表达式和模式。它们加起来总共就 100 多行，但检查它们的类型却要花费近 20 分钟！仅这个文件就占用了自举周期的很大一部分时间。那时，重新编译 $ \mathrm{\LaTeX} $ 中的字体也会花费很长时间，因此我们倾向于把这些耗时的工作放在喝咖啡休息之前或之后。
Caml 中类型推导缓慢的原因有几个：
实例化类型模板时，检查器会创建整个类型的副本——即便是那些没有量化类型变量，可以在不同类型变量间共享的部分都被拷贝了。
每次统合自由类型变量时都会检查该变量是否（就像我们上面展示的玩具级检查器一样）
每次类型泛化都会扫描整个类型环境，从而提升类型推导的时间复杂度。
Didier Rémy 决心加速这一过程。他说道：
因此，当我编写记录类型和变体类型的类型检查器原型时（由于记录和变体是结构性的，往往比普通的 ML 类型大得多），我需要非常小心，尽可能让算法实现贴近其理论复杂度。 - 我的图统合算法时间复杂度是 $O\left(n \log n\right)$——通过路径压缩并延迟
occurs检查。- 我尽可能保持构造类型时引入的类型共享，没有在泛化/实例化的过程中打破这些共享。- 最后，我引入了基于等级的类型泛化。
Rémy 在他的博士论文（法文）和 1992 年的一次技术报告中介绍了他提出的高效类型推导算法。之前的 sound_eager 是 Rémy 算法的一个非常简单的模型，展示了该算法的主要特点。Xavier Leroy 在 Caml Light 中实现了类型等级和基于等级的类型泛化，不过，由于种种原因，他的实现类似于 sound_eager。
Didier Rémy 本人更倾向于从图的角度来看待所谓「等级」或「阶」的概念。如果我们在 AST 的每个节点上添加类型注释，然后将共享同一个类型变量的节点连接在一起，将被量化的变量与量化节点连接在一起，我们就得到了一张图。自由类型变量的等级可视为其 de Bruijn 等级，可以视为一种指向「将要量化这一变量的 AST 节点」的指针。在 HM 系统中，AST 节点必须是 let 节点。统合两个自由变量会把他们连接在一起，因此需要调整他们的等级，以保证量词节点
事实证明，这种把类型等级看作图的视角卓有成效。基于等级的类型泛化很容易扩展到支持字段多态［row polymorphism］记录类型的系统中。这一视角最终促使 Didier Rémy 发明了 MLꟳ 系统，他说：
The main operation in MLꟳ – raising binders – is analogous to the computation of minimal rank between two nodes.
译：MLꟳ 系统的主要操作「提升绑定」——可以类比于计算两个节点的最小阶数。
下面引用的 Rémy 的两个关于 MLꟳ 的演讲描述了该系统，并用一些小动画展示了类型检查过程中如何调整节点的阶。在 «The Essence of ML Type Inference» 中，他还解释了「阶」这一概念如何适用于基于约束求解的 ML 类型推导算法。
引用文献
«The first implementation» 一节中介绍了最初的 Caml 实现。
François Pottier and Didier R�my. The Essence of ML Type Inference
Didier Rémy: Extension of ML Type System with a Sorted Equational Theory on Types
出自 Research Report 1766, Institut National de Recherche en Informatique et Automatique, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992。
- Didier Rémy: A new look on MLF
http://cristal.inria.fr/~remy/mlf/portland.pdf
- Didier Rémy: MLF for Everyone (Users, Implementers, and Designers)
http://cristal.inria.fr/~remy/mlf/mlf-for-everyone.pdf
- David McAllester: A logical algorithm for ML type inference
David McAllester 后来重新发现了这种高效的泛化方法。他还证明：对于大多数实用程序，ML 的类型推导与程序大小几乎呈线性关系。出自 Proc. RTA'03, pp. 436-451。
这篇论文比较了两种基于等级的 HM 推导算法：一种使用 let 等级（如本页），另一种则依赖于 lambda 等级。论文为这两种算法开发了抽象机器，并描述了它们几个有趣的形式化性质。SML/NJ 中使用了 lambda 等级方法。
该文的第 6 章（参见其中的幻灯片和示例）介绍了 Rémy 算法的一种简化版本——本质上就是 sound_eager。出自 Springer Undergraduate Texts in Computer Science. xiv + 278 pages. July 2012。
创建全新类型变量
OCaml 类型检查器提供了两种创建全新类型变量的函数，本节将说明这两个函数之间的区别。这两个函数都定义在 ctype.ml 文件中，其签名如下
newvar : ?name:string -> unit -> type_exp
newgenvar : ?name:string -> unit -> type_exp
两个函数都接受一个可选参数 ?name，如果用户提供了这一参数，就用它来为变量命名，否则自动选择名称。
newvar 会创建一个等级等同于 current_level 的变量，而 newgenvar 则创建一个 generic_level 等级的变量。在下列代码中
let ty1 = newvar () in
unify env ty1 some_type
let ty2 = newgenvar () in
unify env ty2 some_type
变量 ty1 和 ty2 的行为完全相同：类型变量将绑定到 some_type。由于 current_level 对应于最内层的存活区域，some_type 的等级将小于等于当前等级，因此在两种情况下都不会改变。
两者的差异主要体现在下列两个片段中（第二个片段经常出现在 typecore.ml）
let ty1 = newvar () in
let list_type = newgenty (Tconstr(p_list, [ty1])) in
let texp = instance env list_type in
unify env texp some_type
let ty2 = newgenvar () in
let list_type = newgenty (Tconstr(p_list, [ty2])) in
let texp = instance env list_type in
unify env texp some_type
当且仅当类型是泛型时，instance 函数会复制类型（准确的说，是创建一个 Tsubst 类型的节点）。这意味着，在
let ty = newvar () in instance env ty
中，instance 等同于 identity 函数。然而，在
let ty = newgenvar () in instance env ty
中，instance 会复制变量。
因此，上面的第一段代码中，末尾的 unify 可以通过实例化 ty1 来影响 list_type；而在第二段代码中，list_type 不可能会被影响，因为 unify 将作用于 ty2 的副本。
类型泛化的真实复杂性
OCaml 编译器中所执行的 let 泛化远比我们上面所介绍的复杂得多。本节旨在帮助读者了解类型泛化的真实复杂性。
OCaml 的 let 表达式有如下一般形式
let [rec] pattern = exp and pattern = exp ... in body
let 的类型检查函数 type_let 占了文件 typecore.ml 中的 160 行——如果加上检查 let 绑定 pattern 的代码以及递归标志的情况下会更多。下面展示该段代码的结尾部分。
begin_def ();
...
let exp_list =
List.map2
(fun (spat, sexp) (pat, slot) -> .... (* type checking of expressions *)
type_expect exp_env sexp pat.pat_type)
spat_sexp_list pat_slot_list in
...
end_def();
List.iter2
(fun pat exp ->
if not (is_nonexpansive exp) then
iter_pattern (fun pat -> generalize_expansive env pat.pat_type) pat)
pat_list exp_list;
List.iter
(fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
pat_list;
(List.combine pat_list exp_list, new_env, unpacks)
从中可以发现一些眼熟的编码模式：
begin_def(); ... newvar () ... end_def(); generalize
然而 generalize_expansive 中却有着另一段遍历类型结构的代码：只有表达可扩展，即可能产生可被观察到的副作用时才会调用这一段代码。函数 Ctype.generalize_expansive 将会遍历其参数 type_expression：当遇到一个构造好的类型 Tconstr(p,args)（如 list 类型等等），generalize_expansive 将检查类型 p 的声明对于其参数是否协变［covariance］。若 arg 协变，那 generalize_expansive 将遍历 arg，将等级大于 current_level 的组件等级设置为 generic_level；若 arg 非协变（如 ref 和 array 类型构造函数的参数），arg 中等级高于 current_level 的组件将被重置为 current_level，随后的 generalize 将保持这些等级不变 。这就是所谓放松的值限制［relaxed value restriction］的实现原理，有了该技术，就可以为下列表达式推导出多态类型
# let x (fun y -> print_string "ok"; y) [];;
ok
val x : 'a list = []
在上面的表达式中，x 被绑定到了一个不是语法上的值的结构（函数应用），因而可扩展，求值该表达式也会产生可被观察到的副作用。但由于 list 类型对于其参数协变，所以我们还是可以泛化 x。SML 则不会这么做。
引用资料
- Jacques Garrigue: Relaxing the Value Restriction
出自 FLOPS 2004, pp. 196-213。