Distributive subtyping is a thorny topic in the theory of type systems, which nevertheless has many important practical implications. Languages like Scala distribute intersections over function types in a way that would be unsound when done in languages like TypeScript. In turn, this prevents Scala from supporting not only intersection-based overloading but also, more subtly, any implicit form of first-class polymorphism. On the other hand, languages like MLsub distribute intersections like Scala but have no problem with implicit polymorphism because their polymorphism is not first-class. TypeScript-style polymorphism is first-class and implicit. It turns out this is compatible with distributing intersections over unrelated constructed types, such as generic class types, unless one also wishes for polymorphic types to distribute over functions in the expected way, from which unsoundness would ensue even in the absence of imperative effects. Clearly, the design space for distributive subtyping is vast and contains many pitfalls; surprisingly, it has not been systematically explored in a languageagnostic way, so these pitfalls are not well-known nor well-documented and must be rediscovered over and over. I aim to shed some light on these issues for the benefit of programming language and type system designers, especially those who may not be familiar with the plethora of existing literature on subtyping as well as those who have not yet committed to one particular school of subtyping. I will notably show that many of the distinctions in that design space can be attributed to the usual Church/Curry semantic divide.

I am an Assistant Professor at the HKUST CSE department since February 2021. I am looking for students to join my research group! Please contact me (first-name dot last-name at gmail.com) if you’d like to work on something related to programming languages, type systems, or compiler optimization.

I obtained my PhD in 2020 from EPFL, in the Data Analysis Theory and Applications Laboratory (DATA), where I created the Squid type-safe metaprogramming library for Scala.