FPH: First-class polymorphism for Haskell
A declarative, constraint-free specification of type inference for first-class
polymorphism.
Languages supporting polymorphism typically have ad-hoc restrictions
on where polymoprhic 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 polymoprhism 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 transformation; and we give a complete and decidable
type inference algorithm.
This is joint work with Stephanie Weirich and Simon Peyton Jones.
Available material: