Bidirectional Checking [blog/lti/bidirectional]

    至此，我们已经完整地剖析了本文的第一项重点：局部类型参数合成。它通过一套由「变量消去」、「约束生成」和「参数计算」构成的、逻辑严密且完全可执行的算法，完美地解决了由细粒度多命题所引发的类型参数标注繁琐的问题，达成了引言中所述三条设计准则中的第一条。

    然而，我们的工具箱尚不完备。回顾引言中基于 ML 代码分析所提出的三条设计准则，仍有两项亟待解决：

    1. 高阶编程的便利性：如何推断匿名函数（如 fun[](x) x+1）中绑定变量 x 的类型？
    2. 纯函数式风格的支持：如何让大量的局部变量绑定（如 let x = ...）无需显式类型标注？

    局部类型参数合成机制，其信息流本质上是自下而上（bottom-up）的，它根据函数和参数的既有类型，向上推导出一个最佳的结果类型。这套机制，对于上述两个问题鞭长莫及，因为在类似 fun[](x) x+1 这样的表达式中，没有任何子结构能为 x 的类型提供信息。

    我们考虑一种在思想上与前者互补的、功能强大的局部推断技术。它不再仅仅依赖自下而上的信息综合，而是引入了一股自上而下（top-down）的信息流，让表达式所处的语境（context）来指导其内部的类型检查。这便是双向类型检查（Bidirectional Type Checking），其基本思想虽早已是编程语言社区的「民间共识」，并在一些基于属性文法的 ML 编译器中得以应用，本文将其在一个同时包含子类型化与非直谓多态的形式系统中进行严谨的公理化，并将其作为一种独立的局部推断方法，其威力出人意料地强大。

    两种模式：综合与检查

    1. 综合模式 (Synthesis Mode, $\Rightarrow$)

      • 在此模式下，类型信息自下而上传播。
      • 其目标是根据一个表达式的子表达式的类型，来计算（或「综合」）出该表达式自身的类型。
      • 这对应于传统的类型检查方式，适用于那些我们对其期望类型一无所知的上下文，例如在处理一个顶层表达式或一个应用节点的函数部分时。

    2. 检查模式 (Checking Mode, $\Leftarrow$)

      • 在此模式下，类型信息自上而下传播。
      • 其目标是验证（或「检查」）一个表达式是否拥有一个由其所处语境提供的「期望类型」（或者该期望类型的一个子类型）。
      • 当一个表达式所处的语境已经决定了它的类型时，便可切换至此模式。

    双向检查的精髓在于两种模式的灵活切换。一个典型的函数应用 f(e) 完美地展示了这一过程：类型检查器会先综合出函数 f 的类型，然后利用该类型提供的信息，切换模式去检查参数 e。

    1. Typing Rules [blog/lti/bidi_rules]

      本节是我们类型检查程序的最后一块拼图， 描述了整个双向类型检查的过程。

      变量规则 (Variable Rules)

      1. 综合 - 变量 (Synthesis-Var)

      $$ \frac{}{\Gamma \vdash x \Rightarrow \Gamma(x)} \quad (\text{S-Var}) $$

      这是变量的综合规则。如果要在综合模式下推导一个变量 $x$ 的类型，只需在当前的类型上下文 $\Gamma$ 中查找 $x$ 已经声明的类型 $\Gamma(x)$ 即可。这是最直接的类型推导形式：变量的类型就是它被定义时的类型。

      2. 检查 - 变量 (Checking-Var)

      $$ \frac{\Gamma \vdash \Gamma(x) \lt: T}{\Gamma \vdash x \Leftarrow T} \quad (\text{C-Var}) $$

      这是变量的检查规则。要检查变量 $x$ 是否符合预期的类型 $T$，我们需要先从上下文 $\Gamma$ 中查找到 $x$ 的实际类型 $\Gamma(x)$，然后验证这个实际类型 $\Gamma(x)$ 是否是预期类型 $T$ 的一个子类型 (subtype)。这里的子类型关系用 $\Gamma \vdash \Gamma(x) \lt: T$ 表示。

      函数抽象规则 (Function Abstraction Rules)

      3. 综合 - 抽象 (Synthesis-Abs)

      $$ \frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Rightarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Rightarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{S-Abs}) $$

      这是针对带有完整类型标注的函数抽象的综合规则。

      • 一个形式为 fun [X] (x:S) e 的函数，其类型参数 $\overline{X}$ 和值参数 $\overline{x}$ 的类型 $\overline{S}$ 都被明确标注了。
      • 规则的前提是，在将类型变量 $\overline{X}$ 和值变量及其类型 $\overline{x}:\overline{S}$ 加入到当前上下文 $\Gamma$ 后，我们可以综合出函数体 $e$ 的类型为 $T$。
      • 那么，整个函数表达式的类型就可以被综合为多态函数类型 $\forall \overline{X}. \overline{S} \rightarrow T$。

      4. 检查 - 无标注抽象 (Checking-Abs-Inf)

      $$ \frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}) e \Leftarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{C-Abs-Inf}) $$

      这是本节的核心规则之一，用于推断无标注匿名函数的参数类型。

      • 当我们在检查模式下处理一个没有值参数类型标注的函数 fun [X] (x) e 时，我们可以从预期的函数类型 $\forall \overline{X}. \overline{S} \rightarrow T$ 中获取信息。
      • 具体来说，我们可以从预期的类型中提取出参数类型 $\overline{S}$ 和返回类型 $T$。
      • 然后，我们将类型变量 $\overline{X}$ 和推断出的值参数类型 $\overline{x}:\overline{S}$ 加入上下文，并在这个新上下文中以检查模式验证函数体 $e$ 是否符合返回类型 $T$。如果满足，则整个无标注函数就通过了类型检查。
      • 注意：$\overline{X}$ 在这个系统下是无法省略的。

      5. 检查 - 有标注抽象 (Checking-Abs)

      $$ \frac{\Gamma, \overline{X} \vdash \overline{T} \lt: \overline{S} \quad \Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow R}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Leftarrow \forall \overline{X}. \overline{T} \rightarrow R} \quad (\text{C-Abs}) $$

      这是在检查模式下处理一个带有类型标注的函数的规则。

      • 当一个有标注的函数 fun [X] (x:S) e 需要被检查是否符合某个预期类型 $\forall \overline{X}. \overline{T} \rightarrow R$ 时：
      • 首先，由于函数类型的参数类型是逆变 (contravariant) 的，我们需要检查预期类型中的参数类型 $\overline{T}$ 是否是函数实际标注的参数类型 $\overline{S}$ 的子类型。
      • 随后我们在扩展后的上下文中，以检查模式验证函数体 $e$ 是否符合预期的返回类型 $R$。

      函数应用规则 (Function Application Rules)

      6. 综合 - 应用 (Synthesis-App)

      $$ \frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow [\overline{T}/\overline{X}]R} \quad (\text{S-App}) $$

      这是函数应用的综合规则。

      • 首先，在综合模式下推断出函数 $f$ 的类型为多态函数 $\forall \overline{X}. \overline{S} \rightarrow R$。
      • 然后，我们将提供的具体类型参数 $\overline{T}$ 替换掉类型变量 $\overline{X}$，得到参数的预期类型 $[\overline{T}/\overline{X}]\overline{S}$。
      • 接下来，我们切换到检查模式，验证实际参数 $\overline{e}$ 是否符合这个预期类型。
      • 如果检查通过，整个应用表达式的类型就被综合为将 $\overline{T}$ 代入后的返回类型 $[\overline{T}/\overline{X}]R$。

      7. 检查 - 应用 (Checking-App)

      $$ \frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash [\overline{T}/\overline{X}]R \lt: U \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow U} \quad (\text{C-App}) $$

      这是函数应用的检查规则。它与综合规则非常相似，但增加了一个最终的子类型检查。

      • 前两个步骤和 S-App 一样：综合 $f$ 的类型，并检查参数 $\overline{e}$。
      • 在计算出应用的实际返回类型 $[\overline{T}/\overline{X}]R$ 后，我们还必须检查这个实际返回类型是否是整个应用表达式的预期类型 $U$ 的子类型。

      结合双向检查和类型参数综合的规则

      8. 综合 - 应用 - 推断规格 (Synthesis-App-InfAlg)

      $$ \frac{ \begin{array}{ccc} \Gamma \vdash f : \forall \overline{X}.\overline{T} \to R & \Gamma \vdash \overline{e} : \overline{S} & |\overline{X}| > 0 \\ \emptyset \vdash_X \overline{S} \lt: \overline{T} \Rightarrow \overline{D} & C = \bigwedge \overline{D} & \sigma = \sigma_{CR} \end{array} }{ \Gamma \vdash f(\overline{e}) \Rightarrow \sigma R } \quad (\text{S-App-InfAlg}) $$

      这是在综合模式下推断函数应用中缺失的类型参数的规则，这正是上文「类型参数计算」一节导出的规则。

      9. 检查 - 应用 - 推断规格 (Checking-App-InfAlg)

      $$ \frac{\begin{matrix} \Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{T} \rightarrow R \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S} \quad |\overline{X}| \gt 0 \\ \emptyset \vdash \overline{S} \lt: \overline{T} \Rightarrow C \quad \emptyset \vdash R \lt: V \Rightarrow D \quad \sigma \in \bigwedge C \wedge D \end{matrix}}{\Gamma \vdash f(\overline{e}) \Leftarrow V} \quad (\text{C-App-InfAlg}) $$

      这是 App-InfAlg 规则的检查版本。

      • 它描述了编译器如何通过约束求解来找到合适的类型参数。
      • 步骤如下：
        1. 综合函数 $f$ 和参数 $\overline{e}$ 的类型。
        2. 生成两组约束：
          • 第一组约束 $C$ 来自于要求参数的实际类型 $\overline{S}$ 必须是函数期望的参数类型 $\overline{T}$ 的子类型。
          • 第二组约束 $D$ 来自于要求函数的实际返回类型 $R$ 必须是整个表达式的预期类型 $V$ 的子类型。
        3. 求解这两组约束的合取（$\bigwedge C \wedge D$）。如果能找到一个解（一个替换 $\sigma$），那么类型检查就成功了。 因为这是一条检查规则，因而我们只需要知道解的存在性即可，甚至不需要求解它。

      顶类型和底类型

      10. 检查 - 顶类型 (Checking-Top)

      $$ \frac{\Gamma \vdash e \Rightarrow T}{\Gamma \vdash e \Leftarrow \top} \quad (\text{C-Top}) $$

      这是一个从检查模式切换到综合模式的规则。如果一个表达式 $e$ 被要求检查是否符合顶类型 $\top$，由于任何类型都是 $\top$ 的子类型，这个检查总是会成功。$\top$ 类型没有提供任何有用的约束信息，所以规则允许我们直接切换到综合模式，推导出 $e$ 的具体类型 $T$ 即可。

      11. 综合 - 应用 - 底类型 (Synthesis-App-Bot)

      $$ \frac{\Gamma \vdash f \Rightarrow \bot \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow \bot} \quad (\text{S-App-Bot}) $$

      这是处理函数类型为 $\bot$ (底类型) 时的特殊情况。$\bot$ 类型代表那些永不返回的表达式（如抛出异常）。

      • 如果一个函数 $f$ 的类型被推导为 $\bot$，那么无论它被应用于何种参数，整个应用表达式的结果类型也是 $\bot$。
      • 这是因为 $\bot$ 是所有类型的子类型，包括所有函数类型。因此，一个类型为 $\bot$ 的表达式可以被当作任何函数来应用。

      12. 检查 - 应用 - 底类型 (Checking-App-Bot)

      $$ \frac{\Gamma \vdash f \Rightarrow \bot \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow R} \quad (\text{C-App-Bot}) $$

      这是在检查模式下，函数类型为 $\bot$ 的情况。

      • 同样，如果函数 $f$ 的类型为 $\bot$，那么应用的结果类型也是 $\bot$。
      • 因为 $\bot$ 是任何类型 $R$ 的子类型，所以这个检查总是成功的。

      最后的实现即是落到 synthesis 和 check 两个关键函数上， 这是本文最重要的一个练习， 强烈建议读者自己尝试实现这两个函数，来体会双向检查的精妙之处， 并从中学习将类型规则转化为代码的技巧。

      2. Bidirectional Typing Code [blog/lti/bidi_code]

        pub fn synthesis(self : Expr, gamma : Context) -> Type raise {
  match self {
    EVar(v) => gamma[v]
    EAbs(xs, vs, body) => {
      let ctx = gamma.append_vars(xs).append_binds(vs)
      let body_ty = body.synthesis(ctx)
      TyFun(xs, vs.map(xS => xS.1), body_ty)
    }
    EAppI(f, e) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot) else { TyBot }
      guard t is TyFun(xs, t, r) else { raise SynthesisError }
      // guard !xs.is_empty() else { raise NotFound }
      let es = e.map(_.synthesis(gamma))
      let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set::new()))
      let sigma = meets(cs).solve(r)
      sigma.map(s => r.apply_subst(s)).or_error(SynthesisError)
    }
    EApp(f, ty, e) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot) else { TyBot }
      guard t is TyFun(xs, ss, r) else { raise SynthesisError }
      let subst = mk_subst(xs, ty)
      e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
      r.apply_subst(subst)
    }
    _ => raise SynthesisError
  }
}

