Bidirectional type-checking

Bidirectional type-checking is a technique that splits usual type-checking in two phases:

the checking phase, where information from type annotations is propagated to smaller expressions), and
the synthesis phase (where known type information is propagated to bigger phrases, with attendant consistency checks).

Bidirectional type-checking is behind many practical implementations of type systems. For example, it is used by C#, Scala, and Haskell. It is a very old, folklore technique, whose origins are lost in the mists of time.

Bidirectional calculi

Expressing bidirectional type-checking as a formal type system or calculus leads to various interesting observations:

its structure seems to have a relationship with normal forms of the \lambda-calculus
it seems to correspond to polarized or focussed type theories

References

Bidirectional typing seems to have been introduced in the following two papers.

Lee, Oukseh, and Kwangkeun Yi. ‘Proofs about a Folklore Let-Polymorphic Type Inference Algorithm’. ACM Transactions on Programming Languages and Systems 20, no. 4 (1998): 707–23. https://doi.org/10.1145/291891.291892.

@article{lee_1998,
	title = {Proofs about a folklore let-polymorphic type inference algorithm},
	volume = {20},
	doi = {10.1145/291891.291892},
	pages = {707--723},
	number = {4},
	journaltitle = {{ACM} Transactions on Programming Languages and Systems},
	author = {Lee, Oukseh and Yi, Kwangkeun},
	date = {1998}
}

Pierce, Benjamin C., and David N. Turner. ‘Local Type Inference’. ACM Transactions on Programming Languages and Systems 22, no. 1 (2000): 1–44. https://doi.org/10.1145/345099.345100.


@article{pierce_local_2000,
	title = {Local type inference},
	volume = {22},
	doi = {10.1145/345099.345100},
	pages = {1--44},
	number = {1},
	journaltitle = {{ACM} Transactions on Programming Languages and Systems},
	author = {Pierce, Benjamin C. and Turner, David N.},
	date = {2000}
}

A recent survey of the technique is presented in

Dunfield, Jana, and Neel Krishnaswami. ‘Bidirectional Typing’. ACM Computing Surveys 54, no. 5 (2022): 1–38. https://doi.org/10.1145/3450952.

@article{dunfield_2022,
	title = {Bidirectional Typing},
	volume = {54},
	doi = {10.1145/3450952},
	pages = {1--38},
	number = {5},
	journaltitle = {{ACM} Computing Surveys},
	author = {Dunfield, Jana and Krishnaswami, Neel},
	date = {2022}
}

See also

Christiansen, David Raymond. ‘Bidirectional Typing Rules: A Tutorial’. Tutorial, 17 October 2013. http://davidchristiansen.dk/tutorials/bidirectional.pdf.

Christiansen, David Raymond. ‘Checking Dependent Types with Normalization by Evaluation: A Tutorial’. Tutorial, 2018. http://davidchristiansen.dk/tutorials/nbe/.

Christiansen, David Raymond. ‘Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version)’. 21 May 2019. http://davidchristiansen.dk/tutorials/implementing-types-hs.pdf.

Pfenning, Frank. ‘Lecture Notes on Bidirectional Type Checking’. Lecture Notes, 21 October 2004. https://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf.