上周，我们介绍了为 cubiml 添加一些更独特的功能，特别是介绍了流类型，一种在尚未有 case 类型(也就是 sum 类型)的语言中模拟 case 类型的方法。今天我们将另辟蹊径，提高原生 case 类型的精度(对上一篇文章中的模拟空 case 类型进行相应的修改，留给读者去练习，但步骤与下面的非常相似)。

条件流约束

回顾一下，case 类型是一种创建值的方式，可以在运行时代表几种可能性（可能有不同的类型）中的一种，以一种可以在运行时安全匹配的方式。

例如，下面的代码演示了一个函数，它可以取几个形状中的一个并计算其面积。重要的是，这一切都在编译时进行了检查。如果你试图传递没有被处理的 case，或者传递被处理 case 的错误类型，你将在编译时得到一个类型错误。

let area = fun arg ->
    match arg with
        | `Square x -> x.len *. x.len
        | `Rect x -> x.height *. x.width;

area `Square {len=4.};
area `Rect {height=4.; width=2.5};

let area2 = fun arg ->
    match arg with
        | `Circle x -> x.radius *. x.radius *. 3.1415926
        | x -> area x;

area2 `Square {len=4.};
area2 `Rect {height=4.; width=2.5};
area2 `Circle {radius=1.2}

匹配允许处理调用者从未实际传递的 case。在运行时，只有与匹配 case 相关的特定分支会被执行。然而，在编译时，匹配表达式被当作每个分支都有可能被采用。例如，考虑以下代码

let increment = fun x ->
    match x with
        | `Int i -> i + 1
        | `Float f -> f +. 1.0;

(increment `Int 7) * -3

这将导致类型错误：

TypeError: Value is required to be a integer here,
        | `Float f -> f +. 1.0;

(increment `Int 7) * -3
^~~~~~~~~~~~~~~~~~
But that value may be a float originating here.
    match x with
        | `Int i -> i + 1
        | `Float f -> f +. 1.0;
                      ^~~~~~~~

(increment `Int 7) * -3

在运行时，如果传递 Int case，增量函数将返回整型，如果传递 Float case，则返回浮点型。然而，类型检查器会把它当作每个分支总是被采用，从而推断出返回类型为 int | float。在本周的文章中，我们将看到如何解决这个问题。但首先要声明一下。

免责声明

提高类型精度的主要障碍是技术上的 - 哪些功能可以用什么样的复杂度来实现？如果一个特性在技术上不可行，那么进一步讨论它就没有意义，所以这就是我们关注的问题。

然而，仅仅因为你可以实现一个特性，并不意味着你一定应该实现。有时，一个不那么精确的类型系统实际上是一件好事。例如，设计一个完全跳过死代码检查的类型检查器是非常容易的。然而，类型检查无法到达的代码对于检测额外的错误还是很有用的。此外，使类型系统不那么精确有时会让程序员更容易在心理上建模和推理，使语言不那么混乱。

为此，我们今天要实现的功能是一种折中。它仍然会对匹配表达式的每一个分支进行类型检查，甚至是无法到达的分支，但只有可能被采用的分支才会对表达式的结果类型做出贡献。

类型系统设计

回想一下，类型检查器前端目前为匹配表达式的每个分支运行以下代码：

let (wrapped_type, wrapped_bound) = engine.var();
case_type_pairs.push((tag.clone(), wrapped_bound));

let rhs_type = bindings.in_child_scope(|bindings| {
    bindings.insert(name.clone(), wrapped_type);
    check_expr(engine, bindings, rhs_expr)
})?;
engine.flow(rhs_type, result_bound)?;

对于我们的目的来说，最重要的部分是最后一行，它增加了一个流约束，从 rhs_type （匹配臂右侧的类型）到 result_bound （整个匹配表达式的结果类型）。我们不想立即添加这个流边，而是想将这些节点存储在类型检查器中，只有在该分支确定实际使用后，才惰性地添加这个边。

首先，我们为代表延迟流约束的（值，用）对添加一个 typedef。

pub type LazyFlow = (Value, Use);

然后把它添加到 case 用类型头的每个分支和相应的构造函数中。

UCase {
    cases: HashMap<String, (Use, LazyFlow)>,
    wildcard: Option<(Use, LazyFlow)>,
},

     }
