Parametricity

Parametricity

In the theory of programming languages in computer science, parametricity is a theoretical result that states that functions that have types that are related to each other share certain properties in common.

Theory of parametricity

The "parametricity theorem" was originally stated by John C. Reynolds, who called it the "abstraction theorem". [cite conference
first = J.C.
last = Reynolds
title = Types, abstraction, and parametric polymorphism
booktitle = Information Processing
pages = 513-523
year = 1983
location = North Holland, Amsterdam ]

In his paper "Theorems for free!" [cite conference
first = Philip
last = Wadler
url = http://citeseer.ist.psu.edu/wadler89theorems.html
title = Theorems for free!
booktitle = 4th Int'l Conf. on Functional Programming and Computer Architecture
date = September 1989
location = London ] , Philip Wadler described an application of parametricity to derive theorems about parametrically polymorphic functions based on their types.

Parametricity and programming language implementation

Parametricity is the basis for many program transformations 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 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" [cite conference
first = Patricia
last = Johann
coauthors = Janis Voigtlaender
title = Free theorems in the presence of "seq"
url = http://citeseer.ist.psu.edu/johann04free.html
booktitle = Proc., Principles of Programming Languages
date = January 2004
pages = 99-110] , 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.

See also

* Parametric polymorphism
* Non-strict programming language

References


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • parametricity — noun The quality or state of being parametric …   Wiktionary

  • Generic programming — is a style of computer programming in which algorithms are written in terms of to be specified later types that are then instantiated when needed for specific types provided as parameters and was pioneered by Ada which appeared in 1983. This… …   Wikipedia

  • F-algebra — In mathematics, specifically in category theory, an F algebra for an endofunctor :F : mathbf{C}longrightarrow mathbf{C} is an object A of mathbf{C} together with a mathbf{C} morphism :alpha : FA longrightarrow A. In this sense F algebras are dual …   Wikipedia

  • John C. Reynolds — is an American computer scientist (born June 1, 1935).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… …   Wikipedia

  • Initial algebra — In mathematics, an initial algebra is an initial object in the category of F algebras for a given endofunctor F . The initiality provides a general framework for induction and recursion. For instance, consider the endofunctor 1+( ) on the… …   Wikipedia

  • parametric — adjective of, relating to, or defined using parameters See Also: parametrical, parametricity …   Wiktionary

  • Polymorphism (computer science) — This article is about the programming language theory concepts with direct application to functional programming languages. For a gentler introduction of these notions as commonly implemented in object oriented programming, see Polymorphism in… …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”