IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2024 > Record polymorphism for set-theoretic types

Loïc Peyrot

Tuesday, January 23, 2024

11:00am 302-Mountain View and Zoom4 (https://zoom.us/j/4911012202, password:@s3)

Loïc Peyrot, Post-doctoral Researcher, IRIF (Université Paris Cité)

Record polymorphism for set-theoretic types

Abstract:

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.