对于初次接触编程语言理论的读者而言，文中遍布的数学符号与推导规则或许会显得有些陌生和令人生畏。 请不必担忧。这些形式化工具并非为了故作高深，恰恰相反， 它们是为了达到自然语言难以企及的精确性（precision）与无歧义性（unambiguity）。 本节将提供一份阅读这些规则的简单指南，熟悉的读者可以直接跳过。

读者可以将这些规则，看作是一门编程语言最根本的「物理定律」。它们以一种极为严谨的方式， 定义了什么样的程序是结构良好、有意义的，而什么样的程序则不是。

本文中的大多数规则，都呈现为如下的结构： $$\frac{\text{前提}_1 \quad \text{前提}_2 \quad ...}{\text{结论}} \quad (\text{规则名称})$$ 这条长长的横线，是理解一切的核心。

• 横线上方：前提（Premises）
  • 这里列出的是一组条件或假设。
  • 只有当所有前提都得到满足时，这条规则才能被激活或使用。
• 横线下方：结论（Conclusion）
  • 这是在所有前提都满足后，我们能够推导出的新事实。
• 右侧括号：规则名称 (Rule Name)
  • 这只是为了方便我们引用和讨论，给规则起的一个名字，如 Var 或 App。

在规则的前提与结论中，您会反复看到一种形如 $\Gamma \vdash e : T$ 的核心判断（judgment）。让我们来拆解它的每一个符号：

• $\Gamma$ (Gamma)：这是上下文（Context）。它代表了我们进行推导时，所有已知的背景信息或假设。通常，它记录了变量已经被赋予的类型，例如：$x : \mathbb{Z},\ f : \mathrm{Bool} \to \mathrm{Bool}$。您可以把它看作是「在…的环境下」或「已知…」。
• $\vdash$ (Turnstile)：这个符号读作「推导出」或「证明」。它是上下文与待证论断之间的分隔符。
• $e$：这是项（Term），即我们正在分析的那段程序代码。它可以是一个简单的变量 $x$，一个函数 $\mathsf{fun}(x)\ x + 1$，或是一个复杂的表达式。
• $:$ 表示「拥有类型」（has type）。
• $T$：这是类型（Type），例如 $\mathbb{Z}$、$\mathrm{Bool}$、$\mathrm{String} \to \mathbb{Z}$ 等。

将它们组合在一起，$\Gamma \vdash e : T$ 这整个判断的直白解读就是：「在上下文 $\Gamma$ 所提供的已知条件下，我们可以推导出（或证明），程序项 $e$ 拥有类型 $T$。」

在放弃了对「完全类型推断」的追求之后，一个至关重要的问题便浮现出来：一个「部分」类型推断算法，其推断能力需要达到何种程度，才算是「足够」？一个极具实践智慧的回答：一个好的部分类型推断算法，其核心使命在于消除那些既普遍又愚蠢的类型标注。

此处的「愚蠢」与「合理」相对。「合理的」标注，如顶级函数定义中对其参数的类型声明，通常能作为有价值的、且经由编译器检查的文档，帮助人们理解代码。「愚蠢的」标注则恰恰相反，它们徒增代码的冗余，却几乎不提供任何有用的信息。可以想见，在一个完全显式类型的语言中，任何人都不会愿意去书写或阅读 cons[Int](3, nil[Int]) 中那两个多余的 Int 标注。

Pierce 对十几万行 ML 代码的调研，揭示了三种最主要的「愚蠢标注」来源：

• 多态实例化：在所测量的代码中，类型应用（即对多态函数的实例化）的现象无处不在，平均来看，每三行代码中就至少出现一次。这些在多态函数调用点插入的类型参数，几乎没有任何文档价值，纯属语法上的累赘。
• 匿名函数定义：在类似 map(list, fun(x) x+1) 这样的上下文中，为匿名函数的参数 x 补上类型标注，只会掩盖其核心逻辑，实为一种不必要的干扰。
• 局部变量绑定 (Let): 为这些生命周期短暂的中间变量一一标注类型，显然是繁琐且意义不大的。

基于上述的定量观察，我们可以勾画出一个「足够」的部分类型推断算法的轮廓：

