Bidirectional type checking

Deep dive

How it works

Parts:

• synth(Γ, e) → T — type read off the term: variable, literal, annotation, application.
• check(Γ, e, T) — expected type is an input: lambda, if, and the fallback rule.
• context Γ — stack of name : type; checking a lambda pushes the binder with the type from the expected function type.
• mode switch (subsumption) — check on any other term calls synth, then tests inferred <: expected (equality without subtyping).
• annotation (e : T) — the reverse switch: synth calls check(e, T) and returns T.

check(Γ, e, T):

1. λx. b with T = A → B: check b against B in Γ, x : A; if T is not a function type, error.
2. if c then t else f: check c against Bool, then t and f against T.
3. Otherwise U = synth(e); accept iff U <: T.

synth(Γ, e):

1. Variable: lookup. Literal: base type. (e : T): check(e, T), return T.
2. f a: synth(f) must be A → B; check(a, A); return B.
3. Unannotated lambda: fail with "add an annotation" (some systems guess a monotype instead).

 check ──(lambda, if)──► pushes T inwards       annotation (e : T): synth calls check
   ▲                                                       │
   └─── mode switch: U = synth e, then U <: T ◄── synth ◄──┘ (var, app, literal)

Where users annotate. Top-level definitions, let-bound lambdas not applied at once, and a redex (\x. b) a (lambda in synthesis position; write ((\x. b) : A → B) a). Lambdas passed as arguments, returned from annotated functions or stored in annotated fields need nothing. Rule of thumb: an annotation is needed where an introduction form meets an elimination form directly.

Origins. Pierce and Turner's Local Type Inference (TOPLAS 2000) combines this propagation with local inference of omitted type arguments, for System F-like languages with subtyping. Dunfield and Krishnaswami (ICFP 2013) give a small algorithm for predicative higher-rank polymorphism. Its context is ordered and holds universals α, unsolved existentials α^ and solved ones α^ = τ; instantiating a ∀ in synthesis adds a fresh α^, subtyping solves it, and a solution may only mention variables earlier in the context, which keeps scoping sound. Their survey Bidirectional Typing (Computing Surveys 2021) maps the design space.

Versus Hindley-Milner. HM gives each binder a fresh variable and solves all equations by unification: principal types with no annotations, but an error appears wherever two constraints finally clash. Bidirectional checking never invents a binder type, needs no unifier for the core system, loses principality (annotations decide) and gains locality. Real checkers mix both.

Code

STLC with Bool, Int, unannotated lambdas, if, application and annotation; compiled and run with the asserts in main.

use std::rc::Rc;

#[derive(Clone, Debug, PartialEq)]
pub enum Ty { Bool, Int, Fun(Rc<Ty>, Rc<Ty>) }

pub enum Term {
    Var(String),
    Bool(bool),
    Int(i64),
    Lam(String, Box<Term>),            // no annotation on the binder
    App(Box<Term>, Box<Term>),
    If(Box<Term>, Box<Term>, Box<Term>),
    Ann(Box<Term>, Ty),                // (e : T)
}

type Ctx = Vec<(String, Ty)>;          // innermost binding last
type Res<T> = Result<T, String>;

fn fun(a: Ty, b: Ty) -> Ty { Ty::Fun(Rc::new(a), Rc::new(b)) }

/// Synthesis mode: the term determines its own type.
pub fn synth(ctx: &mut Ctx, e: &Term) -> Res<Ty> {
    match e {
        Term::Var(x) => ctx.iter().rev().find(|(n, _)| n == x)
            .map(|(_, t)| t.clone()).ok_or(format!("unbound {x}")),
        Term::Bool(_) => Ok(Ty::Bool),
        Term::Int(_) => Ok(Ty::Int),
        // The annotation is the only place a type enters from the user.
        Term::Ann(e, t) => { check(ctx, e, t)?; Ok(t.clone()) }
        Term::App(f, a) => match synth(ctx, f)? {
            // Function type is known, so the argument is *checked* against it.
            Ty::Fun(dom, cod) => { check(ctx, a, &dom)?; Ok((*cod).clone()) }
            t => Err(format!("applying non-function of type {t:?}")),
        },
        Term::If(c, t, f) => {
            check(ctx, c, &Ty::Bool)?;
            let ty = synth(ctx, t)?;      // first branch decides, second must agree
            check(ctx, f, &ty)?;
            Ok(ty)
        }
        Term::Lam(x, _) => Err(format!("cannot infer \\{x}: add an annotation")),
    }
}

/// Checking mode: the expected type is pushed inwards.
pub fn check(ctx: &mut Ctx, e: &Term, want: &Ty) -> Res<()> {
    match (e, want) {
        (Term::Lam(x, body), Ty::Fun(dom, cod)) => {
            ctx.push((x.clone(), (**dom).clone()));  // binder type comes from `want`
            let r = check(ctx, body, cod);
            ctx.pop();
            r
        }
        (Term::Lam(..), t) => Err(format!("lambda checked against non-function {t:?}")),
        (Term::If(c, t, f), _) => {
            check(ctx, c, &Ty::Bool)?;
            check(ctx, t, want)?;
            check(ctx, f, want)
        }
        // Mode switch (subsumption): synthesize, then compare. With no subtyping
        // "inferred <: expected" is plain equality.
        _ => {
            let got = synth(ctx, e)?;
            if &got == want { Ok(()) } else { Err(format!("expected {want:?}, found {got:?}")) }
        }
    }
}