-    pub fn case_use(&mut self, cases: Vec<(String, Use)>, wildcard: Option<Use>, span: Span) -> Use {
+    pub fn case_use(&mut self, cases: Vec<(String, (Use, LazyFlow))>, wildcard: Option<(Use, LazyFlow)>, span: Span) -> Use {
         let cases = cases.into_iter().collect();

接下来，更新 check_heads 的实现。从类型系统上来说，这是最重要的部分，但它出奇的简单。我们要做的就是，每当检查 case 类型时，也会将对应分支的懒惰流约束添加到待处理的流约束列表中。（注意下面新的 out.push(lazy_flow) 行）。

// Check if the right case is handled
if let Some((rhs2, lazy_flow)) = cases2.get(name).copied() {
    out.push((lhs2, rhs2));
    out.push(lazy_flow);
    Ok(())
} else if let Some((rhs2, lazy_flow)) = wildcard {
    out.push((Value(lhs_ind), rhs2));
    out.push(lazy_flow);
    Ok(())
} else {

最后，还要更新类型检查器前端的代码。

let (wrapped_type, wrapped_bound) = engine.var();
let rhs_type = bindings.in_child_scope(|bindings| {
    bindings.insert(name.clone(), wrapped_type);
    check_expr(engine, bindings, rhs_expr)
})?;

case_type_pairs.push((tag.clone(), (wrapped_bound, (rhs_type, result_bound))));

之前我们有 engine.flow(rhs_type, result_bound)，现在只需将 (rhs_type, result_bound) 对添加到 case_type_pairs 中，而 case_type_pairs 又会被传递给之前定义的类型检查器核心构造函数。

同样的，我们对处理通配符分支的代码（如果有的话）也做同样的事情。

let (wrapped_type, wrapped_bound) = engine.var();
let rhs_type = bindings.in_child_scope(|bindings| {
    bindings.insert(name.clone(), wrapped_type);
    check_expr(engine, bindings, rhs_expr)
})?;

wildcard_type = Some((wrapped_bound, (rhs_type, result_bound)));

就是这样! 上面的代码示例现在已经通过了类型检查器。不过，设计上还是有一些细微的地方需要注意。

多态和条件流

在运行时，任何给定的匹配表达式的计算都只会导致一个分支被计算（并且该分支的值被返回）。然而，我们的代码将匹配臂的类型添加到匹配表达式的结果类型中，如果该分支可以从程序中的任何地方任意调用。

这意味着，如果同时使用 Int 和 Float 两种 case 调用 increment ，结果类型将再次变成 int | float ，我们将再次得到一个类型错误。

let id = fun x -> x;
(* Use id to force increment to be monomorphic *)
let increment = id (fun x ->
    match x with
        | `Int i -> i + 1
        | `Float f -> f +. 1.0);

(increment `Int 7) * -3;
(increment `Float 7.0) *. -3.0

TypeError: Value is required to be a integer here,
        | `Float f -> f +. 1.0);

(increment `Int 7) * -3;
^~~~~~~~~~~~~~~~~~
(increment `Float 7.0) *. -3.0
But that value may be a float originating here.
    match x with
        | `Int i -> i + 1
        | `Float f -> f +. 1.0);
                      ^~~~~~~~

(increment `Int 7) * -3;

这可能会让这个功能显得很无用。反正程序员可以直接删除死代码，那么忽略死代码有什么用呢？事实上，这个功能对于单态代码来说基本上是无用的。然而，当与 let 多态结合后，故事就完全变了。

在前面的例子中，我们为了强制单态化，把 increment 的定义包装在了对 id 的调用中（回忆一下，值限制对函数调用并不友好）。如果我们修改上面的例子，去掉这个调用，让 increment 成为多态的，就不会再产生类型错误。

let increment = fun x ->
    match x with
        | `Int i -> i + 1
        | `Float f -> f +. 1.0;

(increment `Int 7) * -3;
(increment `Float 7.0) *. -3.0

这是因为当 increment 是多态的时候，每次使用都会有一个新的、独立的类型副本被标记，条件流只触发调用者到那个特定副本的匹配臂。在单态的情况下，一个匹配臂只有在所有调用者都未使用的情况下才无用，在这种情况下，代码可以简单地被删除。在多态情况下，一个匹配臂可能在某些调用点未被使用，而在其他地方仍被其他调用者使用。它本质上将匹配表达式类型变成了“只为你使用的付费”，并以每个调用点为基础。

存在变量

这种类型特征有时被称为存在多态，是行多态的近亲。我们可以将上面的 increment 函数的类型方案描述为forall Pi, Pf => (`Int int if Pi | `Float float if Pf) -> (int if Pi | float if Pf)，其中 Pi 和 Pf 不是通常的单态范围之上的类型变量 T 和 U，而是表示 case 存在或确实的的存在变量。

类型级计算

类型级计算并不是我们将在类型系统中实现的具体功能，而是很酷但不实用的技巧，你可以使用已经实现的功能，特别是使用条件流约束。

关键的见解是，条件流允许我们在类型检查过程中有条件地对类型执行操作。当然，条件并不是类型级计算所必需的 - 你甚至可以只用 lambda 计算来实现对类型的任意计算。然而，使用条件的能力使它变得更加容易和自然。

如果没有条件，你必须把所有的东西都编码成无分支代码，SPMD-style。这不仅做起来很麻烦，而且使内存访问的效率非常低。为了在无分支代码中执行随机内存访问，你必须在每次访问时扫描整个内存空间，并且只为你真正需要的一个位置保留结果。而条件流则可以让你以更自然、更高效的方式编写类型级计算。

从上一篇关于 let 多态性能的文章中回想一下，let 多态可以让你简明地将指数数量的调用组合成一个不同类型的单独函数。因此，我们将编写一个执行单步工作的函数，“程序状态”由函数的输入和输出类型表示。然后，我们使用多态来很多次调用该函数，基本上是以期望的步数“运行”程序。

编译时斐波那契

为了便于演示，我们将在编译时实现一个计算斐波那契数的函数。斐波那契数很容易计算。通常情况下，你会使用类似下面的代码：

let rec fib_sub = fun args ->
    if args.n <= 0 then
        args.a
    else
        fib_sub {n=args.n - 1; a=args.a + args.b; b=args.a};

let fib = fun n -> fib_sub {n=n; a=1; b=1};
fib 12

然而，我们希望在编译时使用类型进行计算，这就需要一种更不寻常的编码风格。特别是，不能使用循环或递归。相反，我们必须执行单步计算，然后“返回”状态。此外，我们不能使用常规整数，所以必须创建自己的整数。

类型级整数

为了在类型层面上进行数学运算，我们需要一种表示整数的方法，其中每个整数都是一个独立的类型。传统上，这是用一元编码完成的，但为了提高效率，我们将使用二进制代替。

每个数字都表示为一串二进制数字，其中每个数字都使用一个 case 类型变体来表示。为了使它们易于使用，我们将使用小端数字（在代码中写入时，最低有效数字出现在左边），并有一个特殊的标签 End 来标记数字的结束。下面是一些编码的例子：

let end = `End {};

let one = `1 end;
let two = `0`1 end;
let seven = `1`1`1 end;
let twelve = `0`0`1`1 end;
let million_and_eighty_seven = `1`1`1`0`1`0`0`1`0`1`0`0`0`0`1`0`1`1`1`1 end;

然后，需要编写辅助函数来逐位递增、递减和相加这些编码数字。

let end = `End {};

(* Decrement x by 1. If x is already zero, return `Error,
    else, return `Ok (x - 1) *)
let rec decrement = fun x ->
    match x with
    | `End _ -> `Error {}
    | `1 xs -> `Ok `0 xs
    | `0 xs -> (
        match decrement xs with
        | `Ok xs_dec -> `Ok `1 xs_dec
        | _ -> _
    );

(* Add args.x + 1 *)
let rec increment = fun x ->
    match x with
    | `End _ -> `1 end
    | `0 xs -> `1 xs
    | `1 xs -> `0 (increment xs);

(* Add args.x + args.y *)
let rec add = fun args ->
    match args.y with
    | `End _ -> args.x
    | `0 ys -> add_shifted {x=args.x; ys=ys}
    | `1 ys -> add_shifted {x=increment args.x; ys=ys}
and add_shifted = fun args ->
    (* Add args.x + (args.ys << 1) *)
    match args.x with
    | `End _ -> `0 args.ys
    | `0 xs -> `0 (add {x=xs; y=args.ys})
    | `1 xs -> `1 (add {x=xs; y=args.ys})
    ;

let rec fib_sub = fun args ->
    match decrement args.n with
    | `Error _ -> args.a
    | `Ok n ->
        fib_sub {n=n; a=add {x=args.a; y=args.b}; b=args.a};


let fib = fun n -> fib_sub {n=n; a=`1 end; b=`1 end};
fib `0`0`1`1 end

模拟递归

由于使用了递归，上述代码在编译时仍然无法运行。为了进行类型级别的计算，需要“解开”所有的递归并模拟调用栈。每个帮助函数都会接收一个包含字段 val、stack 和其他可选字段的栈帧。val 被设置为前一个函数调用所“返回”的任意内容。stack 是栈上的下一帧。帧中的其他字段只是在帧最初创建时保存的内容。

我们的函数不直接调用函数，而是将要调用的函数名推送到栈上，然后返回新的栈。然后有一个 tick 函数，只是从栈中弹出并调用相应的函数。

另外，需要在每个函数调用函数的每个点，将它拆成独立的函数，这样就有了“返回”的地方。例如，可以将 increment 函数转换为这种样式，如下所示，添加 increment2 函数来处理推送最后的 `0 到递归的“返回”的值上。

(* Add frame.val + 1 *)
let increment = fun frame ->
    match frame.val with
    | `End _ -> {frame | val=`1 end}
    | `0 xs -> {frame | val=`1 xs}
    | `1 xs -> (
        (* call increment2 (increment xs) *)
        (* where increment2 = fun x -> `0 x *)
        {val=xs; stack=`Increment {stack=`Increment2 {stack=frame.stack}}}
    );
let increment2 = fun frame -> {frame | val=`0 frame.val};

然后可以调用增量函数，如下所示

let tick = fun state ->
    match state.stack with
    | `Increment frame -> increment {frame | val=state.val}
    | `Increment2 frame -> increment2 {frame | val=state.val}
    (* if the computation is done, just return the state unchanged *)
    | `Done _ -> state
    ;

(* set up initial state to call increment `1`1`0`1 end *)
let state = {val=`1`1`0`1 end; stack=`Increment {stack=`Done {}}};
let state = tick state;
let state = tick state;
let state = tick state;
let state = tick state

重要的是，增量函数是在编译类型时计算的，所以可以在编译时对结果进行断言。例如，下面的代码断言结果是 `0`0`1`1 end。如果是其他的东西，编译时就会得到一个错误。

match state.stack with | `Done _ -> _;
match state.val with | `0 x ->
    (match x with | `0 x ->
    (match x with | `1 x ->
    (match x with | `1 x ->
    (match x with | `End _ -> _))))

递增数字并不是那么令人兴奋，所以让我们继续转换剩下的斐波那契计算代码。

let end = `End {};

let push0 = fun frame -> {frame | val=`0 frame.val};
let push1 = fun frame -> {frame | val=`1 frame.val};

(* Add frame.val + 1 *)
let increment = fun frame ->
    match frame.val with
    | `End _ -> {frame | val=`1 end}
    | `0 xs -> {frame | val=`1 xs}
    | `1 xs -> (
        (* call push0 (increment xs) *)
        (* where push0 = fun x -> `0 x *)
        {val=xs; stack=`Increment {stack=`Push0 {stack=frame.stack}}}
    );

(* Decrement frame.val, with initial bit of return value representing status
    if frame.val is zero, returns `0 end to represent an error state
    otherwise, returns `1 (n-1). *)
let decrement = fun frame ->
    match frame.val with
    | `End _ -> {frame | val=`0 end}
    | `1 xs -> {frame | val=`1`0 xs}
    | `0 xs -> (
        (* call decrement2 (decrement xs) *)
        {val=xs; stack=`Decrement {stack=`Decrement2 {stack=frame.stack}}}
    );
let decrement2 = fun frame ->
    match frame.val with
    | `1 xs_dec -> {frame | val=`1`1 xs_dec}
    (* when val represents an error, return it unchanged *)
    | `0 _ -> {frame | val=`0 end}
    (* this case isn't actually reachable, but is needed for type checking *)
    | `End _ -> {frame | val=`0 end}
    ;

(* add frame.val + (frame.ys << 1) *)
let add_shifted = fun frame ->
    match frame.val with
    (* this case isn't actually reachable, but is needed for type checking *)
    | `End _ -> {val=`0 frame.ys; stack=frame.stack}
    | `0 xs -> (
        (* call push0 (add {val=xs; y=ys}) *)
        {val=xs; stack=`Add {y=frame.ys; stack=`Push0 {stack=frame.stack}}}
    )
    | `1 xs -> (
        (* call push1 (add {val=xs; y=ys}) *)
        {val=xs; stack=`Add {y=frame.ys; stack=`Push1 {stack=frame.stack}}}
    );

(* add frame.val + frame.y *)
let add = fun frame ->
    match frame.y with
    (* when y=0, return frame.val unchanged *)
    | `End _ -> frame
    | `0 ys -> add_shifted {val=frame.val; ys=ys; stack=frame.stack}
    | `1 ys ->  (
        (* call add_shifted {val=increment frame.val; ys=ys} *)
        increment {val=frame.val; stack=`AddShifted {ys=ys; stack=frame.stack}}
    );

(* computes an iteration of the fibonacci calculations:
    fib_sub (n, a, b) -> (n-1, a+b, a) where a=frame.val*)
let fib_sub = fun frame -> decrement {val=frame.n; stack=`FibSub2 {a=frame.val; b=frame.b; stack=frame.stack}};

(* note that here, val is the "n" value rather than the "a" value *)
let fib_sub2 = fun frame ->
    match frame.val with
    (* this case isn't actually reachable, but is needed for type checking *)
    | `End _ -> {val=frame.a; stack=frame.stack}
    | `0 _ -> {val=frame.a; stack=frame.stack}
    | `1 n -> {val=frame.a; stack=`Add {y=frame.b; stack=`FibSub {n=n; b=frame.a; stack=frame.stack}}};

let tick = fun state ->
    match state.stack with
    | `Push0 frame -> push0 {frame | val=state.val}
    | `Push1 frame -> push1 {frame | val=state.val}
    | `Increment frame -> increment {frame | val=state.val}
    | `Decrement frame -> decrement {frame | val=state.val}
    | `Decrement2 frame -> decrement2 {frame | val=state.val}
    | `AddShifted frame -> add_shifted {frame | val=state.val}
    | `Add frame -> add {frame | val=state.val}
    | `FibSub frame -> fib_sub {frame | val=state.val}
    | `FibSub2 frame -> fib_sub2 {frame | val=state.val}
    (* if the computation is done, just return the state unchanged *)
    | `Done _ -> state
    ;

现在可以通过运行程序 256 次来测试它，这足以计算出前 12 个斐波那契数。

let tick2 = fun state -> tick (tick state);
let tick3 = fun state -> tick2 (tick2 state);
let tick4 = fun state -> tick3 (tick3 state);
let tick5 = fun state -> tick4 (tick4 state);
let tick6 = fun state -> tick5 (tick5 state);
let tick7 = fun state -> tick6 (tick6 state);
let tick8 = fun state -> tick7 (tick7 state);
let tick9 = fun state -> tick8 (tick8 state);

let fib9 = fun n ->
    (* set up the initial state to call fib_sub *)
    tick9 {val=`1 end; stack=`FibSub {n=n; b=`1 end; stack=`Done {}}};

第 12 个斐波那契数是 377，即二进制的 `1`0`0`1`1`1`1`0`1 end。

(* compute the 12th fibonacci number *)
let state = fib9 `0`0`1`1 end;
match state.stack with | `Done _ -> _;
(* the 12th fibonacci number is 377 = 0b101111001 *)
match state.val with | `1 x ->
    (match x with | `0 x ->
    (match x with | `0 x ->
    (match x with | `1 x ->
    (match x with | `1 x ->
    (match x with | `1 x ->
    (match x with | `1 x ->
    (match x with | `0 x ->
    (match x with | `1 x ->
    (match x with | `End _ -> _)))))))))

你可以在下面的演示中验证它都是在编译时计算出来的。改变最后输出断言中的任何数字都会导致编译时的类型错误。警告：编译这个程序可能相当慢。我选择了 256 个滴答，因为这在我的电脑上运行得相当好，但如果演示开始变得太慢，请尝试刷新页面。

演示

结论

现在我们已经将类型系统推向了极限，下周我将开始介绍如何添加显式类型注释。到目前为止，我已经避开了它们，因为这个系列的重要部分是类型推理，当你必须在多个地方更新所有的东西，并在手动类型注释语法中也处理它们时，向类型系统添加新的功能会更加复杂和烦人。但是，只是因为可以在没有类型注释的情况下写出整个程序，并不意味着这必然是个好主意，所以在“真实世界”的编程语言中支持类型注释是很重要的。