Boxy types: inference for higher-rank types and impredicativity

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. Categories and Subject Descriptors D.3.3 [PROGRAMMING S]: Language Constructs and Features--abstract data types, polymorphism General Terms Languages, Theory Keywords impredicativity, higher-rank types, type inference

• Type: Conference
• Year: 2006
• Where: ICFP
• Authors: Dimitrios Vytiniotis, Stephanie Weirich, Simon L. Peyton Jones
• Keywords: ICFP 2006, Programmer-supplied Type Annotations, Programming Languages, Rich Type Systems, Type Inference Engine