The PhD seminar is a monthly lab event open to any non-permanent member of the LMF. PhD students, interns, post-docs, and engineers are all welcome to attend the presentation and lunch.
📢 Speaker: Marin Costes
Past editions
We often divide programming languages into two categories: those that are strongly-typed but rigid, and those that are more flexible but untyped (or dynamically typed). While static typing offers formal guarantees about the soudness of programs ("well-typed programs cannot go wrong") and can be used for the documentation and the tooling (auto-completion, etc), this often comes at the expense of flexibility, making programs more secure but prototyping more tedious. In this presentation, we study a formal system to statically type dynamic languages such as Python or Javascript, offering a compromise between safety and flexibility.
The static typing of dynamic languages raises new challenges. In particular, in dynamic languages, functions can be overloaded: they can express multiple behaviors that cannot be resolved statically, but instead are selected at runtime (dynamic dispatch). Some work aims to extend these languages with static typing (e.g. Typescript for Javascript), but lacks a formalization and an algorithm for infering type without needing annotations from the programmer.
To address this issue, we present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types, and subtyping. This yields a type discipline in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can capture the overloaded behavior of the functions they type (thanks to the intersection types) and that are deduced by applying advanced techniques of type narrowing (thanks to union types). This makes the system a prime candidate to type dynamic languages.
Dependent type theory is the logical foundation of many popular proof assistants, such as Coq, Agda and Lean. However, when presented in its most primitive form, the syntax of type theory suffers from a serious usability problem: every type annotation must be explicitly spelled out, rendering it unusable in practice. In order to solve this, usual presentations of type theory omit the majority of these annotations, but this has a cost. Because knowing them is still important when typing terms, it becomes unclear how to do this algorithmically.
A solution to this problem is provided by bidirectional typing, a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal.
In this talk I will give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which I define declarative and bidirectional type systems. I then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with various theories.