calc_args]

通过前述的约束生成步骤，我们已经成功地将一个非构造性的最优解搜索问题，转化为了一个具体、有形的产物：一个约束集 $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$ 的具体类型参数。这便是本节「参数计算」的核心任务。

1. Polarity [blog/lti/polarity]

为了计算关于 $R$ 的具体类型参数，还有一个至关重要的操作：变量代换导致的极性变化。一个类型变量 $X$ 在另一个类型表达式 $R$ 中的极性，描述了当该变量的类型变大或变小时，整个表达式的类型会如何相应地变化。

协变 (Covariant)：若 $R$ 在 $X$ 上是协变的，则 $X$ 的「变大」（成为一个超类型）会导致 $R$ 也「变大」。例如，在 $T \to X$ 中，$X$ 是协变的。若 $\mathbb{Z} \lt: \mathbb{R}$，则 $T \to \mathbb{Z} \lt: T \to \mathbb{R}$。
逆变 (Contravariant)：若 $R$ 在 $X$ 上是逆变的，则 $X$ 的「变大」会导致 $R$ 「变小」（成为一个子类型）。例如，在 $X \to T$ 中，$X$ 是逆变的。若 $\mathbb{Z} \lt: \mathbb{R}$，则 $\mathbb{R} \to T \lt: \mathbb{Z} \to T$。
不变 (Invariant)：若 $R$ 在 $X$ 上是不变的，则只有当 $X$ 保持不变时，$R$ 才保持不变。任何改变都会导致不可比较的结果。例如，在 $X \to X$ 中，$X$ 是不变的。
常量 (Constant)：若 $R$ 在 $X$ 上是常量的，则 $X$ 的变化不会影响 $R$ 的类型。常量类型通常是指那些不包含变量的类型，如基本类型或具体的类。

现在我们对极性的考虑主要集中在函数类型之上，只需要关注变量在函数类型中的位置即可（在箭头的左边还是右边），当然，需要考虑到嵌套的函数结构。建议读者在此稍作停顿，考虑一下该算法的设计。当然你也可以直接展开下面的代码块来查看具体实现。

1.1. Variance Code [blog/lti/variance_code]

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 中无法找到唯一最优解的情形。

2. Solving Constraints [blog/lti/solve_code]

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

3. Proof Sketch [blog/lti/proof_eq]

至此，我们已经完整地定义了一个由「变量消去」、「约束生成」和「参数计算」三步构成的、完全可执行的算法。但我们如何确保这个具体的算法，其行为与那个非构造性的、声明式的 App-InfSpec 规约完全一致？

其等价性的证明，浓缩于一个核心命题中，该命题断言：

若最小代换 $\sigma_{CR}$ 存在，那么它就是规约所要求的那个最优解。
若最小代换 $\sigma_{CR}$ 不存在，那么规约所要求的最优解也必然不存在。

证明概要：

第一部分（算法的正确性）：为证明 $\sigma_{CR}$ 是最优的，我们任取另一个满足约束的合法代换 $\sigma'$，并需要证明 $\sigma_{CR}(R) \lt: \sigma'(R)$。考虑构建一个从 $\sigma_{CR}$ 到 $\sigma'$ 的「代换链」，每一步只改变一个变量的值。例如，$\sigma_0 = \sigma_{CR}$，$\sigma_1 = \sigma_0[X_1 \mapsto \sigma'(X_1)]$，…，$\sigma_n = \sigma'$。接着，我们证明在此路径的每一步中，结果类型都是单调不减的，即 $\sigma_{i-1}(R) \lt: \sigma_i(R)$。这一步的证明，直接依赖于前述的极性定义。例如，若 $R$ 在 $X_i$ 上是协变的，我们的算法选择了下界 $S$，而 $\sigma'(X_i)$ 必然大于等于 $S$，因此根据协变的定义，结果类型必然「变大」。同理可以证明其他情况下该论断也成立。最终，通过传递性，我们得出 $\sigma_{CR}(R) \lt: \sigma'(R)$，证明了 $\sigma_{CR}$ 的最优性。
第二部分（算法失败的完备性）：当算法失败时，必然是因为某个不变变量 $X_i$ 的约束区间 $[S, T]$ 中 $S \neq T$。我们采用反证法：假设此时仍然存在一个最优解 $\sigma$。由于 $S \neq T$，我们总能找到另一个合法的代换 $\sigma'$，使得 $\sigma(X_i)$ 与 $\sigma'(X_i)$ 不同。但由于 $R$ 在 $X_i$ 上是不变的，$\sigma(R)$ 与 $\sigma'(R)$ 将变得不可比较，这与「$\sigma$ 是最优解（即比所有其他解都小）」的假设相矛盾。因此，在这种情况下，最优解必然不存在。

这一核心命题证明了我们设计的这套具体算法与 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}) $$