Now: Bidirectional Type Checking

Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program.

This approach — check an expression against a type when we know what type to expect, synthesize a type from an expression when we don't — is called bidirectional type checking, so named because type information flows in two directions in the abstract syntax tree: from leaves to root when synthesizing, from root to leaves when checking.

The two core judgments in any bidir system:

Generally, for constructors of a type we can propagate the type information downward into the term, which means it should be used in the checking judgment (e ↓ τ). Conversely, the destructors generate a result of a smaller type from a constituent of larger type and can therefore be used for synthesis, propagating information upward.

The key subsumption rule that switches modes:

The Sub rule is what lets you switch from synthesis to checking — if you can synthesize a type A for e, and A is a subtype of the expected B, you're done.

Great intro! I want to jump straight to what I think is the most underrated advantage of bidir: error messages.

An advantage bidirectional type checking has over the Hindley-Milner inference algorithm is that we can give a more specific error than simply 'failed to unify types A and B'. One of the commonly cited disadvantages of bidirectional type inference is that we need to sometimes include type annotations in places where it seems obvious.

In HM, when unification fails, you often get a spooky "Cannot unify α3 with Int → β7" message where the type variables have been unified across the whole program. You lose locality completely. In bidir, when checking mode fails, you know exactly where the mismatch happened and what type was expected — that's just structural.

Also want to clarify the annotation burden question. One of the commonly cited disadvantages of bidirectional type inference is that we need to sometimes include type annotations in places where it seems 'obvious'. However: if we extend our language with let-bindings with type annotations and force everything at the top level to be a let-binding, then we should almost never need another type annotation in the body of the let bindings! This restriction isn't unrealistic for a language.

Honestly for any serious language I'd argue the top-level sig discipline is a feature, not a bug. It makes code self-documenting.

I'll add the formal perspective. The key reason bidir dominates in dependent type theory is decidability and subtyping.

If you try to extend Hindley-Milner type inference to add any other language feature that requires subtyping, you run into issues pretty quickly. This is because Hindley-Milner exploits a cute hack that does not generalize well.

In contrast, bidirectional type-checking is not just a method for handling implicit type abstraction/application. Rather, bidirectional type-checking is a framework for introducing any form of subtyping, of which implicit type abstraction/application is just a special case.

The key paper here is Dunfield & Krishnaswami (2013), "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism." Also the so-called "Pfenning recipe" yields a set of bidirectional typing rules that is small and whose annotation discipline is moderately lightweight and highly predictable.

For HM, the limitation is well-understood: in HM type systems, universal quantification can only appear at the top level. This lifts a restriction that prevents higher-rank polymorphism. Concretely, if you want a function that takes a polymorphic argument like ∀a. a → a at rank 2, HM chokes. Bidir handles it cleanly.

The Anno rule is what makes bidir "escape" into synthesis anywhere — you just annotate the term. HM has no equivalent because it doesn't have checking mode at all.

Wait, question — I've heard "local type inference" used almost synonymously with bidirectional. Are they the same thing?

Related but distinct! The term "local type inference" (Pierce and Turner 2000) implies that bidirectional typing should focus on (or even be restricted to) local information, suggesting that annotation disciplines should not need global information.

Local type inference is a pragmatic approach. It is not aimed to provide the same degree of type inference that is possible in languages with Hindley-Milner type inference. Instead, as Pierce and Turner state, the goal is to "exchange complete type inference for simpler methods that work well in the presence of more powerful type-theoretic features such as subtyping and impredicative polymorphism".

In local type inference, the main design decision that is made to simplify type inference is to avoid forms of global type inference that employ long-distance constraints such as unification variables.

So: local type inference is a philosophy/design constraint. Bidirectional is the mechanism usually used to implement it. You can have bidir systems that still use long-distance unification (like "Complete and Easy") — those aren't strictly "local" anymore but still benefit from the checking/synthesis structure.

I want to address the "are they mutually exclusive?" question that always comes up. They're not.

When facing down designing a type system, knowing if you need unification or not decides a lot for you. Unification sits center stage in Hindley-Milner. When you pick HM you pick unification.

