Bidirectional type checking, from scratch

Hindley–Milner gets taught as the way to do type inference: unify everything, generalise at let-bindings, never write an annotation. Then you look at a real checker — TypeScript, Rust, Swift, Idris — and none of them work that way. They all use some flavour of bidirectional type checking, and the reason is worth understanding.

#Two judgements instead of one

Full inference asks one question: what is the type of this term? Bidirectional checking splits it in two.

• Synthesis (e ⇒ A) — read a type out of the term. Used when the term is self-describing.
• Checking (e ⇐ A) — push an expected type into the term. Used when context already knows what's wanted.

// Synthesise: the term tells us its type
declare function synth(ctx: Context, term: Term): Type;
 
// Check: we tell the term its type, and it either fits or it doesn't
declare function check(ctx: Context, term: Term, expected: Type): void;

The two are mutually recursive, and the whole design is about deciding which mode each syntactic form belongs in.

#The rule of thumb

Introduction forms — lambdas, tuples, record literals, empty lists — get checked. They're the shapes that are ambiguous on their own. Elimination forms — variables, applications, field access, annotations — get synthesised. They bottom out at something whose type is already known.

#Why a lambda can't synthesise

Consider the identity function with no annotation:

const f = (x) => x;

There is no single right answer. It could be number => number, string => string, or the polymorphic forall a. a => a. Hindley–Milner picks the last one by generalising, which works beautifully until the language grows subtyping or higher-rank types — then the "most general type" either doesn't exist or isn't unique.

Bidirectional checking sidesteps the question. A lambda is only ever checked against a known function type, and then the binder's type falls straight out:

function check(ctx: Context, term: Term, expected: Type): void {
  if (term.kind === "lambda") {
    if (expected.kind !== "function") {
      throw new TypeError(`Expected ${show(expected)}, got a function`);
    }
    // The parameter type is *given*, not guessed. Bind it and
    // check the body against the known result type.
    check(ctx.extend(term.param, expected.from), term.body, expected.to);
    return;
  }
 
  // ...other checking rules
  subsumption(ctx, term, expected);
}

This is exactly the behaviour you already rely on. Write arr.map((x) => x.trim()) and x is a string, because the expected type flowed inward from map's signature. Write the same lambda standalone and you get an implicit-any error. That asymmetry isn't a wart — it's the mode split showing through.

#Where the modes meet

Eventually a checked position contains a term that can only synthesise. That's where the two judgements connect, via the subsumption rule: synthesise a type, then confirm it's compatible with what was expected.

function subsumption(ctx: Context, term: Term, expected: Type): void {
  const actual = synth(ctx, term);
  if (!isSubtype(actual, expected)) {
    throw new TypeError(
      `Type ${show(actual)} is not assignable to ${show(expected)}`,
    );
  }
}

In a system with no subtyping this is just equality. With subtyping it's where variance lives. Either way, it is the only place the checker compares two types it derived independently — which makes it the only place that needs to produce a good error message.

#Annotations are mode switches

An annotation is the escape hatch that turns a checkable term into a synthesisable one:

function synth(ctx: Context, term: Term): Type {
  switch (term.kind) {
    case "var":
      return ctx.lookup(term.name);
 
    case "annotation":
      // Check the inner term against the ascription, then hand
      // that type back up as the synthesised result.
      check(ctx, term.term, term.type);
      return term.type;
 
    case "application": {
      const fnType = synth(ctx, term.fn);
      if (fnType.kind !== "function") {
        throw new TypeError(`${show(fnType)} is not callable`);
      }
      check(ctx, term.arg, fnType.from);
      return fnType.to;
    }
  }
}

Note the application rule: the function is synthesised, the argument is checked. That ordering is why argument types flow into lambdas but not the other way, and why overload resolution has to happen before argument checking rather than during it.

#What you get out of the split

That last row matters more than it sounds. Under unification, a mistake in one branch surfaces as a confusing failure in another — the classic "expected number, got string" pointing at code you never touched. Under bidirectional checking, the expected type is already known when the checker reaches the bad term, so the error lands on the term itself.

#The practical takeaway

If you're building a checker, resist the urge to make everything synthesise. Decide the mode for each form up front, keep the subsumption rule as the single meeting point, and require annotations exactly where a term is ambiguous in isolation. You end up with a checker that is easier to implement, easier to extend, and — because the expected type is nearly always in hand — far better at explaining itself.