For readers new to programming language theory, the mathematical symbols and inference rules scattered throughout the text may appear unfamiliar and intimidating.
Please do not worry. These formal tools are not designed to be obscure; on the contrary,
they aim to achieve precision and unambiguity that natural language struggles to attain.
This section provides a simple guide to reading these rules. Readers already familiar with them may skip ahead.

You can think of these rules as the fundamental “physical laws” of a programming language. In a highly rigorous manner,
they define what programs are well-structured and meaningful, and which are not.

Most rules in this article are presented in the following form:
$$\frac{\text{Premise}_1 \quad \text{Premise}_2 \quad ...}{\text{Conclusion}} \quad (\text{Rule Name})$$
The long horizontal line is the key to understanding everything.

• Above the line: Premises
  • This lists a set of conditions or assumptions.
  • The rule can only be activated or used when all premises are satisfied.
• Below the line: Conclusion
  • This is the new fact we can infer after all premises are satisfied.
• Right parenthesis: Rule Name
  • This is simply a name assigned to the rule for ease of reference and discussion, such as Var or App.

In the premises and conclusions of the rules, you will repeatedly encounter a core judgment of the form $\Gamma \vdash e : T$. Let us break down each symbol:

• $\Gamma$ (Gamma): This is the context. It represents all known background information or assumptions during inference. Typically, it records types assigned to variables, e.g., $x : \mathbb{Z},\ f : \mathrm{Bool} \to \mathrm{Bool}$. You can interpret it as “given…” or “under the environment of…”.
• $\vdash$ (Turnstile): This symbol is read as “yields” or “proves.” It separates the context from the assertion being verified.
• $e$: This is the term—the piece of program code being analyzed. It could be a simple variable $x$, a function $\mathsf{fun}(x)\ x + 1$, or a complex expression.
• $:$ denotes “has type.”
• $T$: This is the type, such as $\mathbb{Z}$, $\mathrm{Bool}$, $\mathrm{String} \to \mathbb{Z}$, etc.

Putting it all together, the judgment $\Gamma \vdash e : T$ plainly means:
“Given the known conditions in context $\Gamma$, we can infer (or prove) that program term $e$ has type $T$.”

After abandoning the pursuit of “complete type inference,” a crucial question emerges: To what extent must a “partial” type inference algorithm infer types to be considered “enough”? A highly pragmatic answer: The core mission of a good partial type inference algorithm is to eliminate those type annotations that are both pervasive and foolish.

Here, “foolish” stands in contrast to “reasonable.” “Reasonable” annotations, such as type declarations for parameters in top-level function definitions, typically serve as valuable, compiler-verified documentation that aids code comprehension. “Foolish” annotations, conversely, add nothing but syntactic noise while providing almost no useful information. Imagine in a fully explicitly-typed language, no one would want to write or read those redundant Int annotations in cons[Int](3, nil[Int]).

Pierce’s study of hundreds of thousands of lines of ML code revealed three primary sources of “foolish annotations”:

• Polymorphic instantiation: In the measured code, type applications (i.e., instantiations of polymorphic functions) were ubiquitous, occurring at least once every three lines on average. These type parameters inserted at polymorphic function call sites offer virtually no documentation value and are purely syntactic baggage.
• Anonymous function definitions: Adding type annotations to parameters of anonymous functions in contexts like map(list, fun(x) x+1) only obscures the core logic, creating unnecessary distraction.
• Local variable bindings (Let): Annotating types for these short-lived intermediate variables is clearly tedious and meaningless.

Based on these quantitative observations, we can outline the contours of an “enough” partial type inference algorithm:

1. It must infer type arguments in polymorphic function applications. Meanwhile, requiring programmers to provide explicit annotations for top-level functions or relatively scarce local functions is entirely acceptable, as these annotations themselves constitute beneficial documentation.
2. To facilitate higher-order programming, the algorithm should infer types for anonymous function parameters, though this isn’t strictly mandatory.
3. Local variable bindings should generally not require explicit type annotations.

Before rigorously discussing the topic of type inference, we must first clearly define its inference target—an unambiguous, fully annotated internal language. This language serves as the “true” representation within the compiler and is the final form into which the external language—written by programmers and allowing omitted annotations—is translated.