1. 它必须能够推断出多态函数应用中的类型参数。与此同时，要求程序员为顶级函数或相对稀少的局部函数提供显式标注，则是完全可以接受的，因为这些标注本身就是有益的文档。
2. 为了使高阶编程更加便捷，算法应当能够推断匿名函数参数的类型，尽管这并非绝对必要。
3. 局部变量绑定通常不应要求显式的类型标注。

在严谨地探讨类型推导这一议题之前，我们必须首先清晰地界定其推断的目标——一个无歧义的、 被完全标注的内核语言（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)
}

/// 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
  }
}

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
  }
}

在定义了类型与子类型关系之后，我们便可以给出内核语言的类型定则。这些规则定义了类型判断（typing judgment）的形式 $\Gamma \vdash e : T$，意为「在上下文 $\Gamma$ 中，项 $e$ 拥有类型 $T$ 」。

与子类型关系的定义一脉相承，这里的类型定则同样采用了一种算法化的呈现方式。且省略了传统类型系统中常见的包容规则（subsumption，若 $e$ 的类型为 $S$ 且 $S \lt: T$，则 $e$ 的类型亦可为 $T$）。

通过省略此规则，本系统为每一个可被类型化的项，都计算出一个唯一的、最小的类型，作者称之为该项的显式类型（manifest type）。这一设计选择，并不改变语言中可被类型化的项的集合，而只是确保了任何一个项的类型推导路径都是唯一的。这极大地增强了系统的可预测性。

核心定则 (Core Rules)

• 变量 (Variable)

  $$ \frac{}{\Gamma \vdash x : \Gamma(x)} \quad (\text{Var}) $$

• 抽象 (Abstraction) 此规则统一了传统的项抽象与类型抽象。

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

  若想要求解 $\mathbf{fun}[\overline{X}] (\overline{x}:\overline{S})$ 的类型，必须在上下文 $\Gamma$ 中添加类型变量 $\overline{X}$ 和值变量 $\overline{x}:\overline{S}$ 的绑定。然后，在这个扩展的上下文中，推导函数体 $e$ 的类型为 $T$。最终，整个函数的类型便是 $\forall \overline{X}.\overline{S} \to T$。

• 应用 (Application) 此规则同样统一了传统的项应用与多态应用。它首先推导函数 f 的类型，然后验证所有实际参数（包括类型参数与项参数）是否与函数的签名相符。 这里的要求更宽松了一些：只要实际参数的类型满足参数类型的子类型关系即可，而不需要完全匹配。

  $$ \frac{\Gamma \vdash f : \forall \overline{X} . \overline{S} \to R \quad \Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f[\overline{T}] (\overline{e}) : [\overline{T}/\overline{X}]R} \quad (\text{App}) $$

  其中，记法 $\Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}$ 是一个缩写，表示 $\Gamma \vdash \overline{e} \lt: \overline{U}$，然后验证 $\overline{U} \lt: [\overline{T}/\overline{X}]\overline{S}$。最终，整个应用表达式的结果类型，是通过将实际类型参数 $\overline{T}$ 代入函数原始返回类型 $R$ 中得到的。

  4.1. Type Parameter Substitution [blog/lti/subst_code]

  这里出现了一个新的记号 $[\overline{T}/\overline{X}]R$， 它表示将类型参数 $\overline{X}$ 替换为实际类型 $\overline{T}$ 后的结果类型。 这个记号在后续的代码中会频繁出现。 下面的代码定义 mk_subst 函数，用来生成一个类型替换映射， 还有一个 apply_subst 函数可以将这个映射应用到一个具体类型上。 $[\overline{T}/\overline{X}]R$ 就是通过 $\text{apply\_subst}(\text{mk\_subst}(\overline{X},\overline{T}), R)$ 得到的。

  pub fn mk_subst(vars : Array[Var], tys : Array[Type]) -> Map[Var, Type] raise {
    guard vars.length() == tys.length() else { raise ArgumentLengthMismatch }
    Map::from_array(vars.zip(tys))
  }
  
  pub fn apply_subst(self : Type, subst : Map[Var, Type]) -> Type {
    match self {
      TyVar(v) => subst.get(v).unwrap_or(self)
      TyTop | TyBot => self
      TyFun(xs, ss, t) => {
        let fs = subst.iter().filter(kv => !xs.contains(kv.0)) |> Map::from_iter
        let new_ss = ss.map(s => s.apply_subst(fs))
        let new_t = t.apply_subst(fs)
        TyFun(xs, new_ss, new_t)
      }
    }
  }
  

