Type inference for higher-rank types and impredicativity

• FPH : First-class Polymorphism for Haskell, Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, submitted to ICFP 2008.
  • Paper PDF
  • Implementation and technical backup material

  Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting ``first-class'' polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm.

• Boxy types: type inference for higher rank and impredicativity, Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, ICFP 2006, pages 251-262.
  • Paper PDF
  • Accompanying technical report PDF
  • Related papers

  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 and impredicative types.