Currying

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In mathematics and computer science, partial application, invented by Moses Schönfinkel and later re-invented by Haskell Curry,[1][not specific enough to verify] is the technique of transforming a function that takes multiple arguments (or an n-tuple of arguments) in such a way that it can be called as a chain of functions each with a single argument.

Uncurrying is the dual transformation to currying, and can be seen as a form of defunctionalization. It takes a function f(x) which returns another function g(y) as a result, and yields a new function f'(x, y) which takes a number of additional parameters and applies them to the function returned by f. The process can be iterated if necessary.

Contents

[edit] Motivation

Currying is similar to the process of calculating a function of multiple variables for some given values on paper. For example, given the function f(x,y) = y / x:

To evaluate f(2,y), first replace x with 2.
Since the result is a function of y, this function g(y) can be defined as g(y) = f(2,y) = y / 2.
Next, replace the y argument with 3, producing g(3) = f(2,3) = 3 / 2.

On paper, using classical notation, this is usually done all in one step. However, each argument can be replaced sequentially as well. Each replacement results in a simpler function taking one fewer argument. This produces a chain of functions as in lambda calculus, where each function takes only one argument, and multi-argument functions are usually represented in curried form.

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 (often called partial application) are useful; for example, many languages have a function or operator similar to plus_one. Currying makes it easy to define these functions, for example by currying the addition operator with 1 as its first argument.

This is similar in computer code: If we let f be a function f(x,y) = y / x, then the function g_x(y) = (y \mapsto f(x,y)) is a curried version of f. In particular, g_{(2)}(y) = (y \mapsto f(2,y)) is the curried equivalent of the example above.

[edit] Definition

Given a function f of type  f \colon (X \times Y) \to Z , then currying it makes a function  \text{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, and is most easily understood in terms of its right adjoint, apply.

The → operator is often considered right-associative, so the curried function type X \to (Y \to Z) is often written as X \to Y \to Z. Conversely, function application is considered to be left-associative, so that f \; \langle x, y \rangle is equivalent to \text{curry}(f) \; x \; y.

Intuitively, currying says "if you fix the first arguments of the function, 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 (i.e. div 1) is another function: the same as the function inv that returns the multiplicative inverse of its argument, defined by inv(y) = 1 / y.

Some programming languages almost always use curried functions to achieve multiple arguments; notable examples are ML and Haskell, where in both cases all functions have exactly one argument.

Curried functions may be used in any language that supports closures; however, uncurried functions are generally preferred for efficiency reasons, since the overhead of partial application and closure creation can then be avoided for most function calls.

[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 is the natural code between 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. 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; that is there is a natural transformation:

 \hom(A\times B, C) \cong \hom(A,\hom(B,C)) .

This is the key property of being a Cartesian closed category.

Under the Curry-Howard correspondence, the existence of currying and uncurrying is equivalent to the logical theorem (A \and B) \to C \Leftrightarrow A \to (B \to C), as tuples (product type) corresponds to conjunction in logic, and function type corresponds to implication.

Curry is a continuous function in the Scott topology.

[edit] Naming

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

[edit] See also

[edit] Notes

  1. ^ (Barendregt 2000, p. 8)
  2. ^ I. Heim and A. Kratzer (1998). Semantics in Generative Grammar. Blackwell.

[edit] References

[edit] External links

[edit] Language-Specific Implementations

Personal tools
Namespaces
Variants
Actions
Navigation
Interaction
Toolbox
Print/export
Languages