[译]通过例子学子类型推理（十一）：值限制和多态递归
在上一篇中，我们介绍了let 多态的一个非常基本的实现，它允许 let-bound 函数在每个调用点以不同的类型被调用。遗憾的是，它与可变结合起来还不健全。今天，我们将看到如何使用值限制来修复不健全性。
值限制
回顾下面的例子，它错误地通过了类型检查器并在运行时崩溃。
let p = ref (fun x -> x);
(* 42 是可调用的函数，对吧？ *)
p := 42;
!p "arg"
An error occurred during evaluation in the repl: TypeError: $.v0.$p is not a function
问题在于，在类型检查器中，每当变量被引用时，我们都会把 let 表达式当作重复主体，但在编译后的代码中只输出一个副本。这对不可变的代码有效，但对包含引用的代码无效，因为底层代码创建了单一引用，被该变量的所有使用共享。为了解决这个问题，我们需要确保引用类型总是共享，而不是重复的。
让事情变得更加复杂的是，总是强制引用是单态的是不可取的。考虑下面的例子。
let id = fun x ->
let temp = ref x in
!temp;
(id 1) + 3;
(id "x") ^ "y";
引用的使用是新 id 函数的实现细节，我们不希望它妨碍 id 的多态性。事实上，在这种情况下，让 id 多态是安全的，因为对 id 函数的每次调用都会在运行时生成新引用，所以 id 1 和 id "x" 的调用根本没有共享可变状态。
为了解决这个问题，SML 引入了值限制。这基本上说明，只有当 let-bound 变量定义中的所有引用和函数调用都出现在函数定义内部时，才应该使其多态化。
在值限制之前，SML 使用了一个复杂得多的系统，试图跟踪哪些函数可能包含可变状态。然而，这很复杂，而且容易出错，并导致不理想的限制，如上所示。值限制基本上是举起手来，假设任何函数都有可能泄露可变状态，而限制函数调用。
基本上，任何引用的“裸露”使用（或函数调用，在这个系统中被认为等同于引用）都会强制单态化。然而，如果这些引用或函数调用通过出现在函数定义内部而受到“保护”，那么使该函数多态化是可以的，因为每当调用该函数时，该函数的主体都会被重新执行，并根据适用情况创建新引用。
实现值限制
现在，我们不会费心去实现完全的值限制，因为这需要编写一套新的 AST 遍历代码来递归检查引用和函数调用的存在。相反，我们将采用保守的近似方法，只对右边是函数定义的 let 变量直接进行泛化，用 5% 的努力实现 let 多态 95% 的用例。
fn check_let(engine: &mut TypeCheckerCore, bindings: &mut Bindings, expr: &ast::Expr) -> Result<Scheme> {
if let ast::Expr::FuncDef(..) = expr {
// Right hand side is a function definition - ok to make it polymorphic
let saved_bindings = RefCell::new(Bindings {
m: bindings.m.clone(),
changes: Vec::new(),
});
let saved_expr = expr.clone();
let f: Rc<dyn Fn(&mut TypeCheckerCore) -> Result<Value>> =
Rc::new(move |engine| check_expr(engine, &mut saved_bindings.borrow_mut(), &saved_expr));
f(engine)?;
Ok(Scheme::Poly(f))
} else {
// Right hand side is something other than a function definition
// treat it monomorphically for now.
// TODO - implement the recursive value restriction checks
let var_type = check_expr(engine, bindings, expr)?;
Ok(Scheme::Mono(var_type))
}
}
在新 check_let 函数中，我们检查 expr 是否是 FuncDef。如果是，就像以前一样返回多态类型方案。否则，我们只是急切地对主体进行类型检查，并返回单态类型。
前面的不健全例子现在在编译时导致了类型错误，正如预期的那样。
TypeError: Value is required to be a function here,
(* 42 是可调用的函数，对吧？ *)
p := 42;
!p "arg"
^~
But that value may be a integer originating here.
let p = ref (fun x -> x);
(* 42 是可调用的函数，对吧？ *)
p := 42;
^~
!p "arg"
多态递归
现在我们已经解决了常规 let 表达式的问题，现在是时候为 let rec 添加多态了。回想一下，我们对 let rec 定义进行类型检查的方式是创建一个类型变量，将其添加到环境中，用该环境对定义的右侧进行类型检查，然后从该结果中向原始变量添加流约束。
使用临时类型变量似乎可以防止我们推导出 let rec 表达式的多态方案。事实上，let rec-bound 变量在其自身定义的范围内确实必须是单态的。
let rec id = fun x ->
(* id 在这里需要时单态的 *)
let _ = (id 1) + 3 in
(* 所以这导致了类型错误 *)
let _ = (id "x") ^ "y" in
x;
例如，上面的代码使用 let rec 定义了普通的恒等函数 id，只是 id 函数也用不同的类型调用自己。由于 id 只是在求值定义时被设置为（单态）类型变量，这必然会导致类型错误。
TypeError: Value is required to be a string here,
let _ = (id 1) + 3 in
(* 所以这导致了类型错误 *)
let _ = (id "x") ^ "y" in
^~~~~~~~
x;
But that value may be a integer originating here.
let rec id = fun x ->
(* id 在这里需要时单态的 *)
let _ = (id 1) + 3 in
^
(* 所以这导致了类型错误 *)
let _ = (id "x") ^ "y" in
这不仅是我们所使用的算法的产物，而是基本限制。允许多态递归，即允许递归函数用不同的类型调用自己，这使得类型推导无法确定，无论使用什么算法。
然而，并没有这样的问题阻止我们在其定义之外为 let rec-bound 变量推导一个方案。例如，考虑以下愚蠢的递归 id 的实现。
let rec id =
fun x ->
if true then
x
else
(* id 在这里是单态的 *)
id(x);
(* 但在这里让 id 多态是安全的
现在我们已经完成了对其定义的类型检查 *)
(id 1) + 3;
(id "x") ^ "y";
上述函数基本上等同于普通的、非递归的 id 实现，所以如果我们也能多态地使用它就更好了。幸运的是，可以。诀窍是，一旦对递归定义进行了求值，我们就把它变成多态方案，并替换绑定，把它从单态的临时变量变为结果的多态方案。这样，递归定义之外的任何代码都可以多态地使用它。
fn check_let_rec_defs(
engine: &mut TypeCheckerCore,
bindings: &mut Bindings,
defs: &Vec<(String, Box<ast::Expr>)>,
) -> Result<()> {
let saved_bindings = RefCell::new(Bindings {
m: bindings.m.clone(),
changes: Vec::new(),
});
let saved_defs = defs.clone();
let f: Rc<dyn Fn(&mut TypeCheckerCore, usize) -> Result<Value>> = Rc::new(move |engine, i| {
saved_bindings.borrow_mut().in_child_scope(|bindings| {
let mut temp_vars = Vec::with_capacity(saved_defs.len());
for (name, _) in &saved_defs {
let (temp_type, temp_bound) = engine.var();
bindings.insert(name.clone(), temp_type);
temp_vars.push((temp_type, temp_bound));
}
for ((_, expr), (_, bound)) in saved_defs.iter().zip(&temp_vars) {
let var_type = check_expr(engine, bindings, expr)?;
engine.flow(var_type, *bound)?;
}
Ok(temp_vars[i].0)
})
});
f(engine, 0)?;
for (i, (name, _)) in defs.iter().enumerate() {
let f = f.clone();
let scheme = Scheme::Poly(Rc::new(move |engine| f(engine, i)));
bindings.insert_scheme(name.clone(), scheme);
}
Ok(())
}
像往常一样，由于需要潜在地处理多个相互递归的定义，多态 let rec 的实际实现复杂得可怕。从好的方面看，在这种情况下，我们不必担心值限制，因为在语言语法级别上，之前定义的 let rec 上只允许在右边定义函数。如果你决定放宽这个限制，你需要在这里加回检查。
放宽的值限制
事实证明，原来的值限制在 OCaml 中过于繁琐，所以 OCaml 实际上使用了一个稍加修改的变体，叫做放宽的值限制，它接受的程序比经典的值限制更多，同时还能保持合理性。
然而，事实证明，放宽的值限制基本上只是一个弥补 OCaml 缺乏子类型的 hack。问题源于实际上有些值在有子类型的情况下自然可以被赋予单态类型，但在没有子类型的情况下却需要多态来表达。
例如，考虑一个通用的不可变列表类型 List[T] 的情况。由于列表是不可变的，所以 T 是协变的，而不是不变的，如四周前的帖子所述。问题是，空不可变列表的类型是什么？
空列表应该可以在任何地方使用，包括字符串列表，整型列表，或任何其他类型的列表。使用子类型化，答案很简单。空列表只是拥有有类型 List[Bot]，其中 Bot 是底类型，所有其他类型的子类型。由于协变，这意味着如期望的那样，List[Bot] 对于所有 T 来说都是 List[T] 的子类型，不需要多态。
然而，如果没有子类型化，这是不可能的。你必须为 T 选择特定值。给空列表的类型为 List[int]，它不能与字符串列表混合，反之亦然。因此，没有子类型化，单态类型对于空列表是没有意义的。相反，你必须给它多态类型方案 forall T => List[T]。
遗憾是，这与值限制相结合，使得无法从函数中有用地返回空列表。因此，OCaml 增加了放宽的值限制，它声明，如果产生类型方案的每个类型参数只出现在协变或逆变位置，而不是两者都出现，那么值限制原本禁止其成为多态的表达式仍然可以变成多态。
然而，这只是可以用子类型化进行单态类型化的类型集合! 纯协变的类型参数可以像上面一样只分配 Bot，而纯逆变的类型参数可以分配 Top，所有类型的超类型。子类型化给我们提供了放宽的值限制，免费。
性能
我们的 let 多态的懒惰实现是非常低效的，因为每次变量被引用时都会递归地重新运行类型检查器。自然，从最坏情况下的运行时复杂度来看，它也是可能最好的。(╯°□°)╯︵ ┻━┻
计算复杂性的铁律
我喜欢称之为“计算复杂度的铁律”，这是一个有点不直观的观察，即一个算法越强大，它一定越慢，至少在最坏的情况下是这样。假设你在研究某个新问题 FOO，发现 SAT（布尔可满足性，一个出了名的难问题）可以简化为 FOO，这意味着解决 FOO 的算法也可以让你解决 SAT。外行可能会觉得“好消息!只要我们解决了 FOO，也就能解决 SAT 了。这肯定是解决 SAT 路上的一大突破!"而复杂度理论家则会叹息，认为 "Welp，我想也没有希望解决 FOO 了。"
事实证明，光靠增加额外的间接层是吓唬不了数学的。一个算法在最坏的情况下，至少和它能解决的最难问题所需的时间一样慢。在类型推导的情况下，这意味着类型系统精度（即功率）的每一次提高都是有代价的。
程序员喜欢强大的类型系统，因为这可以让他们检查代码中更复杂的不变量，但正是这种能力使得类型推理变得更慢。在子类型化的情况下，子类型化所增加的能力意味着从近乎线性时间的类型推理变成了最坏情况下需要立方时间的类型推理（在看似可信的硬性假设下）。从这个角度来看，let 多态确实付出了非常高的代价。let 多态的类型推理需要指数级的时间。
指数级放大
要看到这一点，考虑下面的代码模式。
let f = fun x -> x;
let f2 = fun x -> f (f x);
let f3 = fun x -> f2 (f2 x);
let f4 = fun x -> f3 (f3 x);
let f5 = fun x -> f4 (f4 x);
f2 调用 f 两次，因此复制 f 类型两次。f3 调用 f2 两次，因此复制 f2 两次，这意味着复制 f 四次。然后 f4 将其复制八次，等等，导致指数级爆炸。
你可能会想，这是否仅仅是目前算法的一个弱点，可以通过充分巧妙的记忆等方式来解决。在上面的玩具例子中，当然可以，因为所有的 f 函数只是简化为 fun x -> x。但在一般情况下，答案是否定的。
在上面的例子中，f 只是恒等函数，但无论 f 是哪个函数，这个例子都是一样的。如果把 f 换成任意函数，f2 仍然会在其参数上调用 f 两次。那么 f3 调用 f2 两次，相当于调用 f 四次，以此类推。let 多态允许简洁地表达对任意函数的指数级调用次数，每次调用的类型不同。这种简洁性既是它的优点，也是它的致命缺陷。
特别是，可以写一个函数 f，在类型层面模拟任意图灵机的单独步骤，其中机器的旧的和新的状态被编码在函数的输入和输出类型中。多次调用 f 多态地模拟图灵机的多个步骤，所以嵌套的多态 fn 函数的类型检查需要在编译时模拟任意图灵机的 2^n 步骤。由于机器的状态被编码在输出类型中，你可以根据任意图灵机是否在最多 2^n 步中停止，编写类型检查或产生类型错误的代码。因此，在最坏的情况下，无论你的算法多么聪明，都不可能做到比指数时间更好。
顺便说一下，多态递归允许你用每次调用的不同类型来表达对给定函数的无限次调用，这意味着有限的代码量可以要求在编译时模拟图灵机的无限步。这有助于解释为什么多态递归使得类型推理无法确定。
优化
在这个系列中，我刻意避免做任何优化，除非有必要提高最坏情况下的复杂度。主要原因是为了让代码尽可能简单，更容易理解。然而，另一个原因是，最坏情况复杂度是一个客观的衡量标准，而“真实世界性能”是可变的，高度依赖于基准。通常情况下，特定的改变是否会使编译器在实践中变得更快或更慢，完全取决于你在实践中把它用在什么样的代码上。由于缺乏现有的带有子类型的语言，这一点尤其成问题，因为这意味着缺乏用子类型编写的真实世界代码，这使得很难测试和剖析不同的编译器设计。
话虽如此，如果你想在真实语言中使用它，优化 let 多态的实现是相当重要的，所以我想我至少要总结一下编译器用来让它“在实践中快”的技术。
最重要的一步是避免每当类型方案实例化时重新运行整个类型检查逻辑。相反，只需运行一次以产生类型图，然后每当方案实例化时，使用新鲜的类型变量复制该图。为了确保合理性，一旦遇到在 let 定义范围外定义的图的部分，一定要停止复制。为了进一步加快速度，你可以将复制限制在两个“端点”都还可达的变量上，并首先应用所有常用的简化技术来减少被复制图的大小。
结论
有了 let 多态，我们现在已经实现了 ML 风格类型推理的所有“基本”功能。下周，我们将添加更多的独特功能，比如流式类型和混合比较运算符。