Boxy type inference for higher-rank types and impredicativity
- Dimitrios Vytiniotis ,
- Stephanie Weirich ,
- Simon Peyton Jones
ICFP 2006 |
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 ﬁrst time, how to combine the virtues of two well-established ideas: uniﬁcation-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.
- Accompanying technical report PDF
- Related papers