[译]通过例子学子类型推理(十二):流类型和混合比较运算符
上周,我们完成了 let 多态的实现,这是经典 Hindley-Milner 类型系统以及代数子类型系统中最后缺少的部分。目前为止,我们所实现的所有东西都是基于代数子类型化中提出的类型系统,或者至少是基于该系统的直接扩展。
然而,本周我们将抛开优雅的窗口,看一些独特的功能,这些功能可以通过立方双合一 hack 进类型系统。具体来说,我们将实现混合比较运算符和流类型。
混合比较运算符
回想一下,最初实现运算符时,我们为比较整型和浮点型引入了单独版本的比较运算符。也就是说,必须使用 <
来比较整型,而使用 <.
来比较浮点型。然而,如果我们能对两者使用相同的运算符,甚至直接比较整型和浮点型,那就更好了。
>> 9007199254740992 > 9007199254740992.0
false
>> 9007199254740992 >= 9007199254740992.0
true
>> 9007199254740993 > 9007199254740992.0
true
到目前为止,值类型头和用类型头之间一直保持着美丽的对称性。然而,现在是时候打破这种局面了,增加一个新的用类型头,UIntOrFloat
,没有对应的值类型。
UFloat,
UInt,
UStr,
+ UIntOrFloat,
UFunc {
arg: Value,
ret: Use,
接下来,需要更新 check_heads
来使用新头类型。UInt或Float
将与左边的 VInt
或 VFloat
进行匹配。从代码上看,这是一个相当微不足道的变化,但它仍然与最初的代数子类型论文中的设想相去甚远。
(&VFloat, &UFloat) => Ok(()),
(&VInt, &UInt) => Ok(()),
(&VStr, &UStr) => Ok(()),
+ (&VInt, &UIntOrFloat) => Ok(()),
+ (&VFloat, &UIntOrFloat) => Ok(()),
(&VFunc { arg: arg1, ret: ret1 }, &UFunc { arg: arg2, ret: ret2 }) => {
out.push((ret1, ret2));
最后,更新 AST、语法、类型检查器前端等,来使用新类型。这个很直接,所以我就不深入介绍了。
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -31,8 +31,7 @@ pub enum OpType {
FloatOp,
StrOp,
- IntCmp,
- FloatCmp,
+ IntOrFloatCmp,
AnyCmp,
}
--- a/src/core.rs
+++ b/src/core.rs
@@ -169,6 +172,7 @@ fn check_heads(
UFloat => "float",
UInt => "integer",
UStr => "string",
+ UIntOrFloat => "float or integer",
UFunc { .. } => "function",
UObj { .. } => "record",
UCase { .. } => "case",
@@ -269,6 +273,9 @@ impl TypeCheckerCore {
pub fn str_use(&mut self, span: Span) -> Use {
self.new_use(UTypeHead::UStr, span)
}
+ pub fn int_or_float_use(&mut self, span: Span) -> Use {
+ self.new_use(UTypeHead::UIntOrFloat, span)
+ }
pub fn func(&mut self, arg: Use, ret: Value, span: Span) -> Value {
self.new_val(VTypeHead::VFunc { arg, ret }, span)
--- a/src/grammar.lalr
+++ b/src/grammar.lalr
@@ -164,15 +164,10 @@ AddOp: Box<ast::Expr> = {
},
}
CmpOpSub: (ast::OpType, ast::Op) = {
- "<" => (ast::OpType::IntCmp, ast::Op::Lt),
- "<=" => (ast::OpType::IntCmp, ast::Op::Lte),
- ">" => (ast::OpType::IntCmp, ast::Op::Gt),
- ">=" => (ast::OpType::IntCmp, ast::Op::Gte),
-
- "<." => (ast::OpType::FloatCmp, ast::Op::Lt),
- "<=." => (ast::OpType::FloatCmp, ast::Op::Lte),
- ">." => (ast::OpType::FloatCmp, ast::Op::Gt),
- ">=." => (ast::OpType::FloatCmp, ast::Op::Gte),
+ "<" => (ast::OpType::IntOrFloatCmp, ast::Op::Lt),
+ "<=" => (ast::OpType::IntOrFloatCmp, ast::Op::Lte),
+ ">" => (ast::OpType::IntOrFloatCmp, ast::Op::Gt),
+ ">=" => (ast::OpType::IntOrFloatCmp, ast::Op::Gte),
"==" => (ast::OpType::AnyCmp, ast::Op::Eq),
"!=" => (ast::OpType::AnyCmp, ast::Op::Neq),
--- a/src/typeck.rs
+++ b/src/typeck.rs
@@ -90,16 +90,9 @@ fn check_expr(engine: &mut TypeCheckerCore, bindings: &mut Bindings, expr: &ast:
engine.flow(rhs_type, rhs_bound)?;
engine.str(*full_span)
}
- IntCmp => {
- let lhs_bound = engine.int_use(*lhs_span);
- let rhs_bound = engine.int_use(*rhs_span);
- engine.flow(lhs_type, lhs_bound)?;
- engine.flow(rhs_type, rhs_bound)?;
- engine.bool(*full_span)
- }
- FloatCmp => {
- let lhs_bound = engine.float_use(*lhs_span);
- let rhs_bound = engine.float_use(*rhs_span);
+ IntOrFloatCmp => {
+ let lhs_bound = engine.int_or_float_use(*lhs_span);
+ let rhs_bound = engine.int_or_float_use(*rhs_span);
engine.flow(lhs_type, lhs_bound)?;
engine.flow(rhs_type, rhs_bound)?;
engine.bool(*full_span)
流类型
在现代编程语言中,你可以用一种方式使用 case 类型(又名 sum 类型)来表示具有几种可能的值和/或类型之一的值,可以由编译器静态检查。例如,下面的 cubiml 代码实现了单例模式,最多调用一次提供的初始化函数,使用 None
和 Some
中的 case 类型分别表示数据未初始化和已经初始化的状态。
let lazy_init = fun init_cb ->
let cache = ref `None {} in
fun _ ->
match !cache with
| `Some val -> val
| `None _ -> (
let val = init_cb {} in
let _ = cache := `Some val in
val
);
然而,旧的语言,特别是 C 启发的语言,可能没有 case 类型。然而,表达具有多种可能性之一的值的需求并不会因为语言没有很好地支持它而消失。相反,这些语言中的程序员会隐式模拟 case 类型,而没有真正的 case 类型的语言支持或静态类型检查。
例如,在 C 风格的语言中,程序员可能会使用空指针来代表未初始化状态,非空指针代表初始化状态来写上面的代码。每当他们读取值时,他们就需要在使用前对其进行空检查,但没有编译器辅助来强制执行这一点。事实上,忘记检查空值是一个很常见的错误,以至于空指针经常被称为“十亿美金的错误”。
类型系统和类型推理通常是在设计一种新语言的背景下讨论的。然而,也可以为现有的编程语言创建新的类型检查器。这样做要难得多,因为你不再有能力塑造语言特性以方便类型检查,而是必须在你希望分析的遗留代码中与程序员正在使用的任何临时代码模式打交道。
然而,回报也是巨大的,因为它允许你在现有遗留代码的庞大生态系统中捕捉问题。这方面的大多数努力都集中在 C 和 JavaScript 上,因为它们巨大的经济重要性,只有它们巨大的错误倾向才能匹配。例如,TypeScript 就是为了改进 JS 代码的类型检查而做出的努力。
此外,即使在设计一种新语言时,你也可能需要添加空指针以实现与现有语言的互操作性。例如,Kotlin 通过密封类和 when 表达式来支持 sum 类型,但它为了和 Java 的互操作性,仍然有空指针。
空安全
类型检查遗留代码意味着找到处理现有代码模式的方法,这通常意味着增加一种有限制的流敏感类型形式。今天我将演示一个最简单的情况,静态空值安全检查。
我们的目标是静态地确保潜在的空值如果没有先通过 if x != null then ...
或类似的代码对其进行空检查,就永远不会被使用。为了做到这一点,我们识别这样的 if 表达式,并在类型检查器中对其进行特殊处理,将其视为对隐式 case 类型的匹配。
然而,还有一个复杂的问题 - 如何暴露精炼类型。我们的匹配表达式语法从一开始就是为处理 case 类型而设计的,所以每个分支都绑定了具有相应类型的新变量。例如,在
match foo with
| `None _ => ...
| non_null_foo => ...
中,non_null_foo
变量的类型将与 foo
相同,只是静态地移除了 None
case。然而,如果试图将传统的 if 表达式转换为模式匹配,我们就没有这种奢侈。普通的 if 语句不会引入任何新变量,我们可以将精炼类型赋予这些变量。
因此,我们将特殊 case 的处理限制在条件形式为 foo == null
或 foo != null
的 if 表达式的 case 下,其中 foo
是局部变量(而不是任意表达式)。然后,在适当的分支中,我们可以就地给该变量赋予精炼类型。我们的目标是实现类似以下的功能
(* Create a value that might be null, at least from the
typechecker's point of view. *)
let s = if true then "Hello" else null;
(* s has type "string | null" here *)
if s != null then
(* Within this branch, s instead has the type "string".
String concatenation is allowed here since s is
statically known to be a string and not null. *)
s ^ " world!"
else
(* We could give s the type "null" here, but that's
pretty much useless, so we'll just leave its
type unchanged on the "null" branch *)
"error, unexpected null";
(* s has type "string | null" again here *)
s
空值
首先,我们需要给 cubiml 添加空值。我们在类型系统中添加新基础类型 null
,以及新字面量 null
来创建该类型的值。这非常直接,因为添加基础类型的过程与之前添加其他基础类型(如布尔值和字符串)的过程完全相同。唯一不同的是,有空值类型,但没有空用类型。
@@ -5,6 +5,7 @@ pub enum Literal {
Bool,
Float,
Int,
+ Null,
Str,
}
@@ -17,6 +17,7 @@ enum VTypeHead {
VBool,
VFloat,
VInt,
+ VNull,
VStr,
VFunc {
arg: Use,
@@ -161,6 +162,7 @@ fn check_heads(
VBool => "boolean",
VFloat => "float",
VInt => "integer",
+ VNull => "null",
VStr => "string",
VFunc { .. } => "function",
VObj { .. } => "record",
@@ -257,6 +259,9 @@ impl TypeCheckerCore {
pub fn int(&mut self, span: Span) -> Value {
self.new_val(VTypeHead::VInt, span)
}
+ pub fn null(&mut self, span: Span) -> Value {
+ self.new_val(VTypeHead::VNull, span)
+ }
pub fn str(&mut self, span: Span) -> Value {
self.new_val(VTypeHead::VStr, span)
}
@@ -38,6 +38,7 @@ VarOrLiteral: Box<ast::Expr> = {
Spanned<Ident> => Box::new(
match <>.0.as_str() {
"false" | "true" => ast::Expr::Literal(ast::Literal::Bool, <>),
+ "null" => ast::Expr::Literal(ast::Literal::Null, <>),
_ => ast::Expr::Variable(<>)
}
),
@@ -160,6 +160,7 @@ fn check_expr(engine: &mut TypeCheckerCore, bindings: &mut Bindings, expr: &ast:
Bool => engine.bool(span),
Float => engine.float(span),
Int => engine.int(span),
+ Null => engine.null(span),
Str => engine.str(span),
})
}
空检查类型
接下来,我们需要给类型系统增加空检查用类型。
UNullCase {
nonnull: Use,
},
pub fn null_check_use(&mut self, nonnull: Use, span: Span) -> Use {
self.new_use(UTypeHead::UNullCase { nonnull }, span)
}
请注意,这里实际上从未使用过跨度参数,但我们仍然必须包含它,因为当前的设计为每个类型节点存储了跨度。
接下来,在 check_heads
中添加支持。
(&VNull, &UNullCase { .. }) => Ok(()),
(_, &UNullCase { nonnull }) => {
out.push((Value(lhs_ind), nonnull));
Ok(())
}
检查这种类型非常简单。它基本上只是之前介绍过的通配符 case 匹配的极其简化的版本。如果左边是非空值,我们从它那里添加流约束到用类型的 nonnull
字段,类似于 case 用类型的 wildcard
字段。如果左边是空值,就什么都不做。
我们还需要把它添加到 check_heads
的 fallthrough 分支中,因为 Rust 还不够聪明,没有意识到它永远不会因为与左边的任何值类型匹配而卷入类型错误。
UObj { .. } => "record",
UCase { .. } => "case",
URef { .. } => "ref",
+ UNullCase { .. } => unreachable!(),
};
前端空检查
现在到了最复杂的部分 - 实际使用这个类型。大部分的工作是在类型检查器前端完成的。回想一下,我们要找到 if foo == null then...
或 if foo != null then...
形式的表达式,并对它们进行特殊处理。
要做到这一点,我们在前端找到处理 If
表达式的分支,并插入一堆代码来寻找 if foo != null then...
模式,并在这种情况下做一些不同的事情。
// Handle conditions of the form foo == null and foo != null specially
if let BinOp((lhs, _), (rhs, _), ast::OpType::AnyCmp, op, ..) = &**cond_expr {
if let Variable((name, _)) = &**lhs {
if let Literal(ast::Literal::Null, ..) = **rhs {
let lhs_type = check_expr(engine, bindings, lhs)?;
// Flip order of branches if they wrote if foo == null instead of !=
let (ok_expr, else_expr) = match op {
ast::Op::Neq => (then_expr, else_expr),
ast::Op::Eq => (else_expr, then_expr),
_ => unreachable!(),
};
let (nnvar_type, nnvar_bound) = engine.var();
let bound = engine.null_check_use(nnvar_bound, *span);
engine.flow(lhs_type, bound)?;
let ok_type = bindings.in_child_scope(|bindings| {
bindings.insert(name.clone(), nnvar_type);
check_expr(engine, bindings, ok_expr)
})?;
let else_type = check_expr(engine, bindings, else_expr)?;
let (merged, merged_bound) = engine.var();
engine.flow(ok_type, merged_bound)?;
engine.flow(else_type, merged_bound)?;
return Ok(merged);
}
}
}
这是相当大的一块儿代码,所以我们把它分解开来。首先,检查 if 条件是否为 foo == null
或 foo != null
形式,其中 foo
是局部变量。然后,抓取该变量的(未精炼)类型,并将其存储在 lhs_type
中。
if let BinOp((lhs, _), (rhs, _), ast::OpType::AnyCmp, op, ..) = &**cond_expr {
if let Variable((name, _)) = &**lhs {
if let Literal(ast::Literal::Null, ..) = **rhs {
let lhs_type = check_expr(engine, bindings, lhs)?;
接下来,找到 if 表达式分支对应的 AST 子表达式,当被检查变量是非空或空时。对于 != null
比较,这些分别只是 if 表达式的 then 和 else 分支。对于 ==null
比较,这些分支是相反的。
// Flip order of branches if they wrote if foo == null instead of !=
let (ok_expr, else_expr) = match op {
ast::Op::Neq => (then_expr, else_expr),
ast::Op::Eq => (else_expr, then_expr),
_ => unreachable!(),
};
接下来,需要细化 lhs_type
,以获得类型的“非空版本”。
let (nnvar_type, nnvar_bound) = engine.var();
let bound = engine.null_check_use(nnvar_bound, *span);
engine.flow(lhs_type, bound)?;
这个过程与通配符 case 匹配非常相似,只是要简单的多,因为只有一个分支。回想一下,null_check_use
接收用类型参数。在 check_heads
中,每当对值类型头与产生的用类型头 UNullCase
进行检查时,当左边是非空的时候,我们会从左边(值)类型向右边存储的用类型添加流约束。当左手边为空时,什么都不做。
假设 lhs_type
的类型是 string | null
,下面是在类型检查器中,一步步发生的。
- 添加流
VString -> lhs_type_bound
,其中lhs_type_bound
是lhs_type
类型变量的“左侧”(根据假设) - 添加流
VNull -> lhs_type_bound
(假设) bound = UNullCase{nonnull=nnvar_bound}
- 添加流
lhs_type -> bound
。- 由于可到达性,这将产生对
check_heads(VString, bound)
和check_heads(VNull, bound)
的调用
- 由于可到达性,这将产生对
check_heads(VString, bound)
:VString
不为空,所以添加流约束VString -> bound.nonnull
。bound.nonnull = nnvar_bound
,所以这意味着VString
流向nnvar_bound
。- 由于
nnvar_bound
是nnvar_type
代表的变量的“左半部分”,这意味着nnvar_type
“看到了”VString
。我们可以认为nnvar_type
现在是类型string
。
check_heads(VNull, bound)
:VNull
为空,所以不采取任何进一步的行动
最终结果是,当 lhs_type
类型为 string | null
时,nnvar_type
类型为 string
。本质上,它是 lhs_type
的非空值版本,正如预期的那样。
接下来,我们在新绑定环境中对非空分支进行类型检查,其中变量具有精炼类型 nnvar_type
而不是 lhs_type
。
let ok_type = bindings.in_child_scope(|bindings| {
bindings.insert(name.clone(), nnvar_type);
check_expr(engine, bindings, ok_expr)
})?;
我们在原始绑定环境中对空分支进行类型检查,其中变量的类型是未精炼的 lhs_type
。我们可以在这里把它的类型细化为普通的 null
,但是没有实际意义,因为如果变量在某一点上确定为空,cubiml 不会让你做任何事情。只有确定不为空才是真正有用的。
let else_type = check_expr(engine, bindings, else_expr)?;
最后,像往常一样,通过创建流约束到新临时变量,将两个分支的结果类型“联合起来”,然后返回联合类型。
let (merged, merged_bound) = engine.var();
engine.flow(ok_type, merged_bound)?;
engine.flow(else_type, merged_bound)?;
return Ok(merged);
处理多态
上面的代码大部分都是可行的,但是有一个问题。当在现有的语言构造中添加特例行为时,必须确保这样做不会随机破坏不相关的代码。不幸的是,上面的实现有可能会破坏多态代码。考虑下面的例子:
let id = fun x -> x;
if id != null then
let _ = (id 1) + 3 in
(id "x") ^ "y"
else {}
上面的代码用多个不兼容的类型调用 id
。不过,由于有了 let 多态性,它应该还能工作,事实上,如果没有特殊情况下的空检查行为,它确实能工作。遗憾的是,上述空检查的实现神奇地将环境中 id
的多态类型方案替换成了单态精炼类型,导致了虚假的类型错误:
TypeError: Value is required to be a integer here,
if id != null then
let _ = (id 1) + 3 in
^~~~~~
(id "x") ^ "y"
else {}
But that value may be a string originating here.
if id != null then
let _ = (id 1) + 3 in
(id "x") ^ "y"
^~~
else {}
感谢上周实现值限制时的懒惰,这很容易解决。由于只对函数定义进行泛化,我们知道多态类型方案将始终代表函数类型,因此是非空的。因此,可以安全地简单跳过这种情况,根本不用费心去尝试精炼类型。
if let Some(scheme) = bindings.get(name.as_str()) {
if let Scheme::Mono(lhs_type) = scheme {
// same code as before...
}
}
cubiml 实现只有当 foo
在当前绑定中具有单态类型时,才会为 if foo != null then ...
执行空检查。我们可以摆脱这种情况,因为值限制的过于保守的实现意味着多态类型方案永远只是函数类型。
然而,如果你实现全值限制,类型方案可以表示任意类型,有可能包括空值,所以你也必须多态地进行空检查。如果你使用推荐的优化方法来实现 let 多态,即预先计算类型图,然后根据需要复制该图,那么这只是用相同的预计算类型图创建新类型方案的问题,除了在图中添加了空检查节点。
// Handle conditions of the form foo == null and foo != null specially
if let BinOp((lhs, _), (rhs, _), ast::OpType::AnyCmp, op, ..) = &**cond_expr {
if let Variable((name, _)) = &**lhs {
if let Literal(ast::Literal::Null, ..) = **rhs {
if let Some(scheme) = bindings.get(name.as_str()) {
if let Scheme::Mono(lhs_type) = scheme {
// Flip order of branches if they wrote if foo == null instead of !=
let (ok_expr, else_expr) = match op {
ast::Op::Neq => (then_expr, else_expr),
ast::Op::Eq => (else_expr, then_expr),
_ => unreachable!(),
};
let (nnvar_type, nnvar_bound) = engine.var();
let bound = engine.null_check_use(nnvar_bound, *span);
engine.flow(*lhs_type, bound)?;
let ok_type = bindings.in_child_scope(|bindings| {
bindings.insert(name.clone(), nnvar_type);
check_expr(engine, bindings, ok_expr)
})?;
let else_type = check_expr(engine, bindings, else_expr)?;
let (merged, merged_bound) = engine.var();
engine.flow(ok_type, merged_bound)?;
engine.flow(else_type, merged_bound)?;
return Ok(merged);
}
}
}
}
}
以上是完整的、修复后的代码版本。它非常丑陋,但对于演示目的来说已经足够好了。如果你决定在你的语言中更广泛地使用流类型,你将需要重构一些东西,以便更干净地进行检查,因为像这样的临时插入很快就会堆积起来,并开始导致错误。理想情况下,你将能够将你的流类型实现与处理模式匹配的代码统一起来,因为它们在引擎盖下做的基本上是同样的事情。
下周,我们将通过向类型检查器(也就是存在变量)添加条件流边来进一步推动类型系统,并看看如何在编译时在类型系统中进行任意计算。