Bidirectional type-checking is a technique that splits usual type-checking in two phases:
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.
Expressing bidirectional type-checking as a formal type system or calculus leads to various interesting observations:
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}
}
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}
}
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.