Parametricity is a result in the theory of programming languages in computer science

Computer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

. The principle of parametricity dictates that functions

Function (mathematics)

In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...

 with similar types

Type theory

In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...

 have similar properties.

Theory of parametricity

The parametricity theorem was originally stated by John C. Reynolds

John C. Reynolds

John C. Reynolds is an American computer scientist.John Reynolds studied at Purdue University and then earned a PhD in theoretical physics from Harvard University in 1961. He was Professor of Information science at Syracuse University from 1970 to 1986. Since then he has been Professor of Computer...

, who called it the abstraction theorem.

In his paper "Theorems for free!", Philip Wadler

Philip Wadler

Philip Wadler is a computer scientist known for his contributions to programming language design and type theory. In particular, he has contributed to the theory behind functional programming and the use of monads in functional programming, the design of the purely functional language Haskell, and...

 described an application of parametricity to derive theorems about parametrically polymorphic

Parametric polymorphism

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...

 functions based on their types.

Parametricity and programming language implementation

Parametricity is the basis for many program transformation

Program transformation

A program transformation is any operation that takes a computer program and generates another program. In many cases the transformed program is required to be semantically equivalent to the original, relative to a particular formal semantics and in fewer cases the transformations result in programs...

s implemented in compilers for the Haskell programming language. These transformations were traditionally thought to be correct in Haskell because of Haskell's non-strict semantics. Despite being a lazy

Lazy evaluation

In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...

 programming language, Haskell does support certain primitive operations — such as the operator seq — that enable so-called "selective strictness", allowing the programmer to force the evaluation of certain expressions. In their paper "Free theorems in the presence of seq", 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.