language]

在严谨地探讨类型推导这一议题之前，我们必须首先清晰地界定其推断的目标——一个无歧义的、被完全标注的内核语言（internal language）。此语言是编译器内部的「真实」表达，亦是程序员书写的、允许省略标注的外部语言（external language）所要翻译成的最终形式。本文所用的内核语言，源自 Cardelli 与 Wegner 提出的，融合了子类型化与非论域性多态的著名演算 System $F_\leq$，但在此基础上我们增设了 $\bot$ (Bottom) 类型，为了保证上确界和下确界的存在，这种代数结构的完备性，是后续章节中约束求解算法得以简洁、确定地运行的根本保障。此外它也可以被用作那些永不返回的表达式（如抛出异常的函数）的结果类型，我们先定义形式语言如下（注：横线是序列记号 $\overline{X} = X_1, X_2, \dots, X_n$，类似的，$\overline{x} : \overline{T} = x_1 : T_1, \dots, x_n : T_n$）：

$$ \begin{array}{ll} T ::= X & \text{type variable} \\ \quad~\mid~ \top & \text{maximal type} \\ \quad~\mid~ \bot & \text{minimal type} \\ \quad~\mid~ \forall \overline{X} . \overline{T} \rightarrow T & \text{function type} \\[1em] e ::= x & \text{variable} \\ \quad~\mid~ \text{fun}[ \overline{X} ]\, ( \overline{x} : \overline{T} )\, e & \text{abstraction} \\ \quad~\mid~ e[ \overline{T} ]\, ( \overline{e} ) & \text{application} \\[1em] \Gamma ::= \bullet & \text{empty context} \\ \quad~\mid~ \Gamma, x : T & \text{variable binding} \\ \quad~\mid~ \Gamma, X & \text{type variable binding} \end{array} $$

我们可将上面的形式语言简单翻译到下面的 MoonBit 代码，其中 Var 是类型变量的实现：

pub(all) enum Type {
  TyVar(Var)
  TyTop
  TyBot
  TyFun(Array[Var], Array[Type], Type)
} derive(Eq)

pub(all) enum Expr {
  EVar(Var)
  EApp(Expr, Array[Type], Array[Expr])
  EAbs(Array[Var], Array[(Var, Type)], Expr)
}

1. Subtyping Relation [blog/lti/subtype]

子类型关系，记作 $S \lt: T$（读作 $S$ 是 $T$ 的一个子类型），是本形式系统的核心。它定义了类型之间的一种「可替换性」：凡是需要类型 $T$ 的地方，都可以安全地使用一个类型为 $S$ 的项来代替。

与许多理论文献中的定义不同，本文特意选择了一种算法化（algorithmic）的方式来呈现子类型关系。这意味着，定义中仅包含一组最核心的、可直接用于实现判定的规则，而像传递性（transitivity）这样通常作为公理的性质，在此系统中则成为了可被证明的引理。这种风格使得定义本身更接近于一个类型检查算法的规约：

$$ \begin{array}{ll} X \lt: X & \text{(S-Refl)} \\[1em] T \lt: \top & \text{(S-Top)} \\[1em] \bot \lt: T & \text{(S-Bot)} \\[1em] \dfrac{ \overline{T} \lt: \overline{R} \quad S \le: U }{ \forall \overline{X}. \overline{R} \rightarrow S \lt: \forall \overline{X}. \overline{T} \rightarrow U } & \text{(S-Fun)} \end{array} $$

其中 $\overline{T} \lt: \overline{R}$ 成立当且仅当 $\text{len}(T) = \text{len}(S) \land \forall 1 \leq i \leq \text{len}(S). S_i \lt: T_i$。 S-Fun 规则体现了函数类型子类型化的核心特征：在参数类型上是逆变（contravariant）的（子类型关系的箭头方向反转），而在返回类型上是协变（covariant）的（子类型关系箭头方向保持不变）。读者可以自己尝试一下将上文的形式语言翻译到 MoonBit 的一个谓词函数，或参考下面折叠起来的代码片段。

1.1. Solution [blog/lti/subtype_code]

/// l <: r
struct Subtype {
  l : Type
  r : Type
}

pub fn subtype(self : Subtype) -> Bool {
  match (self.l, self.r) {
    (TyVar(v1), TyVar(v2)) => v1 == v2
    (_, TyTop) => true
    (TyBot, _) => true
    (TyFun(xs1, r, s), TyFun(xs2, t, u)) if xs1 == xs2 =>
      subtypes(t, r) && { l: s, r: u }.subtype()
    _ => false
  }
}

为了支持后续的约束求解算法，系统必须能计算任意两个类型的最小上界（join, 记作 $\lor$）和最大下界（meet, 记作 $\land$）。得益于 $\bot$ 和 $\top$ 的存在，这两个运算在本系统中是全函数（total functions），即对于任意一对类型，其界都必然存在。下面我们给出这两个运算的定义：

最小上界 $S \vee T$
- 若 $S \lt: T$，则结果为 $T$。
- 若 $T \lt: S$，则结果为 $S$。
- 若 $S$ 和 $T$ 分别为 $\forall\overline{X}.\overline{V} \to P$ 和 $\forall\overline{X}.\overline{W} \to Q$，则结果为 $\forall\overline{X}.(\overline{V} \wedge \overline{W}) \to (P \vee Q)$。
- 在其他所有情况下，结果为 $\top$
最大下界 $S \wedge T$
- 若 $S \lt: T$，则结果为 $S$。
- 若 $T \lt: S$，则结果为 $T$。
- 若 $S$ 和 $T$ 分别为 $\forall\overline{X}.\overline{V} \to P$ 和 $\forall\overline{X}.\overline{W} \to Q$，则结果为 $\forall\overline{X}.(\overline{V} \vee \overline{W}) \to (P \wedge Q)$。
- 在其他所有情况下，结果为 $\bot$

通过简单的结构归纳法可以证明，这两个运算满足以下性质：

$S \vee T$ 和 $S \wedge T$ 分别是 $S$ 和 $T$ 的最小上界和最大下界。
$S \lt: U$ 且 $T \lt: U$ 则 $S \vee T \lt: U$
$U \lt: S$ 且 $U \lt: T$ 则 $U \lt: S \wedge T$

这里同样鼓励读者自己进行代码翻译，答案可展开下面的代码片段。

1.2. Solution [blog/lti/subtype_code2]

在 MoonBit 代码中我们将 $S \vee T$ 实现为 s | t，将 $S \wedge T$ 实现为 s & t。这两个运算符的定义如下：

impl BitAnd for Type with land(s, t) {
  match (s, t) {
    (TyFun(xs1, v, p), TyFun(xs2, w, q)) if xs1 == xs2 => {
      guard v.length() == w.length() else { TyBot }
      TyFun(xs1, v.zip(w).map(z => z.0 | z.1), p & q)
    }
    (s, t) if s.subtype(t) => s
    (s, t) if t.subtype(s) => t
    _ => TyBot
  }
}

impl BitOr for Type with lor(s, t) {
  match (s, t) {
    (TyFun(xs1, v, p), TyFun(xs2, w, q)) if xs1 == xs2 => {
      guard v.length() == w.length() else { TyTop }
      TyFun(xs1, v.zip(w).map(z => z.0 & z.1), p | q)
    }
    (s, t) if s.subtype(t) => t
    (s, t) if t.subtype(s) => s
    _ => TyTop
  }
}