Title: Polymorphic type inference for dynamic languages: reconstructing types for systems combining parametric, ad-hoc, and subtyping polymorphism
Friday, June 21th at 09:30 (Paris time, UTC+2)
Batiment Sophie Germain, 3rd floor, Room 3052 8 Pl. Aurélie Nemours, 75013 Paris
Zoom link: https://u-paris.zoom.us/j/83379216296?pwd=ZxYiEqpCprbs9leonLXgEbniPVmwXs.1 Meeting ID: 833 7921 6296 Passcode: 341938
Abstract. Programming languages can be broadly categorized into two groups: static languages, such as C, Rust, and OCaml, and dynamic languages, such as Python, JavaScript, and Elixir. While static languages generally offer better performance and more security thanks to a phase of static typing that precedes compilation ("well-typed programs cannot go wrong"), this often comes at the expense of flexibility, making programs safer but prototyping more tedious. In this defence, I present a formal system for statically typing dynamic languages, offering a compromise between safety and flexibility.
Statically typing dynamic languages poses new challenges. In particular, functions in dynamic languages can be overloaded: they can express multiple behaviors that cannot be resolved statically, but are instead selected at runtime (either by explicit type-cases or by built-in dynamic dispatch). In addition, programs typically have no (or few) type annotations. To address these problems, I present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types and subtyping, and provide an algorithm to automatically reconstruct (infer) the type of functions. This results in 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 intersection types) and that are deduced by applying advanced techniques of type narrowing (thanks to union types). This makes the system a prime candidate for typing dynamic languages.
The jury will be composed as follows.
Supervisors:
- Giuseppe Castagna, Directeur de recherche (IRIF, Paris)
- Kim Nguyen, Maître de conférences (LMF, Gif-sur-Yvette)
Jury:
- Amal Amhed, Professeure (Northeastern University, Boston)
- Delia Kesner, Professeure (IRIF, Paris)
- Didier Remy, Directeur de recherche (INRIA Paris-Rocquencourt)
- Alan Schmitt, Directeur de recherche (INRIA Rennes)
- Jan Vitek, Professeur (Charles University, Prague)
After the defence, a reception will take place in IRIF (Batiment Sophie Germain, 4th floor).