Predicative vs. Impredicative Polymorphism and Type Reconstruction
The polymorphism of System F is often called impredicative. A definition is called impredicative if it involves a quantifier whose domain includes the very thing being defined. For example in System F, the type variable X in the type T = ∀X. X → X ranges over all types, including T itself (so that, for example, we can instantiate a term of type T at type T, yielding a function from T to T).[6]
The polymorphism found in ML is called predicative, because the range of type variables is restricted to monotypes (i.e. quantifier-free types), which do not contain quantifiers.
When talking about type reconstruction the previous definitions are important. There is a growing “[...] need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types—that is, functions that take polymorphic functions as their arguments.”[1]
Complete type inference is known to be undecidable for higher-rank (impredicative) type systems. This post serves as a reference for type reconstruction in the presence of polymorphism in higher-rank type systems.
[1] Practical type inference for arbitrary-rank types
[3] Type Polymorphism – DocForge
[4] Type Polymorphism -Wikipedia
[5] System F – Polymorphic/Second-Order Lambda Calculus
[6] Types and Programming Languages [p.360]
