The translation of a high level, user friendly surface language into a small, typed core language is a useful pattern for implementing typed programming languages. We call this elaboration because it fills in details that were otherwise implicit, and it is used in the implementations of languages such as GHC Haskell, Idris and Coq.
Unfortunately elaborators can get rather complicated because type checking,
desugaring and error reporting are all fused together.
This project explores a way to alleviate this burden on the elaborator by
taking an LCF-inspired approach for the core language.
Instead of type checking and constructing core terms within the elaborator, we
instead move this behind trusted inference rules defined in the core
(see core.mli).
Elaboration no longer needs to interact with core terms directly, and can
instead focus on desugaring and error reporting (see surface.ml).
- Elaboration of lambda terms
- Elaboration tests
- Unification and metavariables
- Collect multiple errors during elaboration
- LCF architecture on PLS Lab
Presentations:
- Robert Atkey, “An Algebraic Approach to Typechecking and Elaboration” (URL)
- Andrej Bauer, “Derivations as computations”, ICFP’19 (Video) (URL) (Slides)
- John Harrison, “The LCF Approach to Theorem Proving” (Slides)
Related projects:
- jonsterling/dreamtt: Pedagogic abstract elaboration for dependent type theory.
- RedPRL/cooltt: Elaboration for Cartesian cubical type theory.
- RedPRL/algaett: Elaborator for dependent type theory using effects and handlers.
- TOTBWF/MicroTT.ml: A simple single-file elaborator for MLTT.
- TOTBWF/teenytt A very small, didactic proof assistant for dependent type theory.