{{Short description|Type theory concept}} In programming language theory, '''parametricity''' is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.
== Idea ==
Consider this example, based on a set ''X'' and the type ''T''(''X'') = [''X'' → ''X''] of functions from ''X'' to itself. The higher-order function ''twice''<sub>''X''</sub> : ''T''(''X'') → ''T''(''X'') given by ''twice''<sub>''X''</sub>(''f'') = ''f'' ∘ ''f'', is intuitively independent of the set ''X''. The family of all such functions ''twice''<sub>''X''</sub>, parametrized by sets ''X'', is called a "parametrically polymorphic function". We simply write '''twice''' for the entire family of these functions and write its type as <math>\forall</math>''X''. ''T''(''X'') → ''T''(''X''). The individual functions ''twice''<sub>''X''</sub> are called the ''components'' or ''instances'' of the polymorphic function. Notice that all the component functions ''twice''<sub>''X''</sub> act "the same way" because they are given by the same rule. Other families of functions obtained by picking one arbitrary function from each ''T''(''X'') → ''T''(''X'') would not have such uniformity. They are called "''ad hoc'' polymorphic functions". ''Parametricity'' is the abstract property enjoyed by the uniformly acting families such as '''twice''', which distinguishes them from ''ad hoc'' families. With an adequate formalization of parametricity, it is possible to prove that the parametrically polymorphic functions of type <math>\forall</math>''X''. ''T''(''X'') → ''T''(''X'') are one-to-one with natural numbers. The function corresponding to the natural number ''n'' is given by the rule ''f'' <math>\mapsto</math> ''f''<sup>''n''</sup>, i.e., the polymorphic Church numeral for ''n''. In contrast, the collection of all ''ad hoc'' families would be too large to be a set.
== History == The ''parametricity theorem'' was originally stated by John C. Reynolds, who called it the ''abstraction theorem''.<ref>{{cite conference |last1=Reynolds |first1=J.C. |year=1983 |title=Types, abstraction, and parametric polymorphism |book-title=Information Processing |pages=513–523 |url=https://people.mpi-sws.org/~dreyer/tor/papers/reynolds.pdf |location=North Holland, Amsterdam}}</ref> In his paper "Theorems for free!",<ref>{{cite conference |last1=Wadler |first1=Philip |author1-link=Philip Wadler |date=September 1989 |url=http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875 |title=Theorems for free! |book-title=4th International Conference on Functional Programming and Computer Architecture |location=London}}</ref> Philip Wadler described an application of parametricity to derive theorems about parametrically polymorphic functions based on their types.
{{Expand section|date=June 2008}}
== Programming language implementation ==
Parametricity is the basis for many program transformations implemented in compilers for the programming language Haskell. These transformations were traditionally thought to be correct in Haskell because of Haskell's non-strict semantics. Despite being a lazy evaluation programming language, Haskell does support certain primitive operations, such as the operator <code>seq</code>—that enable so-called ''selective strictness'', allowing evaluation to be forced for certain expressions. In their paper "Free theorems in the presence of ''seq''",<ref>{{cite conference |last1=Johann |first1=Patricia |last2=Voigtlaender |first2=Janis |date=January 2004 |title=Free theorems in the presence of ''seq'' |url=https://doi.org/10.1145/964001.964010 |book-title=Proceedings, Principles of Programming Languages |pages=99–110 |doi=10.1145/964001.964010 |url-access=subscription }}</ref> Patricia Johann and Janis Voigtlaender showed that because of the presence of these operations, the general parametricity theorem does not hold for Haskell programs; thus, these transformations are unsound in general.
== Dependent types == {{Expand section|date=June 2013}}
== See also == * Parametric polymorphism * Non-strict programming language
== References == {{Reflist}}
== External links == * [http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html Wadler: Parametricity]
Category:Programming language topics Category:Type theory Category:Polymorphism (computer science)