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.