Parametric polymorphism

In a prenex polymorphic system, type variables may not be instantiated with polymorphic types.[4] This is very similar to what is called "ML-style" or "Let-polymorphism" (technically ML's Let-polymorphism has a few other syntactic restrictions). This restriction makes the distinction between polymorphic and non-polymorphic types very important; thus in predicative systems polymorphic types are sometimes referred to as type schemas to distinguish them from ordinary (monomorphic) types, which are sometimes called monotypes. A consequence is that all types can be written in a form that places all quantifiers at the outermost (prenex) position. For example, consider the append function described above, which has type

forall a. [a] × [a] -> [a]

In order to apply this function to a pair of lists, a type must be substituted for the variable a in the type of the function such that the type of the arguments matches up with the resulting function type. In an impredicative system, the type being substituted may be any type whatsoever, including a type that is itself polymorphic; thus append can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as append itself. Polymorphism in the language ML is predicative. This is because predicativity, together with other restrictions, makes the type system simple enough that full type inference is always possible.

As a practical example, OCaml (a descendant or dialect of ML) performs type inference and supports impredicative polymorphism, but in some cases when impredicative polymorphism is used, the system's type inference is incomplete unless some explicit type annotations are provided by the programmer.

For some fixed value k, rank-k polymorphism is a system in which a quantifier may not appear to the left of k or more arrows (when the type is drawn as a tree).[1]

Type inference for rank-2 polymorphism is decidable, but reconstruction for rank-3 and above is not.[5]

Rank-n polymorphism is polymorphism in which quantifiers may appear to the left of arbitrarily many arrows.

In a predicative parametric polymorphic system, a type ${\displaystyle \tau }$ containing a type variable ${\displaystyle \alpha }$ may not be used in such a way that ${\displaystyle \alpha }$ is instantiated to a polymorphic type. Predicative type theories include Martin-Löf Type Theory and NuPRL.

Impredicative polymorphism (also called first-class polymorphism) is the most powerful form of parametric polymorphism.[6] A definition is said to be impredicative if it is self-referential; in type theory this allows the instantiation of a variable in a type ${\displaystyle \tau }$ with any type, including polymorphic types, such as ${\displaystyle \tau }$ itself. An example of this is the System F with the type variable X in the type ${\displaystyle T=\forall X.X\to X}$, where X could even refer to T itself.

In type theory, the most frequently studied impredicative typed λ-calculi are based on those of the lambda cube, especially System F.[1]