The internal language used in this article originates from the well-known calculus System $F_\leq$ proposed by Cardelli and Wegner, which incorporates subtyping and impredicative polymorphism. However, we extend it by adding the $\bot$ (Bottom) type. To ensure the existence of supremum and infimum, this algebraic structure’s completeness is fundamental for the concise and deterministic operation of the constraint-solving algorithm in subsequent chapters. Additionally, it can serve as the result type for expressions that never return (e.g., functions that throw exceptions). We first define the formal language as follows
(Note: Overline denotes sequence notation $\overline{X} = X_1, X_2, \dots, X_n$; similarly, $\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} $$

We can simply map the above formal language to the following MoonBit code,
where Var implements type variables:

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

After defining the type and subtype relations, we can now present the typing rules for the kernel language. These rules define the typing judgment $\Gamma \vdash e : T$, meaning “in context $\Gamma$, term $e$ has type $T$.”

Consistent with the definition of the subtype relation, these typing rules adopt an algorithmic presentation style and omit the subsumption rule commonly found in traditional type systems (where if $e$ has type $S$ and $S \lt: T$, then $e$ can also have type $T$).

By omitting this rule, the system computes a unique, minimal type for every typable term, which the author calls its manifest type. This design choice does not alter the set of typable terms in the language but ensures that every term has exactly one type derivation path. This significantly enhances the system’s predictability.

Core Rules

• Variable

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

• Abstraction
  This rule unifies traditional term abstraction and type 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}) $$

  To derive the type of $\mathbf{fun}[\overline{X}] (\overline{x}:\overline{S})$, we add bindings for type variables $\overline{X}$ and value variables $\overline{x}:\overline{S}$ to context $\Gamma$. We then derive type $T$ for the function body $e$ in this extended context. The entire function’s type is $\forall \overline{X}.\overline{S} \to T$.

• Application
  This rule unifies traditional term application and polymorphic application. It first derives the type of function f, then verifies that all actual arguments (type and term arguments) conform to the function’s signature.
  The requirement is relaxed: actual argument types need only satisfy the subtype relation with parameter types, not exact matches.

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

  Here, the notation $\Gamma \vdash \overline{e} \lt: [\overline{T}/\overline{X}]\overline{S}$ abbreviates $\Gamma \vdash \overline{e} \lt: \overline{U}$ followed by verifying $\overline{U} \lt: [\overline{T}/\overline{X}]\overline{S}$. The result type is obtained by substituting actual type arguments $\overline{T}$ into the function’s original return type $R$.

  4.1. Type Parameter Substitution [blog/lti-english/subst_code][edit]

  A new notation $[\overline{T}/\overline{X}]R$ appears here, representing the resulting type after substituting the type parameters $\overline{X}$ with the actual types $\overline{T}$. This notation will appear frequently in subsequent code. The following code defines the mk_subst function to generate a type substitution map, and an apply_subst function that applies this map to a concrete type. $[\overline{T}/\overline{X}]R$ is obtained through $\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 Type::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 Application
  Introducing the $\bot$ type necessitates this special application rule to maintain type soundness.
  Since $\bot$ is a subtype of any function type, a $\bot$-typed expression should be applicable to any valid arguments without type errors.

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

  This rule states that when a $\bot$-typed term is applied, the entire expression has type $\bot$ regardless of arguments—the most precise (minimal) result type possible.

These rules collectively ensure a key property: Uniqueness of Manifest Types. If $\Gamma \vdash e : S$ and $\Gamma \vdash e : T$, then $S=T$.

So far, we have defined the type rules for the core language, but we are still far from our goal: the core language requires numerous annotations, including explicitly providing type arguments during polymorphic instantiation. Since this occurs frequently in code, it becomes the primary pain point we aim to address in this section.

