## Practical type inference for arbitrary-rank types

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields.
To appear in the Journal of Functional Programming.
Very minor post-JFP revision: Nov 2006
Final minor revision: Feb 2006

Second major revision: July 2005

Major revision: April 2004

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 lambda-calculus proposed by Odersky and
Laufer. Their system supports arbitrary-rank polymorphism through
the exploitation of type annotations on lambda-bound
arguments and arbitrary sub-terms. Though elegant, and more
convenient than some other proposals, Odersky and Laufer's system
requires many annotations. We show how to use local type inference
(invented by Pierce and Turner) to greatly reduce the annotation burden,
to the point where higher-rank types become eminently usable.

Higher-rank types have a very modest impact on type inference. We
substantiate this claim in a very concrete way, by presenting a
complete type-inference engine, written in Haskell, for a traditional
Damas-Milner type system, and then showing how to extend it for
higher-rank types. We write the type-inference engine using a monadic
framework: it turns out to be a particularly compelling example of
monads in action.

The paper is long, but is strongly tutorial in style.

Simon Peyton Jones, simonpj@microsoft.com