THE BIDIRECTIONAL TYPING two modes: check against a known type, or synthesize an unknown one
Full type inference can be undecidable once types get rich; bidirectional typing is the practical discipline that keeps checking simple. It splits into two modes: check a term against a type you already know (a lambda against a function type), and synthesize a type from a term you don't (the type of a variable, or of an application from its function). The two modes call each other — synthesize the function, check the argument — and this handshake type-checks even higher-rank and dependent systems with a clear, local algorithm and readable error messages. It is how most modern checkers actually work.
THE TECHNIQUE synthesize f : A→B, check x : A, conclude (f x) : B
Application typing, bidirectionally: synthesize the function's type, check the argument against its domain, yield the codomain. The demo types f x with type-tags: live demo
HISTORY & CREDIT folklore · Pierce-Turner 1998/2000
“A type checker either infers everything or you annotate everything.” — the middle path is best: know some types, synthesize the rest, and let the two directions meet. Bidirectional typing is why real checkers give local, legible errors instead of a global “unification failed.” cited
1980s–90s · folklore among language and proof-assistant developers; Thierry Coquand (1996) uses bidirectional checking for dependent types. 1998–2000 · Benjamin Pierce & David Turner — “Local Type Inference” (POPL 1998; TOPLAS 2000): name and systematize the check/synthesize discipline as local type inference (they call the idea itself folklore). now · Dunfield & Krishnaswami survey it; the standard skeleton of typecheckers for rich systems.
Two modes that call each other turn an undecidable global search into a decidable local walk. The annotations you must write are exactly the places synthesis cannot reach. Pierce-Turner 2000
RECOMMEND FOR I-13 application typing, computed
On the canonical compiler, with f : Int→Bool, applying it to an Int synthesizes Bool(2); applying it to a Bool is rejected (0):
$ i13 run t_bidirectional.i13 # synth (f x): check x against f's domain
synth_ok = 2 -- x:Int matches Int->Bool's domain -> result Bool
synth_illtyped = 0 -- x:Bool != Int -> rejected
Recommend: bidirectional typing is the algorithm i13 would use if it ever grew types — and it is a good fit for its ethos. It is single-pass-friendly (a local walk, no global constraint soup), it produces the clear file:line:col errors i13 already prizes, and its “check vs synthesize” split mirrors i13's own “COVERED vs NOT COVERED” honesty. i13 doesn't do it today (one type, nothing to synthesize), but of the whole batch this is the mechanism most compatible with a single-pass, diagnostics-first validator.