fn lam(x: &str, b: Term) -> Term { Term::Lam(x.into(), Box::new(b)) }

fn main() {
    let ib = fun(Ty::Int, Ty::Bool);
    let id = lam("x", Term::Var("x".into()));
    let mut c = Ctx::new();
    // Unannotated lambda checks against an expected type...
    assert!(check(&mut c, &id, &fun(Ty::Int, Ty::Int)).is_ok());
    // ...but cannot be synthesized.
    assert!(synth(&mut c, &id).unwrap_err().contains("annotation"));
    // ((\x. x) : Int -> Int) 3 : Int
    let app = Term::App(Box::new(Term::Ann(Box::new(id), fun(Ty::Int, Ty::Int))), Box::new(Term::Int(3)));
    assert_eq!(synth(&mut c, &app), Ok(Ty::Int));
    // if in check mode pushes the lambda type into both branches
    let iff = Term::If(Box::new(Term::Bool(true)),
        Box::new(lam("n", Term::Bool(false))), Box::new(lam("n", Term::Bool(true))));
    assert!(check(&mut c, &iff, &ib).is_ok());
    // ill-typed: argument mismatch is reported at the application argument
    let bad = Term::App(Box::new(Term::Ann(Box::new(lam("n", Term::Bool(true))), ib.clone())),
                        Box::new(Term::Bool(false)));
    assert_eq!(synth(&mut c, &bad).unwrap_err(), "expected Int, found Bool");
    // ill-typed: wrong body type under the annotation
    let bad2 = Term::Ann(Box::new(lam("n", Term::Var("n".into()))), ib);
    assert_eq!(synth(&mut c, &bad2).unwrap_err(), "expected Bool, found Int");
    // ill-typed: if branches disagree
    let bad3 = Term::If(Box::new(Term::Bool(true)), Box::new(Term::Int(1)), Box::new(Term::Bool(false)));
    assert!(synth(&mut c, &bad3).is_err());
    println!("ok");
}

Complexity and constants

• Each node is visited once per mode switch and annotations cut the chain: O(n) overall. Context lookup is O(depth) for a Vec scan, O(1) with de Bruijn indices (De Bruijn indices).
• Cost drivers: allocating or cloning types on every synth result, context push/pop per binder, and type-equality or subtyping tests on large types. Intern types and compare ids.

Efficiency

• Cost: one tree walk, no substitution pass, no global constraint set: time linear in term size, memory proportional to depth plus the types built. Bound: allocation and pointer chasing, not arithmetic. Not benchmarked here.
• Levers:
  • intern types as integers — equality is one compare and synth copies a word (not measured) — nearly always.
  • de Bruijn or persistent context — O(1) lookup and cheap scope exit (design argument) — deep scopes.
  • check each annotated top-level definition independently — parallel and cacheable by body hash (design argument) — large codebases, incremental builds.
• Naive → standard → state of the art: substitute and retype each application · can be quadratic or worse; one-pass check/synth with a stack context · O(n); interned types, de Bruijn contexts and per-definition caching in an incremental engine · near-linear with warm caches (design claim, not measured).

Implementation notes

• Two functions keep rules readable; one function with Mode::Check(T) | Mode::Synth shares code for if and blocks.
• Return an elaborated term (inserted coercions, type arguments, implicit arguments), not only a type: the main reason Lean, Agda and Idris are bidirectional.
• Push expected types into every result position: if/match arms, let bodies, block tails, tuple and array elements, struct fields. A missed one forces surprising annotations.

Pitfalls

• Synthesizing a lambda: fail clearly, or guess monotype existentials (needs a solver, may reject valid programs). Never silently default.
• if in synthesis mode: the first branch decides and the second is blamed; checking against an expected type removes the asymmetry.
• check falling to synth before the lambda case makes lambdas unusable in check mode.

Variants and alternatives

In production

• Language compilers: TypeScript contextual typing gives lambda parameters the type of the surrounding call or declaration (handbook). Rust closures get parameter types from the expected Fn* bound; Scala 3 infers lambda parameter types from the expected type.
• Editor and static-analysis tools: Pyright (the Pylance engine) infers with an "expected type" taken from the declared left-hand side (docs).
• Proof assistants: Lean 4 elaborates terms against expected types, falling back to synthesis, and inserts implicit arguments (reference); Agda and Idris 2 work the same way.
• Databases: PostgreSQL resolves an unknown-typed literal or parameter from the other operand of an operator (docs), the same expected-type flow in a SQL analyzer.

Implementations

Sources

• Pierce, Turner, Local Type Inference, ACM TOPLAS 22(1), 2000. pdf
• Dunfield, Krishnaswami, Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, ICFP 2013. arXiv
• Dunfield, Krishnaswami, Bidirectional Typing, ACM Computing Surveys 54(5), 2021. arXiv
• Peyton Jones, Vytiniotis, Weirich, Shields, Practical type inference for arbitrary-rank types, JFP 17(1), 2007. paper