This is the goal of Local Type Argument Synthesis: allowing programmers to safely omit type arguments when calling polymorphic functions, writing $\text{id}(3)$ instead of $\text{id}[\mathbb{Z}](3)$. However, omitting type arguments introduces a core challenge: for a given application like $\text{id}(x)$ (where $x : \mathbb{Z}$ and $\mathbb{Z} \lt: \mathbb{R}$), there are often multiple valid type argument instantiations, such as $\text{id}[\mathbb{Z}](x)$ or $\text{id}[\mathbb{R}](x)$ here. We must establish a clear criterion for selection: choose the type argument that yields the most precise (i.e., smallest) result type for the entire application expression. In the $\text{id}(x)$ example, since the result type $\mathbb{Z}$ of $\text{id}[\mathbb{Z}](x)$ is a subtype of $\mathbb{R}$ (the result type of $\text{id}[\mathbb{R}](x)$), the former is clearly the superior and more informative choice.

However, this locally optimal “best result type” strategy is not universally applicable. In some cases, a “best” solution may not exist. For example, consider a function $f$ with type $\forall X. () \to (X \to X)$. For the application $f()$, both $f[\mathbb{Z}]()$ and $f[\mathbb{R}]()$ are valid completions, yielding result types $\mathbb{Z} \to \mathbb{Z}$ and $\mathbb{R} \to \mathbb{R}$ respectively. These function types are incomparable under the subtype relation, so no unique minimal result type exists. In such scenarios, local synthesis fails.

Recalling our earlier core language definition, we required application constructs to take the form $e[\overline{T}](\overline{e})$, meaning we manually specified type arguments $\overline{T}$. Rule App could compute the result type based on these arguments. Now, to make the language simpler and more ergonomic, we allow omitting type arguments $\overline{T}$. We update the language construct as follows:

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

This introduces a new expression structure EAppI(Expr, Array[Expr]), corresponding to the type-argument-omitted form. (For later discussion convenience, we also add the EAbsI construct here.) We now require a new rule:

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

As humans, we can intuitively formulate rules or even design declarative rules that cannot be implemented as code, precisely defining “what constitutes a correct, optimal type argument inference”:

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

Here we use existential quantification $\exists \overline{U}$ and require $\overline{U}$ to satisfy multiple conditions. For instance, $\overline{S} \lt: [\overline{U}/\overline{X}]\overline{T}$ is the validity constraint, ensuring that the chosen type arguments $\overline{U}$ are legal. Legality here means that after substituting $\overline{U}$ into the function’s formal parameter types $\overline{T}$, the actual argument types $\overline{S}$ must be subtypes. Crucially, the final rule $\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$ requires considering all possible type argument tuples $\overline{V}$. This translates to searching through a potentially infinite space of $\overline{V}$, making it a classic non-constructive description that cannot be implemented in a computer.

Thus, our goal becomes clear: we need a truly executable algorithm whose results align with (App-InfSpec), but without requiring non-constructive search or backtracking. This is precisely the role that constraint generation will play. Its design motivation stems from an ingenious perspective shift on the problem itself.

Rather than treating type parameter inference as a search problem of “finding and verifying the optimal solution” among infinite possibilities,
we reframe it as a problem of “solving for unknown boundaries” similar to solving algebraic equations.
Instead of guessing what the type parameters $\overline{X}$ might be,
we derive the conditions $\overline{X}$ must satisfy by analyzing the subtyping relation itself.

Observing that our rules contain subtyping constraints, consider the general case $S \lt: T$,
which inherently implies constraints on its components (including unknown variables).
If $X$ is an unknown variable in $T$, the structure of $S$ necessarily restricts the possible forms of $X$.
Our algorithm transforms this implicit structural restriction into a set of explicit assertions about $X$’s bounds.

However, before systematically extracting these constraints, we must first address a preliminary yet critical challenge related to variable scoping.
If not handled properly, the constraints we generate may themselves be ill-formed.
This challenge motivates the algorithm’s first concrete step: variable elimination.

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

Constraint generation is the core engine of the local type parameter synthesis algorithm.
After ensuring scoping safety through variable elimination,
this step’s mission is to transform a subtyping judgment—for example,
$S \lt: T$ where $S$ or $T$ contains undetermined type parameters $\overline{X}$—into a set of explicit constraints on these unknowns $\overline{X}$.
We now formally define the structure of constraints in code:

• Constraint: In this system, each constraint takes the form $S_i \lt: X_i \lt: T_i$, specifying both a lower bound $S_i$ and an upper bound $T_i$ for a single unknown type variable $X_i$.

