Boxy Types: Inference for Higher-Rank Types and Impredicativity
Postprint version. Copyright ACM, 2006. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SIGPLAN Notices, Volume 41, Issue 9, September 2006, pages 251-262.
Publisher URL: http://doi.acm.org/10.1145/1160074.1159838
Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established ideas: unification-based inference, and bidirectional propagation of type annotations. The result is a type system that conservatively extends Hindley-Milner, and yet supports both higher-rank types and impredicativity.
Dimitrios Vytiniotis, Stephanie C. Weirich, and Simon Peyton Jones . "Boxy Types: Inference for Higher-Rank Types and Impredicativity" Departmental Papers (CIS) (2006).
Available at: http://works.bepress.com/stephanie_weirich/7