Loïc Peyrot, Post-doctoral Researcher, IRIF (Université Paris Cité)
A strong argument in favour of dynamically-typed programming languages is their flexibility, enabling quick code writing and prototyping. But this is also a weakness, as many bugs are only detected when executing the program. Hence, statically-typed versions of well-known languages are in rapid expansion, such as Typescript or Luau. To guarantee the safety of a program without sacrifing expressivity, augmenting types with set operations, such as union and intersection, has proven very useful. Considering those set-theoretic operators naturally leads to so-called semantic subtyping: types are interpreted as sets, union and intersection types with the corresponding set operators, and subtyping is derived from set inclusion in the interpretation. Systems with semantic subtyping and set-theoretic types now support first-order polymorphism à la ML, a powerful programming abstraction. This kind of polymorphism however, is not sufficient when considering a language with extensible records (or structs), as it does not capture precise enough typings. In this talk, I will give an introduction to type systems with set-theoretic types and semantic subtyping. I will showcase some programs with typing failures, and show how the addition of row polymorphism for records solves the problem. I will then describe how we integrated row polymorphism to a type system with set-theoretic types, semantic subtyping and first-order polymorphism.