Currying

From Wikipedia, the free encyclopedia

In computer science, currying, invented by Moses Schönfinkel and Gottlob Frege, is the technique of transforming a function that takes multiple arguments (or more accurately an n-tuple as argument) into a higher-order function that takes a single argument.

Contents

[edit] Nomenclature

The name "currying", coined by Christopher Strachey in 1967, is a reference to logician Haskell Curry. An alternative name, Schönfinkelisation, has been proposed. [1]

[edit] Definition

Given a function f of type  f \colon (X \times Y) \to Z , then currying it makes a function  \mbox{curry}(f) \colon X \to (Y \to Z) . That is, curry(f) takes an argument of type X and returns a function of type  Y \to Z . Uncurrying is the reverse transformation.

Intuitively, currying says "if you fix some arguments, you get a function of the remaining arguments". For example, if function div stands for the curried form of the division operation x / y, then div with the parameter x fixed at 1 is another function: the same as the function inv that returns the multiplicative inverse of its argument, defined by inv(y) = 1 / y.

The practical motivation for currying is that very often the functions obtained by supplying some but not all of the arguments to a curried function are useful; for example, many languages have a function or operator similar to plus_one. Currying makes it easy to define these functions.

Some programming languages have built-in syntactic support for currying, where certain multi-argument functions are expanded to their curried form; notable examples are ML and Haskell. Any language that supports closures can be used to write curried functions.

[edit] Mathematical view

In theoretical computer science, currying provides a way to study functions with multiple arguments in very simple theoretical models such as the lambda calculus in which functions only take a single argument.

When viewed in a set-theoretic light, currying becomes the theorem that the set A^{B\times C} of functions from B\times C to A, and the set (AB)C of functions from C to the set of functions from B to A, are isomorphic.

In category theory, currying can be found in the universal property of an exponential object, which gives rise to the following adjunction in cartesian closed categories: There is a natural isomorphism between the morphisms from a binary product  f \colon (X \times Y) \to Z and the morphisms to an exponential object  g \colon X \to Z^Y . In other words, currying is the statement that product and Hom are adjoint functors; this is the key property of being a Cartesian closed category.

[edit] See also

[edit] References

  1. ^ I. Heim and A. Kratzer (1998). Semantics in Generative Grammar. Blackwell.

[edit] External links

Look up currying in Wiktionary, the free dictionary.