Boxy Types: Inference for Higher-Rank Types and Impredicativity

Dimitrios Vytiniotis, University of Pennsylvania
Stephanie C. Weirich, University of Pennsylvania
Simon Peyton Jones , Microsoft Research

Article comments

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

Abstract

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.