[译]通过例子学子类型推理(十):Let 多态
上周,我们为 cubiml 添加了不完全匹配和记录扩展。今天我们处理 let 多态。
Let 多态
到目前为止,类型系统中的所有东西都是单态的,这意味着每个表达式都推导出单一类型。然而,在某些情况下,这是不适当的限制。考虑以下代码示例
let id = fun x -> x;
(id 1) + 3;
(id "x") ^ "y";
目前,这导致了类型错误,因为 id
被迫是单态的,给它推断的类型是 (int & string) -> (int | string)
。本质上,单态意味着编译器认为来自任何函数调用的参数都有可能流向每个函数调用的结果。因此,如果我们用整型调用函数,后来又用字符串,它们就会在函数类型中混在一起,导致错误。
为了使上述代码通过类型检查,我们需要在类型检查器中加入上下文敏感,使编译器对同一函数的不同调用保持分离,并理解只有特定调用的参数可能流向该特定调用的结果。
Hindley-Milner 系统通过一个称为 let 多态的特性来处理这个问题。基本上,当推断 let 绑定变量的类型时(即 let v = e1 in e2
),我们不是为 v
推断单一单态类型,而是推断类型方案。
类型方案
类型方案基本上是一个模板,可以用来根据需求标记新的类型。对于 let 绑定变量,我们在类型环境中存储类型方案,而不是单一类型。每当变量被引用时,方案就会被用来标记一个新类型,这个新类型是针对变量的特定用法的。
在上面的代码示例中,如果没有 let 多态,id
将具有推导类型 T -> T
。在这种情况下,T
是单类型变量,这意味着 id
的每一次使用都必须共享 T
的相同的值,从而导致上述错误。通过 let 多态,我们可以推导出类型方案 forall T => (T -> T)
。这就是说,每当引用 id
时,我们就创建新类型变量,然后返回类型 T -> T
,其中 T
是新创建的变量。这意味着,对 id
的不同使用将有不同的类型变量 T
,根本不会相互影响,意味着一个可以用 int
代替,另一个可以用 string
代替,而不会造成任何虚假的类型错误。
懒惰 let 多态
实现 let 多态的方法有很多,但现在,我们只选择最简单、最懒惰的合适实现,以使事情更容易理解,即使它比更优实现慢。
回想一下,前面代码例子中的问题是,我们希望每次引用时,都能用不同的类型重用(let 绑定)id
函数。如果没有多态性,我们仍然可以解决这个问题,只要在每次引用函数时重复该函数的代码即可。例如,如果将上面的代码重写如下,即使没有 let 多态,它也会通过类型检查。
let id = fun x -> x
in (id 1) + 3;
let id = fun x -> x
in (id "x") ^ "y";
基本上,let 多态的目标是能够编写一个函数,并让类型检查器在每次引用它进行类型检查时都把它当作是重复的,但在运行时仍然只有一个函数的实际副本。最简单的方法是每当类型方案被实例化时,在定义的代码上重新运行类型检查器(后面我们将介绍一些注意事项)。
实现
之前,我们在前端的类型环境中存储了普通类型(变量名与之前推导类型的映射)。因此,开始时,我们需要修改它来存储类型方案。
#[derive(Clone)]
enum Scheme {
Mono(Value),
Poly(Rc<dyn Fn(&mut TypeCheckerCore) -> Result<Value>>),
}
struct Bindings {
m: HashMap<String, Scheme>,
changes: Vec<(String, Option<Scheme>)>,
}
之前,绑定存储的是 String -> Value
映射。我们定义了新枚举 Scheme
,并将其改为 String -> Scheme
映射。注意,这里的术语与上面略有不同。Scheme
枚举可以存储普通单态类型(用于函数参数和递归变量)或多态类型方案(用于 let 绑定变量)。
Poly(Rc<dyn Fn(&mut TypeCheckerCore) -> Result<Value>>),
在后一种情况下,枚举存储了闭包对象,它可以被调用来根据需求标记新类型。它接收对类型检查核心的引用,使用它来创建任何适用的新类型变量,并返回新单态类型。
接下来,我们要更新 AST 中处理 Variable
节点的代码。
Variable((name, span)) => {
if let Some(scheme) = bindings.get(name.as_str()) {
match scheme {
Scheme::Mono(v) => Ok(*v),
Scheme::Poly(cb) => cb(engine),
}
} else {
Err(SyntaxError::new1(format!("SyntaxError: Undefined variable {}", name), *span))
}
}
之前,我们只是在绑定映射中查找类型,现在在绑定映射中查找 Scheme
枚举。如果它包含一个类型,就使用它,否则我们调用包含的闭包来生成新类型。
推导类型方案
说完了这些,是时候实际创建一些类型方案了。记得之前,Let
处理代码在处理 let
表达式和顶层 let
定义之间是重复的。由于将对它进行更复杂的修改,我已经提前将它重构为 check_let
函数,以避免重复。
Let((name, var_expr), rest_expr) => {
let var_scheme = check_let(engine, bindings, var_expr)?;
bindings.in_child_scope(|bindings| {
bindings.insert_scheme(name.clone(), var_scheme);
check_expr(engine, bindings, rest_expr)
})
}
现在到了有趣的部分 - check_let
本身。
fn check_let(engine: &mut TypeCheckerCore, bindings: &mut Bindings, expr: &ast::Expr) -> Result<Scheme> {
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))
}
这看起来可能有点吓人,但它所做的就是创建一个闭包,对给定的 Expr
进行类型检查,并返回结果类型。
let saved_bindings = RefCell::new(Bindings {
m: bindings.m.clone(),
changes: Vec::new(),
});
let saved_expr = expr.clone();
首先,我们需要复制类型环境和 ast 子树,这样就可以在闭包中存储它们。这并不是严格必须的。可以通过在代码的其他地方做一些改动来消除 AST 副本和大部分绑定副本,但现在我们要采用真正的懒惰实现方法来最小化所需的代码改动。(不过必须将 AST 节点类型标记为可克隆。如果不这样做,会导致 Rust 中出现一个非常混乱的编译器错误,所以要注意这一点。)
let f: Rc<dyn Fn(&mut TypeCheckerCore) -> Result<Value>> =
Rc::new(move |engine| check_expr(engine, &mut saved_bindings.borrow_mut(), &saved_expr));
之后,只需创建闭包对象。遗憾的是,Rust 在这里需要一个明确的类型注释。
f(engine)?;
Ok(Scheme::Poly(f))
最后,调用闭包,然后返回一个包含闭包的 Scheme
。第一点有点微妙。回顾一下,我们目前的实现基本上只是在变量被引用时对 let
定义的主体进行类型检查。然而,cubiml 有严格的执行语义,意味着我们需要对定义进行至少一次类型检查,即使变量从未被引用。
例如,考虑以下代码。
let x = false + 34 in
"hello, world!";
如果没有上面额外的 f(engine)?
调用,错误的 false + 34
相加将通过类型检查器而不是返回错误,因为变量 x
从未被引用,因此它的方案回调从未被调用。
需要注意的是,如果你事先在单独的通道中进行变量解析(这是个好主意),你可以通过在变量解析过程中标记(甚至优化掉)未使用的变量来消除这个检查的需要。
值限制
遗憾的是,我们还没有完全完成。上面的代码大部分是可行的,但与可变结合起来就不健全了。考虑下面的例子。
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
下周,我们将看到如何使用值限制来解决这个问题。