When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
This program is tentative and subject to change.
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, until now many basic problems remain open, such as how to type check expressions like (𝜆𝑥. (𝑥 123, 𝑥 True)) id reliably. We show that a type inference approach based on multi-bounded polymorphism, a form of implicit polymorphic subtyping with multiple lower and upper bounds, can help us resolve most of these problems in a uniquely simple and regular way. We define F{≤ }, a declarative type system derived from the existing theory of implicit coercions by Cretin and Rémy, and we introduce SuperF, a novel algorithm to infer polymorphic multi-bounded F{≤ } types while checking user type annotations written in the syntax of System F. We use a recursion-avoiding heuristic to guarantee termination of type inference at the cost of rejecting some valid programs, which thankfully rarely triggers in practice. We show that SuperF is vastly more powerful than all first-class-polymorphic type inference systems proposed so far, significantly advancing the state of the art in type inference for general-purpose programming languages.
This program is tentative and subject to change.
Fri 19 JanDisplayed time zone: London change
13:20 - 14:40 | |||
13:20 20mTalk | When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism POPL Lionel Parreaux Hong Kong University of Science and Technology, Aleksander Boruch-Gruszecki EPFL, Andong Fan The Hong Kong University of Science and Technology, Chun Yin Chau HKUST | ||
13:40 20mTalk | Parametric Subtyping for Structural Parametric Polymorphism POPL Henry DeYoung CMU, Andreia Mordido LASIGE, University of Lisbon, Frank Pfenning Carnegie Mellon University, USA, Ankush Das Amazon | ||
14:00 20mTalk | Unboxed data constructors -- or, how cpp decides a halting problem POPL Nicolas Chataing ENS Paris, Stephen Dolan Jane Street, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge | ||
14:20 20mTalk | Polymorphic Type Inference for Dynamic Languages POPL Giuseppe Castagna CNRS; Université Paris Cité, Mickaël Laurent Université de Paris, Kim Nguyễn Université Paris-Saclay |