pub fn check(self : Expr, ty : Type, gamma : Context) -> Unit raise {
  match (self, ty) {
    (_, TyTop) => ()
    (EVar(v), t) => {
      let gx = gamma[v]
      guard gx.subtype(t) else { raise CheckError }
    }
    (EAbs(xs, vs, body), TyFun(xsP, t, r)) if xs == xsP => {
      let ctx = gamma.append_vars(xs)
      guard t.zip(vs.map(xS => xS.1)).iter().all(z => z.0.subtype(z.1)) else {
        raise CheckError
      }
      body.check(r, ctx.append_binds(vs))
    }
    (EAbsI(xs, vs, body), TyFun(xsP, ss, t)) if xs == xsP &&
      ss.length() == vs.length() =>
      body.check(t, gamma.append_vars(xs).append_binds(vs.zip(ss)))
    (EAppI(f, e), u) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot && u is TyBot) else { () }
      guard f.synthesis(gamma) is TyFun(xs, t, r) else { raise CheckError }
      guard !xs.is_empty() else { () }
      let es = e.map(_.synthesis(gamma))
      let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set::new()))
      let d = { l: r, r: u }.generate(xs, Set::new())
      guard meets(cs).meet(d).satisfiable() else { raise CheckError }
    }
    (EApp(f, ty, e), u) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot && u is TyBot) else { () }
      guard t is TyFun(xs, ss, r)
      let subst = mk_subst(xs, ty)
      e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
      guard r.apply_subst(subst).subtype(u) else { raise CheckError }
    }
    _ => raise CheckError
  }
}

        最后一个关键目标是局部变量绑定的设计， 这要求我们引入新的语法结构 ELet，但其规则是显然的：

        $$ \frac{\Gamma \vdash e \Rightarrow S \quad \Gamma, x:S \vdash b \Rightarrow T}{\Gamma \vdash \textbf{let } x = e \textbf{ in } b \Rightarrow T} \quad (\text{S-Let}) $$

        $$ \frac{\Gamma \vdash e \Rightarrow S \quad \Gamma, x:S \vdash b \Leftarrow T}{\Gamma \vdash \textbf{let } x = e \textbf{ in } b \Leftarrow T} \quad (\text{C-Let}) $$

        实现留作习题。