In mathematics and computer science, currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument.
In the prototypical example, one begins with a function $f:(X\backslash times\; Y)\backslash to\; Z$ that takes two arguments, one from $X$ and one from $Y,$ and produces objects in $Z.$ The curried form of this function treats the first argument as a parameter, so as to create a family of functions $f\_x\; :Y\backslash to\; Z.$ The family is arranged so that for each object $x$ in $X,$ there is exactly one function $f\_x.$
In this example, $\backslash mbox\{curry\}$ itself becomes a function, that takes $f$ as an argument, and returns a function that maps each $x$ to $f\_x.$ The proper notation for expressing this is verbose. The function $f$ belongs to the set of functions $(X\backslash times\; Y)\backslash to\; Z.$ Meanwhile, $f\_x$ belongs to the set of functions $Y\backslash to\; Z.$ Thus, something that maps $x$ to $f\_x$ will be of the type $X\backslash to\; Y\backslash to.$ With this notation, $\backslash mbox\{curry\}$ is a function that takes objects from the first set, and returns objects in the second set, and so one writes $\backslash mbox\{curry\}:(X\backslash times\backslash to\; (X\backslash to\; Y\backslash to).$ This is a somewhat informal example; more precise definitions of what is meant by "object" and "function" are given below. These definitions vary from context to context, and take different forms, depending on the theory that one is working in.
Currying is related to, but not the same as, partial application. The example above can be used to illustrate partial application; it is quite similar. Partial application is the function $\backslash mbox\{apply\}$ that takes the pair $f$ and $x$ together as arguments, and returns $f\_x.$ Using the same notation as above, partial application has the signature $\backslash mbox\{apply\}:((X\backslash times\; \backslash times\; X)\; \backslash to\; Y\backslash to.$ Written this way, application can be seen to be adjoint to currying.
The currying of a function with more than two arguments can be defined by induction.
Currying is useful in both practical and theoretical settings. In functional programming languages, and many others, it provides a way of automatically managing how arguments are passed to functions and exceptions. In theoretical computer science, it provides a way to study functions with multiple arguments in simpler theoretical models which provide only one argument. The most general setting for the strict notion of currying and uncurrying is in the closed monoidal categories, which underpins a vast generalization of the Curry–Howard correspondence of proofs and programs to a correspondence with many other structures, including quantum mechanics, cobordisms and string theory.
The concept of currying was introduced by Gottlob Frege,
developed by Moses Schönfinkel,Originally published as and further developed by Haskell Curry.Uncurrying is the dual transformation to currying, and can be seen as a form of defunctionalization. It takes a function $f$ whose return value is another function $g$, and yields a new function $f\text{'}$ that takes as parameters the arguments for both $f$ and $g$, and returns, as a result, the application of $f$ and subsequently, $g$, to those arguments. The process can be iterated.
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. This property is inherited from lambda calculus, where multiargument functions are usually represented in curried form.
Currying is related to, but not the same as partial application. In practice, the programming technique of closures can be used to perform partial application and a kind of currying, by hiding arguments in an environment that travels with the curried function.
The originator of the word "currying" is not clear. David Turner says the word was coined by Christopher Strachey in his 1967 lecture notes Fundamental Concepts in Programming Languages, but although the concept is mentioned and Curry is mentioned in the context of higherorder functions, the word "currying" does not appear in the notes and Curry is not associated with the concept. John C. Reynolds defined "currying" in a 1972 paper, but did not claim to have coined the term.
Given a function
currying constructs a new function
That is, $g$ takes an argument of type $X$ and returns a function of type $Y\backslash to\; Z$. It is defined by
for $x$ of type $X$ and $y$ of type $Y$. We then also write
Uncurrying is the reverse transformation, and is most easily understood in terms of its right adjoint, the apply
Indeed, it is this natural bijection that justifies the exponential notation for the set of functions. As is the case in all instances of currying, the formula above describes an Adjoint functors: for every fixed set $C$, the functor $B\backslash mapsto\; B\backslash times\; C$ is left adjoint to the functor $A\; \backslash mapsto\; A^C$.
In the category of sets, the object $Y^X$ is called the exponential object.
while uncurrying is the inverse map. If the set $Y^X$ of continuous functions from $X$ to $Y$ is given the compactopen topology, and if the space $Y$ is locally compact Hausdorff, then
is a homeomorphism. This is also the case when $X$, $Y$ and $Y^X$ are compactly generated,
although there are more cases.One useful corollary is that a function is continuous if and only if its curried form is continuous. Another important result is that the apply, usually called "evaluation" in this context, is continuous (note that eval is a strictly different concept in computer science.) That is,
$\backslash begin\{align\}\; \&\&\backslash text\{eval\}:Y^X\; \backslash times\; X\; \backslash to\; Y\; \backslash \backslash $
&& (f,x) \mapsto f(x) \end{align}
is continuous when $Y^X$ is compactopen and $Y$ locally compact Hausdorff.
These two results are central for establishing the continuity of homotopy, i.e. when $X$ is the unit interval $I$, so that $Z^\{I\backslash times\; Y\}\; \backslash cong\; (Z^Y)^I$ can be thought of as either a homotopy of two functions from $Y$ to $Z$, or, equivalently, a single (continuous) path in $Z^Y$.
The duality between the mapping cone and the mapping fiber (cofibration and fibration) can be understood as a form of currying, which in turn leads to the duality of the long exact and coexact .
In homological algebra, the relationship between currying and uncurrying is known as tensorhom adjunction. Here, an interesting twist arises: the Hom functor and the tensor product functor might not lift to an exact sequence; this leads to the definition of the Ext functor and the Tor functor.
The notion of continuity makes its appearance in homotopy type theory, where, roughly speaking, two computer programs can be considered to be homotopic, i.e. compute the same results, if they can be "continuously" code refactoring from one to the other.
where $\backslash lambda$ is the abstractor of lambda calculus. Since curry takes, as input, functions with the type $(X\backslash times\; Y)\backslash to\; Z$, one concludes that the type of curry itself is
The → operator is often considered rightassociative, so the curried function type $X\; \backslash to\; (Y\; \backslash to\; Z)$ is often written as $X\; \backslash to\; Y\; \backslash to\; Z$. Conversely, function application is considered to be leftassociative, so that $f(x,\; y)$ is equivalent to
That is, the parenthesis are not required to disambiguate the order of the application.
Curried functions may be used in any programming 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.
The typetheoretical approach is expressed in programming languages such as ML and the languages derived from and inspired by it: CaML, Haskell and F#.
The typetheoretical approach provides a natural complement to the language of category theory, as discussed below. This is because categories, and specifically, monoidal categories, have an internal language, with simplytyped lambda calculus being the most prominent example of such a language. It is important in this context, because it can be built from a single type constructor, the arrow type. Currying then endows the language with a natural product type. The correspondence between objects in categories and types then allows programming languages to be reinterpreted as logics (via Curry–Howard correspondence), and as other types of mathematical systems, as explored further, below.
The exponential object $Q^P$ in the category of is normally written as material implication $P\backslash to\; Q$. Distributive Heyting algebras are , and the exponential object has the explicit form $\backslash neg\; P\; \backslash lor\; Q$, thus making it clear that the exponential object really is material implication.
This generalizes to a broader result in closed monoidal categories: Currying is the statement that the tensor product and the internal Hom are adjoint functors; that is, for every object $B$ there is a natural isomorphism:
Here, Hom denotes the (external) Homfunctor of all morphisms in the category, while $B\backslash Rightarrow\; C$ denotes the internal hom functor in the closed monoidal category. For the category of sets, the two are the same. When the product is the cartesian product, then the internal hom $B\backslash Rightarrow\; C$ becomes the exponential object $C^B$.
Currying can break down in one of two ways. One is if a category is not closed category, and thus lacks an internal hom functor (possibly because there is more than one choice for such a functor). Another way is if it is not monoidal, and thus lacks a product (that is, lacks a way of writing down pairs of objects). Categories that do have both products and internal homs are exactly the closed monoidal categories.
The setting of cartesian closed categories is sufficient for the discussion of classical logic; the more general setting of closed monoidal categories is suitable for quantum computation.
The difference between these two is that the product for cartesian categories (such as the category of sets, complete partial orders or ) is just the Cartesian product; it is interpreted as an ordered pair of items (or a list). Simply typed lambda calculus is the internal language of cartesian closed categories; and it is for this reason that pairs and lists are the primary type system in the type theory of LISP, Scheme and many functional programming languages.
By contrast, the product for monoidal categories (such as Hilbert space and the of functional analysis) is the tensor product. The internal language of such categories is linear logic, a form of quantum logic; the corresponding type system is the linear type system. Such categories are suitable for describing entangled quantum states, and, more generally, allow a vast generalization of the Curry–Howard correspondence to quantum mechanics, to in algebraic topology, and to string theory.
The linear type system, and linear logic are useful for describing synchronization primitives, such as mutual exclusion locks, and the operation of vending machines.
Given a function of type $f\; \backslash colon\; (X\; \backslash times\; Y\; \backslash times\; Z)\; \backslash to\; N$, currying produces $\backslash text\{curry\}(f)\; \backslash colon\; X\; \backslash to\; (Y\; \backslash to\; (Z\; \backslash to\; N))$. That is, while an evaluation of the first function might be represented as $f(1,\; 2,\; 3)$, evaluation of the curried function would be represented as $f\_\backslash text\{curried\}(1)(2)(3)$, applying each argument in turn to a singleargument function returned by the previous invocation. Note that after calling $f\_\backslash 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 $f$ above, we might fix (or 'bind') the first argument, producing a function of type $\backslash text\{partial\}(f)\; \backslash colon\; (Y\; \backslash times\; Z)\; \backslash to\; N$. Evaluation of this function might be represented as $f\_\backslash 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 argument 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.
Partial application can be seen as evaluating a curried function at a fixed point, e.g. given $f\; \backslash colon\; (X\; \backslash times\; Y\; \backslash times\; Z)\; \backslash to\; N$ and $a\; \backslash in\; X$ then $\backslash text\{curry\}(\backslash text\{partial\}(f)\_a)(y)(z)\; =\; \backslash text\{curry\}(f)(a)(y)(z)$ or simply $\backslash text\{partial\}(f)\_a\; =\; \backslash text\{curry\}\_1(f)(a)$ where $\backslash text\{curry\}\_1$ curries f's first parameter.
Thus, partial application is reduced to a curried function at a fixed point. Further, a curried function at a fixed point is (trivially), a partial application. For further evidence, note that, given any function $f(x,y)$, a function $g(y,x)$ may be defined such that $g(y,x)\; =\; f(x,y)$. Thus, any partial application may be reduced to a single curry operation. As such, curry is more suitably defined as an operation which, in many theoretical cases, is often applied recursively, but which is theoretically indistinguishable (when considered as an operation) from a partial application.
So, a partial application can be defined as the objective result of a single application of the curry operator on some ordering of the inputs of some function.

