A framework for erased syntax and bidirectional typing

We introduce CompLF, a logical framework allowing for the definition of computational type theories -- that is, those whose definitional equality is purely generated by rewrite rules. Its main goal is to capture the usual presentation of type theories in a faithful way. Whereas other frameworks impose a fully-annotated presentation of syntax, quite different from the ones used in practice, our proposal allows the definition of dependent type theories with their usual non-annotated syntaxes. This is achieved by the introduction of erased arguments, which correspond to premises of typing rules that are not recorded in the syntax. If on the one hand erased arguments allow us to capture the usual syntax of type theories, they can easily break decidability of type checking, as one might need to guess the erased information. We address this by proposing a bidirectional typing algorithm for CompLF. When comparing it with other algorithms in the literature, its main novelty is that it is not designed for a specific theory, but is instead generic and can be instantiated with various type theories. Moreover, it features a modular proof of completeness, in which one can fine-tune the subset of terms for which it is complete by varying the amount of annotations in the syntax. In particular, we can capture in a single framework the two main approaches for bidirectional typing, in which one reduces the amount of annotations to the minimal by restricting completeness only to normal forms, or in which one trades minimality of annotations in exchange for full completeness. Finally, CompLF is designed to be not only a theoretical tool but also a practical one: it has been implemented in a prototype that is openly available on GitHub.