• Constraint Set: A constraint set $C$ is a finite mapping (implementable as a Hash Map in code) from a group of unknown variables $\overline{X}$ to their corresponding constraints. A key invariant is that the bounds ($S_i$, $T_i$) in any constraint must not contain any pending unknown variables (i.e., variables in $\overline{X}$) or any local variables to be eliminated (i.e., variables in $V$). The empty constraint set ($\emptyset$) represents the least restrictive constraint, equivalent to $\bot \lt: X_i \lt: \top$ for each $X_i$.

• Constraint set intersection ($\wedge$) is defined as the intersection of two constraint sets $C$ and $D$, obtained by merging constraints for the same variable. The new lower bound is the least upper bound (join, $\vee$) of the original lower bounds, while the new upper bound is the greatest lower bound (meet, $\wedge$) of the original upper bounds.

struct Constraints(Map[Var, Subtype])

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

fn Constraints::items(self : Constraints) -> Map[Var, Subtype] {
  let Constraints(items) = self
  items
}

pub fn Constraints::meet(
  self : Constraints,
  other : Constraints,
) -> Constraints {
  Constraints(
    union_with(self.items(), other.items(), (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)
}

The constraint generation process is formalized as a derivation relation $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$, meaning: given a set of variables $V$ to avoid, the (weakest) constraint set $C$ on unknown variables $\overline{X}$ required for $S \lt: T$ to hold, where $C$ is the output of this relation.

The algorithm is defined by recursive rules, with key rules as follows (note: we always assume $\overline{X} \cap V = \emptyset$):

• Trivial Cases: When the upper bound of the subtyping relation is $\top$ or the lower bound is $\bot$, the relation holds unconditionally, thus generating an empty constraint set $\emptyset$.
• Upper Bound Constraint: When judging $Y \lt: S$ (where $Y \in \overline{X}$ is an unknown variable and $S$ is a known type), the algorithm generates an upper bound constraint for $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}) $$
  Note that the variable elimination operation ($S \Downarrow^V T$) ensures the upper bound $T$ is well-formed.
• Lower Bound Constraint: Dually, when judging $S \lt: Y$, the algorithm generates a lower bound constraint for $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: When comparing function types, the algorithm recursively processes parameter and return types, then merges the resulting sub-constraint sets.
  $$ \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}) $$
  Here, constraints are accumulated through intersection ($\wedge$) of sub-constraint sets.

/// Pre-condition: xs and v are disjoint sets of variables.
pub fn Subtype::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)
      Constraints(Map::from_array([(y, { l: TyBot, r: t })]))
    }
    (s, TyVar(y)) if xs.contains(y) => {
      let t = s.promotion(v)
      Constraints(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
  }
}

A crucial observation is that in any invocation $V \vdash_{\overline{X}} S \lt: T \Rightarrow C$, the unknown variables $\overline{X}$ appear only on one side of $S$ or $T$. This makes the entire process a matching-modulo-subtyping problem rather than a full unification problem, ensuring the algorithm’s simplicity and determinism.

Through the preceding constraint generation step, we have successfully transformed a non-constructive optimal solution search problem into a concrete, tangible outcome: a constraint set $C$. This constraint set encapsulates all boundary conditions that the undetermined type parameters $\overline{X}$ must satisfy for the entire polymorphic application to be type-correct. For each unknown variable $X_i$, we obtain a valid interval of the form $S_i \lt: X_i \lt: T_i$.

At this point, the first phase of the algorithm—“What do we know about the unknowns?”—has been successfully completed. However, our work is not yet finished. A constraint interval, such as $\mathbb{Z} \lt: X \lt: \mathbb{R}$, may itself permit multiple valid solutions (e.g., $\mathbb{Z}$ or $\mathbb{R}$). Ultimately, we must select a concrete type value for each $X_i$ to finalize the construction of the core language term.

This leads us to the final and crucial step of the algorithm: By what criteria should we make the ultimate choice from each variable’s valid interval? The answer must return to our original intent—the optimality requirement declared in the App-InfSpec specification: Our choices must yield a unique, minimal result type for the entire application expression. Therefore, the algorithm’s last step is to design a selection strategy that leverages the constraint set $C$ we have diligently collected, combines it with the function’s original return type $R$, and computes a set of concrete type arguments that ultimately minimize $R$. This is the core task of this section: “Calculating Type Arguments.”

