Currying

From Wikipedia, the free encyclopedia
  (Redirected from Curry function)
Jump to: navigation, search
For leather finishing, see Currier.

In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments (or a tuple of arguments) into evaluating a sequence of functions, each with a single argument (partial application). It was introduced by Moses Schönfinkel[1][2][3] and later developed by Haskell Curry.[4][5]

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 function f. The process can be iterated if necessary.

Motivation[edit]

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,3), first replace x with 2
Since the result is a function of y, this new 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 function taking exactly one argument. This produces a chain of functions as in lambda calculus, and multi-argument functions are usually represented in curried form.

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.

If we let f be a function

f(x,y) = \frac{y}{x}

then the function h where

h(x) = y \mapsto f(x,y)

is a curried version of f. Here, \scriptstyle y \mapsto z is a function that maps an argument y to result z. In particular,

g(y) = h(2) = y \mapsto f(2,y)

is the curried equivalent of the example above. Note, however, that currying, while similar, is not the same operation as partial function application.

Definition[edit]

Given a function \scriptstyle f of type \scriptstyle f \colon (X \times Y) \to Z , currying it makes a function \scriptstyle \text{curry}(f) \colon X \to (Y \to Z) . That is, \scriptstyle \text{curry}(f) takes an argument of type \scriptstyle X and returns a function of type \scriptstyle 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 \scriptstyle X \to (Y \to Z) is often written as \scriptstyle X \to Y \to Z. Conversely, function application is considered to be left-associative, so that \scriptstyle f \; \langle x, y \rangle is equivalent to \scriptstyle\text{curry}(f) \; x \; y.

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.

Mathematical view[edit]

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.

In a set-theoretic paradigm, currying is the natural correspondence between the set \scriptstyle A^{B\times C} of functions from \scriptstyle B\times C to A, and the set \scriptstyle\left(A^C\right)^B of functions from \scriptstyle B to the set of functions from \scriptstyle C to \scriptstyle 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 \scriptstyle f \colon (X \times Y) \to Z and the morphisms to an exponential object \scriptstyle 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, C^B) .

This is the key property of being a Cartesian closed category, and more generally, a closed monoidal category.[6] The latter, though more rarely discussed, is interesting, as it is the suitable setting for quantum computation,[7] whereas the former is sufficient for classical logic. The difference is that the Cartesian product can be interpreted simply as a pair of items (or a list), whereas the tensor product, used to define a monoidal category, is suitable for describing entangled quantum states.[8]

Under the Curry–Howard correspondence, the existence of currying and uncurrying is equivalent to the logical theorem \scriptstyle (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.[9]

Naming[edit]

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.[10]

Contrast with partial function application[edit]

Main article: Partial application

Currying and partial function application are often conflated.[11] One of the significant differences between the two is that a call to a partially applied function returns the result right away, not another function down the currying chain; this distinction can be illustrated clearly for functions whose arity is greater than two.[12]

Given a function of type \scriptstyle f \colon (X \times Y \times Z) \to N , currying produces \scriptstyle \text{curry}(f) \colon X \to (Y \to (Z \to N)) . That is, while an evaluation of the first function might be represented as \scriptstyle f(1, 2, 3), evaluation of the curried function would be represented as \scriptstyle f_\text{curried}(1)(2)(3), applying each argument in turn to a single-argument function returned by the previous invocation. Note that after calling \scriptstyle f_\text{curried}(1), we are left with a function that takes a single argument and returns another function, not a function that takes two arguments.

In contrast, partial function application refers to the process of fixing a number of arguments to a function, producing another function of smaller arity. Given the definition of \scriptstyle f above, we might fix (or 'bind') the first argument, producing a function of type \scriptstyle\text{partial}(f) \colon (Y \times Z) \to N. Evaluation of this function might be represented as \scriptstyle f_\text{partial}(2, 3). Note that the result of partial function application in this case is a function that takes two arguments.

Intuitively, partial function application 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 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.

The practical motivation for partial application is that very often the functions obtained by supplying some but not all of the arguments to a function are useful; for example, many languages have a function or operator similar to plus_one. Partial application makes it easy to define these functions, for example by creating a function that represents the addition operator with 1 bound as its first argument.

See also[edit]

Notes[edit]

  1. ^ Strachey, Christopher (2000). "Fundamental Concepts in Programming Languages". Higher-Order and Symbolic Computation 13: 11–49. doi:10.1023/A:1010000313106. There is a device originated by Schönfinkel, for reducing operators with several operands to the successive application of single operand operators.  (Reprinted lecture notes from 1967.)
  2. ^ Reynolds, John C. (1998). "Definitional Interpreters for Higher-Order Programming Languages". Higher-Order and Symbolic Computation 11 (4): 374. doi:10.1023/A:1010027404223. In the last line we have used a trick called Currying (after the logician H. Curry) to solve the problem of introducing a binary operation into a language where all functions must accept a single argument. (The referee comments that although “Currying” is tastier, “Schönfinkeling” might be more accurate.) 
  3. ^ Kenneth Slonneger and Barry L. Kurtz. Formal Syntax and Semantics of Programming Languages. p. 144.
  4. ^ Henk Barendregt, Erik Barendsen, "Introduction to Lambda Calculus", March 2000, page 8.
  5. ^ Curry, Haskell; Feys, Robert (1958). Combinatory logic I (2 ed.). Amsterdam, Netherlands: North-Holland Publishing Company. 
  6. ^ Currying in nLab
  7. ^ Samson Abramsky and Bob Coecke, "A Categorical Semantics for Quantum Protocols", "[1].
  8. ^ John c. Baez and Mike Stay, "Physics, Topology, Logic and Computation: A Rosetta Stone", (2009) ArXiv 0903.0340 in New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174.
  9. ^ Barendregt, H.P. (1984). The Lambda Calculus. North-Holland. ISBN 0-444-87508-5.  (See theorems 1.2.13, 1.2.14)
  10. ^ I. Heim and A. Kratzer (1998). Semantics in Generative Grammar. Blackwell.
  11. ^ Partial Function Application is not Currying
  12. ^ Functional Programming in 5 Minutes

References[edit]

  • Schönfinkel, Moses (1924). "Über die Bausteine der mathematischen Logik". Math. Ann. 92 (3–4): 305–316. doi:10.1007/BF01448013. 
  • Heim, Irene; Kratzer, Angelika (1998). "Semantics in a Generative Grammar". Malden: Blackwall Publishers 

External links[edit]