Abstract

Type inference in the presence of first-class or “impredicative” second-order polymorphism à la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, previous solutions to this problem have been quite limited in power and flexibility. For example, it was not clear how to type check expressions like (𝜆𝑥. (𝑥 123, 𝑥 True)) id reliably. This talk introduces SuperF, a new approach based on multi-bounded polymorphism, a form of implicit polymorphic subtyping with multiple upper and lower bounds. SuperF significantly improves on the state of the art in type inference for first-class polymorphism while remaining relatively simple and regular. This talk also discusses a practical implementation of SuperF in the MLscript programming language, together with the existing approach of Boolean-algebraic type inference, and suggests applications in statically guaranteeing the scope safety properties of various programming constructs.

Bio: Lionel Parreaux is an Assistant Professor at HKUST (The Hong Kong University of Science and Technology) since February 2021. He works primarily on type systems, programming language design, and compilers. Together with his research team, the TACO Lab, he is developing the MLscript programming language. He obtained his PhD in 2020 from EPFL , in the Data Analysis Theory and Applications Laboratory (DATA), where he created the Squid type- and scope-safe metaprogramming library for Scala.