When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin Chau
Abstract
Type inference in the presence of first-class or “ impredicative ” second-order polymorphism à la System <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="normal">F</mml:mi> </mml:math> 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mo stretchy="true">(</mml:mo> <mml:mi mathvariant="italic">λ</mml:mi> <mml:mi mathvariant="italic">x</mml:mi> <mml:mo>.</mml:mo> <mml:mo stretchy="true">(</mml:mo> <mml:mi>x</mml:mi> <mml:mtext> </mml:mtext> <mml:mtext> </mml:mtext> <mml:mn>123</mml:mn> <mml:mo>,</mml:mo> <mml:mtext> </mml:mtext> <mml:mi>x</mml:mi> <mml:mtext> </mml:mtext> <mml:mtext> </mml:mtext> <mml:mtext>True</mml:mtext> <mml:mo stretchy="true">)</mml:mo> <mml:mo stretchy="true">)</mml:mo> </mml:math> 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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msub> <mml:mi mathvariant="normal">F</mml:mi> <mml:mfenced close="}" open="{"> <mml:mo>≤</mml:mo> </mml:mfenced> </mml:msub> </mml:math> , a declarative type system derived from the existing theory of implicit coercions by Cretin and Rémy (LICS 2014), and we introduce SuperF, a novel algorithm to infer polymorphic multi-bounded <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:msub> <mml:mi mathvariant="normal">F</mml:mi> <mml:mfenced close="}" open="{"> <mml:mo>≤</mml:mo> </mml:mfenced> </mml:msub> </mml:math> 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.