pub fn Type::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)
}

To minimize the return type $R$, our selection strategy becomes evident:

• If $X_i$ is covariant in $R$, we should choose the minimum value within its valid interval, i.e., its constraint’s lower bound.
• If $X_i$ is contravariant in $R$, we should choose the maximum value within its valid interval, i.e., its constraint’s upper bound.
• If $X_i$ is invariant in $R$, then to ensure result uniqueness and comparability, its valid interval must be a “single point,” i.e., its constraint’s upper and lower bounds must be equal.

The above strategy is formalized as an algorithm for computing the minimal substitution $\sigma_{CR}$. Given a satisfiable constraint set $C$ and return type $R$:

For each constraint $S \lt: X_i \lt: T$ in $C$:

• If $R$ is covariant or constant in $X_i$, then $\sigma_{CR}(X_i) = S$.
• If $R$ is contravariant in $X_i$, then $\sigma_{CR}(X_i) = T$.
• If $R$ is invariant in $X_i$ and $S=T$, then $\sigma_{CR}(X_i) = S$.
• In all other cases (especially when $S \neq T$ for invariant variables), $\sigma_{CR}$ is undefined.

When $\sigma_{CR}$ is undefined, the algorithm fails, precisely corresponding to the scenario in App-InfSpec where no unique optimal solution can be found.

pub fn Constraints::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 constraints = self.items()
  let solved = constraints.iter().filter_map(f).to_array()
  guard solved.length() == constraints.length() else { None }
  Some(Map::from_array(solved))
}

This core proposition proves the equivalence between our designed concrete algorithm and the App-InfSpec specification. It allows us to ultimately replace that non-executable specification with a fully algorithmic rule 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}) $$

At this point, we have thoroughly dissected the first key focus of this article: local type parameter synthesis. Through a logically rigorous and fully executable algorithm comprising “variable elimination,” “constraint generation,” and “parameter calculation,” it perfectly resolves the cumbersome type parameter annotation issues caused by fine-grained multipropositions, achieving the first of the three design principles stated in the introduction.

However, our toolbox remains incomplete. Revisiting the three design principles proposed in the introduction based on ML code analysis, two critical challenges remain unresolved:

1. Convenience of Higher-Order Programming: How to infer the type of bound variables (e.g., x in fun[](x) x+1) within anonymous functions?
2. Support for Purely Functional Style: How to enable extensive local variable bindings (e.g., let x = ...) without explicit type annotations?

The local type parameter synthesis mechanism, with its inherently bottom-up information flow, derives an optimal result type based on the existing types of functions and parameters. This approach falls short for the two problems above because expressions like fun[](x) x+1 contain no substructures that provide type information for x.

We consider a powerful local inference technique conceptually complementary to the former. Instead of relying solely on bottom-up information synthesis, it introduces a top-down information flow, allowing the context surrounding an expression to guide its internal type checking. This is Bidirectional Type Checking. Though its core idea has long been a “folk consensus” in the programming language community and has been applied in some attribute grammar-based ML compilers, this article rigorously axiomatizes it within a formal system combining subtyping and impredicative polymorphism. We present it as an independent local inference method, revealing surprisingly potent capabilities.

Two Modes: Synthesis and Checking

1. Synthesis Mode ($\Rightarrow$)

   • In this mode, type information propagates bottom-up.
   • Its goal is to compute (or “synthesize”) the type of an expression based on the types of its subexpressions.
   • This corresponds to traditional type checking and applies to contexts where the expected type is unknown, such as top-level expressions or the function part of an application node.

2. Checking Mode ($\Leftarrow$)

   • In this mode, type information propagates top-down.
   • Its goal is to verify (or “check”) whether an expression satisfies an “expected type” (or a subtype thereof) provided by its context.
   • This mode activates when the context already determines the expression’s type.

The essence of bidirectional checking lies in the flexible switching between modes. A typical function application f(e) perfectly illustrates this process: the type checker first synthesizes the type of function f, then uses this information to switch modes and check the argument e.

The final implementation centers on two key functions: synthesis and check.
This is the most crucial exercise in this article.
Readers are strongly encouraged to implement these functions themselves to appreciate the elegance of bidirectional checking
and learn techniques for translating type rules into code.