• Bot 应用 (Bot Application) $\bot$ 类型的引入，要求我们补充一条特殊的应用规则，以维护系统的类型安全（type soundness）。 由于 $\bot$ 是任何函数类型的子类型，一个类型为 $\bot$ 的表达式应当可以被应用于任何合法的参数，而不会产生类型错误。

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

  此规则规定，当一个类型为 $\bot$ 的项被应用时，无论参数为何，整个表达式的结果类型也是 $\bot$，这正是我们能给出的最精确（即最小）的结果类型。

这些规则共同保证了本类型系统的一个关键性质，即显式类型的唯一性（Uniqueness of Manifest Types）：若 $\Gamma \vdash e : S$ 且 $\Gamma \vdash e : T$，那么必有 $S=T$。

截至目前，我们已经定义了内核语言的类型规则， 但是距离我们的目标还有很大距离：核心语言要求我们做出很多注解， 包括多态实例化时需要提供的类型参数，因为这在代码中非常常见，因此这是我们本节首要解决的痛点。

此即局部类型参数合成（Local Type Argument Synthesis）的目标：允许程序员在调用多态函数时，安全地省略其类型参数，写成 $\text{id}(3)$ 而不是 $\text{id}[\mathbb{Z}](3)$ 的形式。省略类型参数后，一个核心挑战随之而来：对于一个给定的应用，如 $\text{id} (x)$（其中 $x : \mathbb{Z}$，且 $\mathbb{Z} \lt: \mathbb{R}$），通常存在多种合法的类型参数实例化方案，例如这里的 $\text{id} [\mathbb{Z}](x)$ 或 $\text{id} [\mathbb{R}](x)$。我们必须确立一个清晰的标准来做出选择：选择能为整个应用表达式带来最精确（即最小）结果类型的类型参数。在 $\text{id} (x)$ 的例子中，由于 $\text{id} [\mathbb{Z}](x)$ 的结果类型 $\mathbb{Z}$ 是 $\text{id} [\mathbb{R}](x)$ 的结果类型 $\mathbb{R}$ 的一个子类型，前者显然是更优、更具信息量的选择。

然而，这种基于「最佳结果类型」的局部策略并非万能。在某些情况下，「最佳」解可能并不存在。例如，假设一个函数 $f$ 的类型为 $\forall X. () \to (X \to X)$。对于应用 $f()$，$f[\mathbb{Z}]()$ 和 $f[\mathbb{R}]()$ 都是合法的补全，其结果类型分别为 $\mathbb{Z} \to \mathbb{Z}$ 和 $\mathbb{R} \to \mathbb{R}$。这两种函数类型在子类型关系下是不可比较的，因此不存在一个唯一的最小结果类型。在这种情况下，局部合成宣告失败。

回顾之前的核心语言定义，我们要求 application 构造的形式为 $e[\overline{T}](\overline{e})$， 也就是说我们手动填写了类型参数 $\overline{T}$，规则 App 能够根据此参数为应用表达式计算出结果类型。 现在我们为了语言更简单易用，允许省略类型参数 $\overline{T}$，现在我们更新语言的构造：

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

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

这里加入了新的表达式结构 EAppI(Expr, Array[Expr])，对应我们的省略类型参数形式。 （为了后文叙述方便，这里也增加了后文会用到的 EAbsI 构造） 现在我们需要一条新的规则：

