Sciweavers

JFP
2007

Practical type inference for arbitrary-rank types

13 years 10 months ago
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...
Simon L. Peyton Jones, Dimitrios Vytiniotis, Steph
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JFP
Authors Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields
Comments (0)