pub fn Expr::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 e.length() == t.length() else { raise ArgumentLengthMismatch }
      // guard !xs.is_empty() else { raise NotFound }
      let es = e.map(expr => expr.synthesis(gamma))
      let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set([])))
      let sigma = meets(cs).solve(r)
      sigma.map(s => r.apply_subst(s)).unwrap_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)
      guard e.length() == ss.length() else { raise ArgumentLengthMismatch }
      e.zip(ss).each(es => es.0.check(es.1.apply_subst(subst), gamma))
      r.apply_subst(subst)
    }
    _ => raise SynthesisError
  }
}

pub fn Expr::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.length() == vs.length() else { raise CheckError }
      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) else { () }
      guard f.synthesis(gamma) is TyFun(xs, t, r) else { raise CheckError }
      guard e.length() == t.length() else { raise ArgumentLengthMismatch }
      guard !xs.is_empty() else { () }
      let es = e.map(expr => expr.synthesis(gamma))
      let cs = es.zip(t).map(z => { l: z.0, r: z.1 }.generate(xs, Set([])))
      let d = { l: r, r: u }.generate(xs, Set([]))
      guard meets(cs).meet(d).satisfiable() else { raise CheckError }
    }
    (EApp(f, ty, e), u) => {
      let t = f.synthesis(gamma)
      guard !(t is TyBot) else { () }
      guard t is TyFun(xs, ss, r)
      let subst = mk_subst(xs, ty)
      guard e.length() == ss.length() else { raise ArgumentLengthMismatch }
      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
  }
}

The last critical objective is the design for local variable bindings,
which requires introducing a new syntactic construct ELet. Its rules are straightforward:

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

Implementation is left as an exercise.

Thus far, following in the footsteps of Pierce and Turner, we have thoroughly dissected an elegant and powerful mechanism for local type inference. By combining the two core techniques of local type parameter synthesis and bidirectional type checking, we have ultimately completed the design of a truly robust type checker. This system not only theoretically handles powerful type systems like System $F_{\le}$—which integrates subtyping and impredicative polymorphism—but also practically resolves the most pervasive and vexing issues of type annotations arising from polymorphism, higher-order programming, and pure functional styles. Entirely grounded in the principle of “locality,” this algorithm exhibits predictable behavior, ease of implementation, and user-friendly error diagnostics, serving as an exemplary bridge connecting profound theory with everyday programming practice.

Of course, this article only addresses the core aspects of the seminal paper. The original work explores a broader landscape, with its most significant extension being support for bounded quantification. Bounded quantification, expressed as $\forall (X \lt: T_2, Y \lt: T_2, \cdots) . e$, allows type parameters to be constrained by their supertypes. This feature is indispensable for precisely modeling advanced constructs like inheritance in object-oriented languages and represents a critical pathway toward greater expressive power. Chapter 5 of the original paper details how to extend the local inference technique discussed here to systems supporting bounded quantification. This extension renders the algorithm—particularly constraint generation and solving—more intricate and complex, introducing new challenges when handling interactions between the $\bot$ type and type bounds. Due to space constraints, a deeper examination of this topic must be deferred to future articles. Additionally, a notable limitation of this work is the absence of formal proofs. Our focus has been on elucidating the algorithm’s design motivations and intuitions while presenting its logic in a manner akin to practical implementation. Consequently, we omitted rigorous mathematical details—such as soundness and completeness proofs for the constraint generation algorithm—providing only brief summaries.

Finally, it is worth emphasizing this work’s reliance on the algebraic properties of type systems—for instance, ensuring that the least upper bound (join) and greatest lower bound (meet) always exist between any types—which reveals a profound design principle: type systems with well-behaved algebraic structures often yield more elegant and powerful type inference algorithms. Since this paper’s publication, the quest for a more refined algebraic theory of subtyping has continued unabated. Subsequent research, such as Stephen Dolan’s “Algebraic Subtyping,” advances this intellectual trajectory by abstracting and simplifying the formalization of subtyping relations—a transformative contribution that, in the author’s view, redefines subtyping research. Naturally, exploring these cutting-edge developments exceeds the scope of interpreting this classic 2000 paper and remains a subject for future work.