$$ \frac{\text{magic we don't know}}{\Gamma \vdash f (\overline{e}) : [\overline{T}/\overline{X}]R} \quad (\text{App-Magic}) $$

身为人类我们可以用直觉来制定规则，甚至设计出一些无法写成代码的声明式规则， 精确地定义「何为一次正确的、最优的类型参数推断」：

$$ \frac{ \begin{array}{l} \Gamma \vdash f : \forall \overline{X}. \overline{T} \to R \qquad \exists \overline{U} \\ \Gamma \vdash \overline{e} : \overline{S} \qquad |\overline{X}| > 0 \qquad \overline{S} \lt: [\overline{U}/\overline{X}]\overline{T} \\ \text{forall} (\overline{V}). \overline{S} \lt: [\overline{V}/\overline{X}]\overline{T} \implies [\overline{U}/\overline{X}]R \lt: [\overline{V}/\overline{X}]R \end{array} }{\Gamma \vdash f(\overline{e}) : [\overline{U}/\overline{X}]R} \quad (\text{App-InfSpec}) $$

此处我们使用存在量化 $\exists \overline{U}$，并且要求 $\overline{U}$ 满足很多条件。 例如 $\overline{S} \lt: [\overline{U}/\overline{X}]\overline{T}$ 为合法性约束。 它规定我们所选定的类型参数 $\overline{U}$ 必须是合法的。 所谓合法，即指将 $\overline{U}$ 代入函数的形式参数类型 $\overline{T}$ 后，实际参数的类型 $\overline{S}$ 必须是其子类型。 更重要的是最后一条 $\text{forall} (\overline{V}). \overline{S} \lt: [\overline{V}/\overline{X}]\overline{T} \implies [\overline{U}/\overline{X}]R \lt: [\overline{V}/\overline{X}]R$ 规则， 它要求我们对所有可能的类型参数元组 $\overline{V}$ 进行考量， 这可以转化为对潜在无限空间 $\overline{V}$ 进行搜索的过程，是典型的非构造性描述， 我们无法在计算机中实现它。

至此，我们的目标已经明确：我们需要一个真正可执行的算法，其结果与 (App-InfSpec) 一致， 但不需要我们进行非构造性的搜索和回溯。这正是「约束生成」这一步骤所要扮演的角色。 它的设计动机，源于对问题本身的一次精妙的视角转换。

与其将类型参数推断视为一个在无限可能性中「寻找并验证最优解」的搜索问题， 不妨将其重构为一个类似于解代数方程的「求解未知数边界」的问题。 我们不再去猜测类型参数 $\overline{X}$ 可能是什么， 而是通过分析子类型关系本身，去推导出 $\overline{X}$ 必须满足的条件。

观察到我们的规则存在子类型约束，不妨考虑一般情况 $S \lt: T$， 这本身就隐含着对其构成部分（包括其中的未知变量）的约束。 若 $X$ 是 $T$ 中的一个未知变量，那么 $S$ 的结构就必然会限制 $X$ 可能的形态。 我们的算法，正是要将这种隐含的、结构上的限制，转化为一组显式的、关于 $X$ 上下界的断言。

然而，在系统性地提取这些约束之前，我们必须首先面对一个与变量作用域相关的、 虽属前期准备但至关重要的挑战。若不妥善处理，我们生成的约束本身就可能是非良构的。 这一挑战，催生了算法的第一个具体操作步骤：变量消去。

pub fn promotion(self : Type, v : Set[Var]) -> Type {
  match self {
    TyFun(xs, ss, t) => {
      let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
      let us = ss.map(_.demotion(vP))
      let r = t.promotion(vP)
      guard xs.iter().all(x => !v.contains(x))
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyTop
    _ => self
  }
}

pub fn demotion(self : Type, v : Set[Var]) -> Type {
  match self {
    TyFun(xs, ss, t) => {
      let vP = v.iter().filter(x => !xs.contains(x)) |> Set::from_iter
      let us = ss.map(_.demotion(vP))
      let r = t.demotion(vP)
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyBot
    _ => self
  }
}

约束生成是局部类型参数合成算法的核心引擎。 在通过变量消去确保了作用域安全之后， 此步骤的使命是将一个子类型判定问题——例如， $S \lt: T$，其中 $S$ 或 $T$ 中含有待定的类型参数 $\overline{X}$ 转化为一组对这些未知参数 $\overline{X}$ 的显式约束。 现在我们形式化地定义代码中的约束具体是什么结构：

• 约束 (Constraint)：在本系统中，每一个约束都具有形式 $S_i \lt: X_i \lt: T_i$，它为单个未知类型变量 $X_i$ 同时指定了一个下界 (lower bound) $S_i$ 和一个上界 (upper bound) $T_i$ 。

• 约束集 (Constraint Set)：一个约束集 $C$ 是关于一组未知变量 $\overline{X}$ 到其对应约束的有限映射（在代码中可以实现为一个 Hash Map）。约束集的一个关键不变量是，其中任何约束的上下界（$S_i, T_i$）都不能含有任何待定的未知变量（即 $\overline{X}$ 中的变量）或任何需要被消去的局部变量（即 $V$ 中的变量）。空约束集 ($\emptyset$) 代表最无限制的约束，相当于为每一个 $X_i$ 指定了约束 $\bot \lt: X_i \lt: \top$ 。

• 约束集的交 ($\wedge$) 定义为两个约束集 $C$ 和 $D$ 的交集，是通过将其对同一个变量的约束进行合并得到的。新的下界是原下界的最小上界（join, $\vee$），而新的上界是原上界的最大下界（meet, $\wedge$） 。

struct Constraints(Map[Var, Subtype])

pub fn Constraints::empty() -> Constraints {
  Constraints(Map::new())
}

pub fn meet(self : Constraints, other : Constraints) -> Constraints {
  union_with(self.inner(), other.inner(), (l, r) => {
    let { l: l1, r: r1 } = l
    let { l: l2, r: r2 } = r
    { l: l1 & l2, r: r1 | r2 }
  })
}

pub fn meets(c : Array[Constraints]) -> Constraints {
  c.iter().fold(init=Constraints::empty(), Constraints::meet)
}

约束生成过程被形式化为一个推导关系 $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$，其意为：在需要回避的变量集为 $V$ 的条件下，为使 $S \lt: T$ 成立，关于未知变量 $\overline{X}$ 需满足的（最弱）约束集是 $C$，这个 $C$ 可以被视为是该推导关系的输出。

算法由一组递归规则定义，其中关键规则如下（注：我们始终假定 $\overline{X} \cap V = \emptyset$）：

• 平凡情况 (Trivial Cases)：当子类型关系的上界是 $\top$ 或下界是 $\bot$ 时，该关系无条件成立，因此生成一个空约束集 $\emptyset$ 。
• 上界约束 (Upper Bound Constraint)：当需要判定 $Y \lt: S$（其中 $Y \in \overline{X}$ 是未知变量，而 $S$ 是已知类型）时，算法会为 $Y$ 生成一个上界约束。 $$ \frac{Y \in \overline{X} \quad S \Downarrow^V T \quad \text{FV}(S) \cap \overline{X} = \emptyset}{V \vdash_{\overline{X}} Y \lt: S \Rightarrow \{ \bot \lt: Y \lt: T \}} \quad (\text{CG-Upper}) $$ 注意，这里利用了前述的变量消去操作（$S \Downarrow^V T$）来确保上界 $T$ 本身是良构的。
• 下界约束 (Lower Bound Constraint)：对偶地，当需要判定 $S \lt: Y$ 时，算法为 $Y$ 生成一个下界约束。 $$ \frac{Y \in \overline{X} \quad S \Uparrow^V T \quad \text{FV}(S) \cap \overline{X} = \emptyset}{V \vdash_{\overline{X}} S \lt: Y \Rightarrow \{ T \lt: Y \lt: \top \}} \quad (\text{CG-Lower}) $$
• 函数类型 (Function Type)：当比较两个函数类型时，算法递归地处理其参数和返回类型，并将生成的子约束集合并。 $$ \frac{V \cup \{\overline{Y}\} \vdash_{\overline{X}} \overline{T} \lt: \overline{R} \Rightarrow \overline{C} \quad V \cup \{\overline{Y}\} \vdash_{\overline{X}} S \lt: U \Rightarrow D}{V \vdash_{\overline{X}} \forall \overline{Y}.\overline{R} \to S \lt: \forall \overline{Y}.\overline{T} \to U \Rightarrow (\bigwedge \overline{C}) \wedge D} \quad (\text{CG-Fun}) $$ 这里，通过对子约束集取交集 ($\wedge$)，实现了约束的累积。

/// Pre-condition: xs and v are disjoint sets of variables.
pub fn generate(
  self : Subtype,
  xs : Array[Var],
  v : Set[Var],
) -> Constraints raise {
  match (self.l, self.r) {
    (_, TyTop) | (TyBot, _) => Constraints::empty()
    (TyVar(y1), TyVar(y2)) if y1 == y2 && !xs.contains(y1) =>
      Constraints::empty()
    (TyVar(y), s) if xs.contains(y) => {
      let t = s.demotion(v)
      Map::from_array([(y, { l: TyBot, r: t })])
    }
    (s, TyVar(y)) if xs.contains(y) => {
      let t = s.promotion(v)
      Map::from_array([(y, { l: t, r: TyTop })])
    }
    (TyFun(ys1, r, s), TyFun(ys2, t, u)) if ys1 == ys2 => {
      let vy = v.union(Set::from_array(ys1))
      let cs = t.zip(r).map(tr => { l: tr.0, r: tr.1 }.generate(xs, vy))
        |> meets()
      cs.meet({ l: s, r: u }.generate(xs, vy))
    }
    _ => raise ConstraintGenerationError
  }
}

一个至关重要的观察是，在任何一次调用 $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$ 时，未知变量 $\overline{X}$ 都只会出现在 $S$ 和 $T$ 的其中一边。这使得整个过程是一个匹配模子类型（matching-modulo-subtyping）问题，而非一个完全的合一（unification）问题，从而保证了算法的简洁性与确定性。

通过前述的约束生成步骤，我们已经成功地将一个非构造性的最优解搜索问题， 转化为了一个具体、有形的产物：一个约束集 $C$。 这个约束集，凝聚了为了使整个多态应用类型正确，所有待定类型参数 $\overline{X}$ 必须满足的全部边界条件。 对于每一个未知变量 $X_i$，我们都得到了一个形如 $S_i \lt: X_i \lt: T_i$ 的合法区间。

至此，算法的第一阶段「我们对未知数了解了什么？」已经圆满完成。 然而，我们的工作尚未结束。一个约束区间，例如 $\mathbb{Z} \lt: X \lt: \mathbb{R}$， 本身可能允许多个合法的解（如 $\mathbb{Z}$ 或 $\mathbb{R}$）。 我们最终必须为每一个 $X_i$ 挑选出一个具体的类型值，以完成对内核语言项的最终构造。

这就引出了算法的最后一个，也是画龙点睛的一步：我们应依据何种准则，从每个变量的合法区间中做出最终的选择？ 答案，必须回归到我们的初衷，即 App-InfSpec 规约中所声明的最优性要求： 我们所做的选择，必须能使整个应用表达式获得唯一的、最小的结果类型。 因此，算法的最后一步，便是要设计一个选择策略， 它能利用我们已经辛勤收集到的约束集 $C$， 并结合函数原始的返回类型 $R$， 来计算出一组能最终最小化 $R$ 的具体类型参数。 这便是本节「参数计算」的核心任务。

pub fn variance(self : Type, va : Var) -> Variance {
  letrec go = (ty : Type, polarity : Bool) => match ty {
    TyVar(v) if v == va => if polarity { Covariant } else { Contravariant }
    TyVar(_) | TyTop | TyBot => Constant
    TyFun(_, params, ret) => {
      let param_variance = params
        .map(p => go(p, !polarity))
        .fold(init=Constant, combine_variance)
      combine_variance(param_variance, go(ret, polarity))
    }
  }
  and combine_variance = (v1 : Variance, v2 : Variance) => match (v1, v2) {
    (Constant, v) | (v, Constant) => v
    (Covariant, Covariant) | (Contravariant, Contravariant) => v1
    (Covariant, Contravariant) | (Contravariant, Covariant) => Invariant
    (Invariant, _) | (_, Invariant) => Invariant
  }

  go(self, true)
}

为了最小化返回类型 $R$，我们的选择策略变得显而易见：

• 若 $X_i$ 在 $R$ 中是协变的，我们应为 $X_i$ 选择其合法区间内的最小值，即其约束的下界。
• 若 $X_i$ 在 $R$ 中是逆变的，我们应为 $X_i$ 选择其合法区间内的最大值，即其约束的上界。
• 若 $X_i$ 在 $R$ 中是不变的，则为了保证结果的唯一性与可比较性，其合法区间必须是一个「点」，即其约束的上下界必须相等。

上述策略被形式化为一个计算最小代换（minimal substitution） $\sigma_{CR}$ 的算法。给定一个可满足的约束集 $C$ 和返回类型 $R$：

对于 $C$ 中的每一个约束 $S \lt: X_i \lt: T$：

• 若 $R$ 在 $X_i$ 上是协变或常数的，则 $\sigma_{CR}(X_i) = S$。
• 若 $R$ 在 $X_i$ 上是逆变的，则 $\sigma_{CR}(X_i) = T$。
• 若 $R$ 在 $X_i$ 上是不变的，且 $S=T$，则 $\sigma_{CR}(X_i) = S$。
• 在其他所有情况下（尤其是不变变量的约束区间 $S \neq T$ 时），$\sigma_{CR}$ 未定义。

当 $\sigma_{CR}$ 未定义时，算法宣告失败，这精确地对应了 App-InfSpec 中无法找到唯一最优解的情形。

pub fn solve(self : Constraints, ty : Type) -> Map[Var, Type]? {
  let f = (vs : (Var, Subtype)) => {
    let { l, r } = vs.1
    let v = match ty.variance(vs.0) {
      Constant | Covariant => Some(l)
      Contravariant => Some(r)
      Invariant => if l == r { Some(l) } else { None }
    }
    v.map(v => (vs.0, v))
  }
  let i = self.inner().iter().filter_map(f)
  guard i.count() == self.inner().size() else { None }
  Some(Map::from_iter(i))
}

这一核心命题证明了我们设计的这套具体算法与 App-InfSpec 规约之间的等价性。 它允许我们最终用一个完全算法化的规则 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}) : \sigma R } \quad (\text{App-InfAlg}) $$

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

然而，我们的工具箱尚不完备。回顾引言中基于 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。

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

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}) $$

