Bidirectional Checking [blog/lti-english/bidirectional][edit]

    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.

    1. Typing Rules [blog/lti-english/bidi_rules][edit]

      This section is the final piece of our type checker, describing the entire bidirectional type checking process.

      Variable Rules

      1. Synthesis - Variable (Synthesis-Var)

      $$ \frac{}{\Gamma \vdash x \Rightarrow \Gamma(x)} \quad (\text{S-Var}) $$

      This is the synthesis rule for variables. To synthesize the type of a variable $x$, simply look up its declared type $\Gamma(x)$ in the current typing context $\Gamma$. This is the most straightforward form of type derivation: a variable’s type is its declared type.

      2. Checking - Variable (Checking-Var)

      $$ \frac{\Gamma \vdash \Gamma(x) \lt: T}{\Gamma \vdash x \Leftarrow T} \quad (\text{C-Var}) $$

      This is the checking rule for variables. To verify that variable $x$ conforms to expected type $T$, we first retrieve its actual type $\Gamma(x)$ from context $\Gamma$, then validate that this actual type $\Gamma(x)$ is a subtype of $T$. The subtype relation is denoted by $\Gamma \vdash \Gamma(x) \lt: T$.

      Function Abstraction Rules

      3. Synthesis - Abstraction (Synthesis-Abs)

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

      This is the synthesis rule for fully annotated function abstractions.

      • For a function of the form fun [X] (x:S) e where type parameters $\overline{X}$ and value parameter types $\overline{S}$ are explicitly annotated.
      • The premise requires that after adding type variables $\overline{X}$ and value variables with types $\overline{x}:\overline{S}$ to context $\Gamma$, we can synthesize type $T$ for the body $e$.
      • The entire function expression can then be synthesized as polymorphic function type $\forall \overline{X}. \overline{S} \rightarrow T$.

      4. Checking - Unannotated Abstraction (Checking-Abs-Inf)

      $$ \frac{\Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow T}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}) e \Leftarrow \forall \overline{X}. \overline{S} \rightarrow T} \quad (\text{C-Abs-Inf}) $$

      This core rule infers parameter types for unannotated anonymous functions.

      • When checking an unannotated function fun [X] (x) e against expected type $\forall \overline{X}. \overline{S} \rightarrow T$, we extract parameter types $\overline{S}$ and return type $T$ from the expected type.
      • We then add type variables $\overline{X}$ and inferred parameter types $\overline{x}:\overline{S}$ to the context, and check that body $e$ conforms to return type $T$ in this extended context.
      • Note: $\overline{X}$ cannot be omitted in this system.

      5. Checking - Annotated Abstraction (Checking-Abs)

      $$ \frac{\Gamma, \overline{X} \vdash \overline{T} \lt: \overline{S} \quad \Gamma, \overline{X}, \overline{x}:\overline{S} \vdash e \Leftarrow R}{\Gamma \vdash \textbf{fun} [\overline{X}] (\overline{x}:\overline{S}) e \Leftarrow \forall \overline{X}. \overline{T} \rightarrow R} \quad (\text{C-Abs}) $$

      This rule handles annotated functions in checking mode.

      • When checking an annotated function fun [X] (x:S) e against expected type $\forall \overline{X}. \overline{T} \rightarrow R$:
      • First, due to contravariance of function parameters, verify that expected parameter types $\overline{T}$ are subtypes of the function’s actual parameter types $\overline{S}$.
      • Then check that body $e$ conforms to expected return type $R$ in the extended context.

      Function Application Rules

      6. Synthesis - Application (Synthesis-App)

      $$ \frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Rightarrow [\overline{T}/\overline{X}]R} \quad (\text{S-App}) $$

      This is the synthesis rule for function application.

      • First, synthesize the type of $f$ as polymorphic function $\forall \overline{X}. \overline{S} \rightarrow R$.
      • Substitute type variables $\overline{X}$ with provided type arguments $\overline{T}$ to obtain expected parameter types $[\overline{T}/\overline{X}]\overline{S}$.
      • Check that actual arguments $\overline{e}$ conform to these expected types.
      • The application’s type is then synthesized as $[\overline{T}/\overline{X}]R$.

      7. Checking - Application (Checking-App)

      $$ \frac{\Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{S} \rightarrow R \quad \Gamma \vdash [\overline{T}/\overline{X}]R \lt: U \quad \Gamma \vdash \overline{e} \Leftarrow [\overline{T}/\overline{X}]\overline{S}}{\Gamma \vdash f [\overline{T}] (\overline{e}) \Leftarrow U} \quad (\text{C-App}) $$

      This checking rule for function application adds a final subtype check.

      • First two steps mirror S-App: synthesize $f$’s type and check arguments $\overline{e}$.
      • After computing the application’s return type $[\overline{T}/\overline{X}]R$, verify it is a subtype of the expected type $U$.

      Rules Combining Bidirectional Checking and Type Argument Synthesis

      8. Synthesis - Application - Infer Specification (Synthesis-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}) \Rightarrow \sigma R } \quad (\text{S-App-InfAlg}) $$

      This synthesis rule infers missing type arguments in function applications, derived from the “Type Argument Calculation” section.

      9. Checking - Application - Infer Specification (Checking-App-InfAlg)

      $$ \frac{\begin{matrix} \Gamma \vdash f \Rightarrow \forall \overline{X}. \overline{T} \rightarrow R \quad \Gamma \vdash \overline{e} \Rightarrow \overline{S} \quad |\overline{X}| \gt 0 \\ \emptyset \vdash \overline{S} \lt: \overline{T} \Rightarrow C \quad \emptyset \vdash R \lt: V \Rightarrow D \quad \sigma \in \bigwedge C \wedge D \end{matrix}}{\Gamma \vdash f(\overline{e}) \Leftarrow V} \quad (\text{C-App-InfAlg}) $$

      This checking version of App-InfAlg describes constraint-solving for type parameters.

      • Steps:
        1. Synthesize types for $f$ and $\overline{e}$.
        2. Generate constraints:
          • $C$: Argument types $\overline{S}$ must be subtypes of expected parameter types $\overline{T}$.
          • $D$: Actual return type $R$ must be a subtype of expected type $V$.
        3. Solve the conjunction $\bigwedge C \wedge D$. If a solution (substitution $\sigma$) exists, type checking succeeds. Since this is a checking rule, we only require solution existence, not computation.

      Top and Bottom Types

      10. Checking - Top Type (Checking-Top)

      $$ \frac{\Gamma \vdash e \Rightarrow T}{\Gamma \vdash e \Leftarrow \top} \quad (\text{C-Top}) $$

      This rule switches from checking to synthesis mode. When checking $e$ against top type $\top$ (where all types are subtypes of $\top$), the check always succeeds. Since $\top$ provides no constraints, we directly synthesize $e$’s concrete type $T$.

      11. Synthesis - Application - Bottom Type (Synthesis-App-Bot)

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

      Special case when function type is $\bot$ (bottom type), representing non-terminating expressions (e.g., exceptions).

      • If $f$’s type is $\bot$, the application result is $\bot$ regardless of arguments.
      • Since $\bot$ is a subtype of all types (including function types), a $\bot$-typed expression can be applied as any function.

      12. Checking - Application - Bottom Type (Checking-App-Bot)

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

      Checking rule for $\bot$-typed functions.

      • If $f$ has type $\bot$, the application result is $\bot$.
      • Since $\bot$ is a subtype of any type $R$, the check always succeeds.

      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.

      2. Bidirectional Typing Code [blog/lti-english/bidi_code][edit]

        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.