If you look to the literature, you'll find plenty of examples of bidirectional typing without unification in sight. By introducing annotations at key locations, you can type check sophisticated programs with no type variables. A key insight of bidirectional typing is how much you can do without unification.

BUT — and this is important — you can absolutely combine them. A combination of the two — a bidirectional typing system with unification — will be the best approach in many cases. In fact, if you are going to choose a Hindley-Milner type system, you might as well add a few lines of code and make it a bidirectional system.

Here's the combined approach in pseudocode:

The weakness of pure bidirectional typing systems is that they do not talk about "partially-known" types. Bidirectional typing systems require "complete" types, but the inference rules of the lambda calculus fundamentally give us partial information about types. Unification fills exactly that gap.

Good points all around. Let me add a practical comparison table:

A few languages use Hindley-Milner type inference, such as Rust, Haskell, and F#. What bidirectional type checking is used in includes TypeScript, Scala, and others.

One thing I didn't list: Hindley-Damas-Milner inference typically provides a stronger form of principality — the property that type inference never "chooses" among incompatible, valid types for subexpressions. Bidir can sometimes be ambiguous about which type to synthesize in certain cases. That's a real tradeoff.

Really appreciate that table!! One thing I'm confused about — why can't HM just... infer dependent types? Like what's the actual theoretical blocker?

Wonderful question. The short answer: type checking becomes undecidable once types can depend on terms, because you'd need to evaluate arbitrary programs at compile time. HM's whole power comes from working purely in a stratified world where terms and types are separate layers.

In dependent types, you might have something like Vec A n where n : ℕ is a term. Checking Vec A (f 3) ~ Vec A (g 2) reduces to checking f 3 = g 2 — but f and g can be arbitrary programs! Deciding that requires deciding program equality, which is undecidable in general.

In complexity theory, it is often relatively easy to check that a given solution is valid, but finding (synthesizing) a solution may be complex or even undecidable. This general rule holds for type systems: synthesizing types may be convenient for the programmer, but computationally intractable.

To go beyond the specific feature set of traditional Damas–Milner typing, it might seem necessary to abandon synthesis. Instead, however, we can combine synthesis with checking. In this approach — bidirectional typing — language designers are not forced to choose between a rich set of typing features and usability.

Bidir handles this by making the programmer provide enough annotations so the checker can verify without needing to invent types from scratch. The ⇒/⇐ discipline gives you a principled way to decide exactly where annotations are mandatory.

One more concept worth covering: mode-correctness, which is the formal property that makes a bidirectional system actually work as an algorithm.

As Dunfield and Krishnaswami outlined, mode-correctness for a bidirectional typing rule means that (i) each 'input' type variable in a premise must be an 'output' variable in 'earlier' premises, or provided by the conclusion if the rule is checking; (ii) each 'output' type variable in the conclusion should be some 'output' variable in a premise if the rule is synthesising.

The algorithm of a bidirectional type synthesiser can often be 'read off' from a well-designed bidirectional type system: as the synthesiser traverses a raw term, it switches between synthesis and checking, following the modes assigned to the judgements in the typing rules.

This is the beautiful part: if your rules are mode-correct, the implementation almost writes itself. You get two mutually recursive functions synth and check, and the rules directly correspond to pattern match arms. No unification variable management, no occurs-check headaches, no backtracking.

Compare that to implementing Algorithm W, where you have to thread a substitution through everything and apply it carefully. It's not hard, but it's much more stateful.

This thread is making me so much smarter omg. So for someone building a new language in 2025 — just go bidir? Or does HM still make sense?

My take after all this research: bidir + unification is the sweet spot for most new languages. Here's my decision tree:

If you're in the "no subtyping, no deptype, yes ML-style" space, HM is absolutely still valid and time-tested. Hindley-Milner doesn't combine easily with subtyping and union types, but if you don't need those, you're fine.

The rest of the replies are more deep dives — click to next page for discussion on constraint-based inference, GHC's OutsideIn(X), and how Lean 4 does it.