实现留作习题。

至此，我们循着 Pierce 与 Turner 的足迹，完整地剖析了一套精巧而强大的局部类型推断机制。 通过将局部类型参数合成与双向类型检查这两项核心技术相结合， 我们最终完成了一个真正强大的类型检查器的设计。 它不仅能在理论上驾驭如 System $F_{\le}$ 这样兼具子类型化与非直谓多态的强大类型系统， 更在实践中，精准地解决了由多态、 高阶编程与纯函数式风格所引发的最为普遍和恼人的类型标注问题。 这套完全基于「局部性」原则的算法，其行为可预测、 易于实现且错误提示友好，堪称是连接艰深理论与日常编程实践的一座典范之桥。

当然，本文所探讨的，仅是这篇经典论文的核心部分。原文的疆域更为广阔， 其中最重要的扩展，便是对有界量化（Bounded Quantification）的支持。 有界量化，即形如 $\forall (X \lt: T_2, Y \lt: T_2, \cdots) . e$ 的多态， 它允许类型参数本身受到其超类型的约束。这一特性对于精确建模面向对象语言中的继承等高级特性至关重要，是通往更强大表达能力的必由之路。 原文第五章详细阐述了如何将本文介绍的局部推断技术扩展至支持有界量化的系统。该扩展使得算法，尤其是约束的生成与求解，将变得更为精妙和复杂， 特别是在处理 $\bot$ 类型与类型边界的相互作用时， 引入了新的挑战。限于篇幅，对这一部分的深入剖析，或许只能留待未来的文章再行探讨。 此外，本文的另一大遗憾是「形式证明」的缺失。我们关注的重点，在于阐明算法的设计动机与直觉， 并以一种接近实际代码实现的方式来呈现其逻辑。为此，我们省略了诸多严谨的数学证明细节， 例如约束生成算法的可靠性与完备性证明，仅以提要的形式一笔带过。

最后，值得一提的是，本文对类型系统代数性质的倚重——例如，确保任意类型间的最小上界（join）与最大下界（meet）总是存在——揭示了一条深刻的设计原则：一个具有良好代数结构的类型系统，往往更能催生出简洁而强大的类型推断算法。自这篇论文发表以来，寻求更优美的子类型化代数理论的探索从未停止。后续的研究，如 Stephen Dolan 等人提出的「代数子类型」（Algebraic Subtyping）， 正是沿着这一思想路径，对子类型关系的形式化进行了更为深刻的抽象与简化， 在笔者看来，它是真正改变子类型研究的天才之作。 当然，对这些更前沿工作的介绍，已然超出了对这篇 2000 年经典论文本身进行解读的范畴， 我们把它留给未来的文章。