Parametric polymorphism: Difference between revisions

Revision as of 16:29, 17 June 2022

Revision as of 22:43, 30 September 2022

Line 14:

The most general form of polymorphism is "higher-rank [[impredicative]] polymorphism". Two popular restrictions of this form are restricted rank polymorphism (for example, rank-1 or ''prenex'' polymorphism) and predicative polymorphism. Together, these restrictions give "predicative prenex polymorphism", which is essentially the form of polymorphism found in ML and early versions of Haskell.

== HigherPredicativity, impredicativity, and higher-rankedrank polymorphism ==

=== Rank-1 (prenexpredicative) polymorphism ===

{{refimprove section|date=February 2019}}

In a ''[[Impredicativity|predicative]]'' type system (also known as a ''[[prenex]] polymorphic'' system), type variables may not be instantiated with polymorphic types.<ref name="TAPL">{{cite book|author1=Benjamin C. Pierce|author2=Benjamin C. (Professor Pierce, University of Pennsylvania)|title=Types and Programming Languages|url=https://books.google.com/books?id=ti6zoAC9Ph8C|year=2002|publisher=MIT Press|isbn=978-0-262-16209-8}}</ref>{{rp|pages=359–360}} Predicative type theories include [[Intuitionistic type theory|Martin-Löf type theory]] and [[NuPRL]]. 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 <code>append</code> function described above, which has type

Line 27:

As a practical example, [[OCaml]] (a descendant or dialect of [[ML (programming language)|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.

=== RankHigher-''k''rank polymorphism ===

Some type systems support an impredicative function type constructor even though other type constructors remain predicative. For example, the type <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math> is permitted in a system that supports higher-rank polymorphism, even though <math>[\forall \alpha. \alpha \rightarrow \alpha]</math> may not be.<ref>{{cite web |author1=Kwang Yul Seo |title=Kwang's Haskell Blog - Higher rank polymorphism |url=https://kseo.github.io/posts/2016-12-27-higher-rank-polymorphism.html |website=kseo.github.io |access-date=30 September 2022}}</ref>

{{expand section|date=November 2013}}

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).{{sfn|Pierce|2002}}

A type is said to be of rank ''k'' (for some fixed integer ''k'') if no path from its root to a <math>\forall</math> quantifier passes to the left of ''k'' or more arrows, when the type is drawn as a tree.<ref name="TAPL" />{{rp|359}} A type system is said to support rank-''k'' polymorphism if it admits types with rank less than or equal to ''k''. For example, a type system that supports rank-2 polymorphism would allow <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math> but not <math>((\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T) \rightarrow T</math>. A type system that admits types of arbitrary rank is said to be "rank-''n'' polymorphic".

[[Type inference]] for rank-2 polymorphism is decidable, but reconstruction for rank-3 and above is not.{{sfn|Pierce|2002|p=359}}

[[Type inference]] for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.<ref>{{cite journal |last1=Kfoury |first1=A. J. |last2=Wells |first2=J. B. |title=Principality and decidable type inference for finite-rank intersection types |journal=Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages |date=1 January 1999 |pages=161–174 |doi=10.1145/292540.292556 |url=https://dl.acm.org/doi/abs/10.1145/292540.292556 |publisher=Association for Computing Machinery}}</ref><ref name="TAPL" />{{rp|359}}

=== Rank-''n'' ("higher-rank") polymorphism ===

{{expand section|date=November 2013}}

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

== Predicativity and impredicativity ==

=== Predicative polymorphism ===

In a predicative parametric polymorphic system, a type <math>\tau</math> containing a type variable <math>\alpha</math> may not be used in such a way that <math>\alpha</math> is instantiated to a polymorphic type. Predicative type theories include [[Intuitionistic type theory|Martin-Löf type theory]] and [[NuPRL]].

=== Impredicative polymorphism ===

''Impredicative polymorphism'' (also called ''first-class polymorphism'') is the most powerful form of parametric polymorphism.<ref name="TAPL" />{{sfnrp|Pierce|2002|p=340}} AIn [[formal logic]], a definition is said to be [[impredicativity|impredicative]] if it is self-referential; in type theory, thisit allowsrefers to the instantiationability offor a variabletype to be in the ___domain of a quantifier it contains. This allows the instantiation of any type <math>\tau</math>variable with any type, including polymorphic types, such as <math>\tau</math> itself. An example of thisa issystem thesupporting full impredicativity is [[System F]], withwhich theallows type variable ''X'' in the typeinstantiating <math>T = \forall X\alpha. X\alpha \to X\alpha</math>, whereat ''X''any couldtype, even refer to ''T''including itself.

In [[type theory]], the most frequently studied impredicative [[typed lambda calculus|typed λ-calculi]] are based on those of the [[lambda cube]], especially [[System F]].{{sfn|Pierce|2002}}

== Bounded parametric polymorphism ==