Type systems are often presented in a declarative style, but with an emphasis on ensuring that there is some sort of type synthesis algorithm. Since Pierce and Turner’s “Local Type Inference” system, however, there has been a small but growing alternative: bidirectional typing, where types are synthesized for variables and elimination forms, but must always be proposed in advance for introduction forms and checked. You can still get away without any type annotations, as long as you write only normal forms. But where’s the fun in that? If you want to write terms that compute, you need to write type annotations at exactly the point where an introduction form collides with its elimination form, showing exactly the type at which computation is happening.

For type systems with some sorts of value dependency, the bidirectional approach seriously cuts down on the amount of annotation required in terms, needed only to achieve type synthesis. We have a real opportunity to reduce clutter and also to give a clearer account of the connections between types and computation.

But it doesn’t stop there. A disciplined approach to the construction of bidirectional type systems makes it easier to get their metatheory right. I’ll show this by reconstructing Martin-Löf’s 1971 type theory (the inconsistent one) in a bidirectional style and show why it has type
preservation, even without normalization.

Abstract
Dependent types are increasingly used in functional programming languages. The surface syntax of dependent types, as seen by a programmer, is elaborated by a compiler into an internal, type-theoretic representation. In order to perform this step, the compiler needs to infer a nontrivial amount of information to successfully type-check the internal representation. This process—type refinement—is complex, implementation dependent, and very few formal developments currently exist. We discuss a novel and simpler formalisation of type refinement in first order type theory with dependent types. We propose a translation of type-refinement problems to Horn-Clause logic with explicit proof-terms, using proof-relevant resolution as the type inference mechanism.

Adam Barwell (adb23) will be presenting a summary of his recently submitted thesis.