Variable Elimination [blog/lti-english/var_elim][edit]

    Suppose we want to generate constraints for variable $X$ such that type $\forall Y. () \to (Y\to Y)$ becomes a subtype of $\forall Y. () \to X$. According to the contravariant/covariant rules for function subtyping, this requires $Y \to Y \lt: X$. However, we cannot directly generate the constraint $\{ Y \to Y \lt: X \lt: \top\}$ because the type variable $Y$ is free in this constraint, yet it should be bound by $\forall Y$, resulting in a scope error.

    The correct approach is to find a supertype of $Y \to Y$ that contains no $Y$ and is as precise as possible, then use it to constrain $X$. In this case, that supertype is $\bot \to \top$. The variable elimination mechanism formally accomplishes this task of “finding the most precise bound”.

    1. Promotion, $S \Uparrow^V T$: $T$ is a minimal supertype of $S$ containing no free variables from set $V$.
    2. Demotion, $S \Downarrow^V T$: $T$ is a maximal subtype of $S$ containing no free variables from set $V$.

    These two relations are defined by a set of recursive rules, ensuring that for any type $S$ and variable set $V$, the resulting $T$ is unique and always computable (i.e., they are total functions).
    We suggest readers pause here to consider how to design recursive rules for these relations and implement them in code (hint: for promotion, if $X \in V$ then promote it to $\top$, otherwise leave it unchanged; other cases are straightforward).

    1. Promotion and Demotion Rules [blog/lti-english/ve_rules][edit]

      • Promotion Rules ($S \Uparrow^V T$)

        • For $\top$ and $\bot$: $$ \top \Uparrow^V \top \quad (\text{VU-Top}) $$ $$ \bot \Uparrow^V \bot \quad (\text{VU-Bot}) $$
        • For type variable $X$:
          • If $X$ belongs to the set $V$ that needs to be eliminated, promote it to $\top$. $$ \frac{X \in V}{X \Uparrow^V \top} \quad (\text{VU-Var-1}) $$
          • If $X$ is not in $V$, it remains unchanged. $$ \frac{X \notin V}{X \Uparrow^V X} \quad (\text{VU-Var-2}) $$
        • For function types:
          • Recursively demote its parameter types (contravariant position) and promote its return type (covariant position). $$ \frac{\overline{S} \Downarrow^V \overline{U} \quad T \Uparrow^V R \quad \overline{X} \notin V}{\forall\overline{X}.\overline{S} \to T \Uparrow^V \forall\overline{X}.\overline{U} \to R} \quad (\text{VU-Fun}) $$

      • Demotion Rules ($S \Downarrow^V T$)

        • Handling of $\top$ and $\bot$ is consistent with promotion rules.
        • For type variable $X$:
          • If $X$ belongs to $V$, demote it to $\bot$. $$ \frac{X \in V}{X \Downarrow^V \bot} \quad (\text{VD-Var-1}) $$
          • If $X$ is not in $V$, it remains unchanged.
        • For function types:
          • Recursively promote its parameter types and demote its return type. $$ \frac{\overline{S} \Uparrow^V \overline{U} \quad T \Downarrow^V R \quad \overline{X} \notin V}{\forall\overline{X}.\overline{S} \to T \Downarrow^V \forall\overline{X}.\overline{U} \to R} \quad (\text{VD-Fun}) $$

      This can be implemented very straightforwardly in MoonBit:

      pub fn Type::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(s => s.demotion(vP))
      let r = t.promotion(vP)
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyTop
    _ => self
  }
}

pub fn Type::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(s => s.promotion(vP))
      let r = t.demotion(vP)
      TyFun(xs, us, r)
    }
    TyVar(vr) if v.contains(vr) => TyBot
    _ => self
  }
}

      This carefully designed rule set guarantees the correctness and optimality of variable elimination, ensured by two key lemmas:

      • Soundness: If $S \Uparrow^V T$, then $S \lt: T$ holds and $T$ contains no free variables from $V$. Dually, if $S \Downarrow^V T$, then $T \lt: S$ holds and $T$ contains no free variables from $V$.
      • Completeness: The operation finds the “best” bound. For example, in promotion, if there exists another supertype $T'$ of $S$ containing no variables from $V$, then the $T$ computed by $S \Uparrow^V T$ must be a subtype of $T'$ (that is, $T \lt: T'$), proving $T$ is the smallest among all possible options.