Practical type inference for arbitrary-rank types

Haskell’s popularity has driven the need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types—that is, functions that take polymorphic functions as their arguments. Complete type inference is known to be undecidable for higher-rank (impredicative) type systems, but in practice programmers are more than willing to add type annotations to guide the type inference engine, and to document their code. However, the choice of just what annotations are required, and what changes are required in the type system and its inference algorithm, has been an ongoing topic of research. We take as our starting point a λ-calculus proposed by Odersky and L¨aufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations on λ-bound arguments and arbitrary sub-terms. Though elegant, and more convenient than s...

• Type: Journal
• Year: 2007
• Where: JFP
• Authors: Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields
• Keywords: Annotation, JFP 2007, Type Inference, Type System