Parametricity

Parametricity is a property that given a parametric polymorphic function, its behaviour should be the same no matter how its type parameters are specialized.
This property is enjoyed by some (in fact, most) of the functional programming languages, but there are exceptions, such as Idris2 that supports pattern matching on types.

To some extent, parametricity is similar to a "η-rule" for polymorphic types. For instance, the type \forall t. t \to t has a unique instance -- the polymorphic identity function, but this is true only if the type theory satisfies parametricity (and in a type theory that contradicts parametricity, there might be multiple distinct instances of this type).

Parametricity is necessary for proving the isomorphism between lambda-encoded inductive types and the conventional inductive types.

See also

• Parametric polymorphism
• System F
• John Reynolds
• Jean-Yves Girard

References

• The most celebrated application of parametricity is in automatically generating algebraic laws between purely functional programs:

@inproceedings{wadler_theorems_1989,
	address = {New York, New York, USA},
	title = {Theorems for free!},
	volume = {112},
	isbn = {0-89791-328-0},
	doi = {10.1145/99370.99404},
	booktitle = {Proceedings of the fourth {International} {Ponference} on {Functional} {Programming} languages and computer architecture - {FPCA} '89},
	publisher = {ACM Press},
	author = {Wadler, Philip},
	year = {1989},
	pages = {347--359}
}

• The first parametric model of System F was introduced in 1983 by John C. Reynolds. Even though the idea has been extremely influential, this first attempt was subject to [Russell's Paradox](/concepts/Russell's Paradox):

@inproceedings{reynolds_1983,
	address = {Amsterdam},
	title = {Types, {Abstraction}, and {Parametric} {Polymorphism}},
	booktitle = {Information {Processing} 83: {Proceedings} of the {IFIP} 9th {World} {Computer} {Congress}, {Paris}, {France}, {September} 19-23, 1983},
	publisher = {Elsevier Science Publishers B. V. (North-Holland)},
	author = {Reynolds, John C.},
	editor = {Mason, R. E. A},
	year = {1983},
	pages = {513--523}
}