Transforming a function in such a way that it only takes a single argument
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 formula_1 that takes two arguments, one from formula_2 and one from formula_3 and produces objects in formula_4 The curried form of this function treats the first argument as a parameter, so as to create a family of functions formula_5 The family is arranged so that for each object formula_6 in formula_7 there is exactly one function formula_8 
In this example, formula_9 itself becomes a function, that takes formula_10 as an argument, and returns a function that maps each formula_6 to formula_8 The proper notation for expressing this is verbose. The function formula_10 belongs to the set of functions formula_14 Meanwhile, formula_15 belongs to the set of functions formula_16 Thus, something that maps formula_6 to formula_15 will be of the type formula_19 With this notation, formula_9 is a function that takes objects from the first set, and returns objects in the second set, and so one writes formula_21 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 formula_22 that takes the pair formula_10 and formula_6 together as arguments, and returns formula_8 Using the same notation as above, partial application has the signature formula_26 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,
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 formula_10 whose return value is another function formula_28, and yields a new function formula_29 that takes as parameters the arguments for both formula_10 and formula_28, and returns, as a result, the application of formula_10 and subsequently, formula_28, to those arguments. The process can be iterated.
Motivation.
Currying provides a way for working with functions that take multiple arguments, and using them in frameworks where functions might take only one argument. For example, some analytical techniques can only be applied to functions with a single argument. Practical functions frequently take more arguments than this. Frege showed that it was sufficient to provide solutions for the single argument case, as it was possible to transform a function with multiple arguments into a chain of single-argument functions instead. This transformation is the process now known as currying. All "ordinary" functions that might typically be encountered in mathematical analysis or in computer programming can be curried. However, there are categories in which currying is not possible; the most general categories which allow currying are the closed monoidal categories.
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 multi-argument 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.
History.
The "Curry" in "Currying" is a reference to logician Haskell Curry, who used the concept extensively, but Moses Schönfinkel had the idea six years before Curry. The alternative name "Schönfinkelisation" has been proposed. In the mathematical context, the principle can be traced back to work in 1893 by Frege.
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 that source introduces the concept as "a device originated by Schönfinkel", and the term "currying" is not used, while Curry is mentioned later in the context of higher-order functions. John C. Reynolds defined "currying" in a 1972 paper, but did not claim to have coined the term.
Definition.
Currying is most easily understood by starting with an informal definition, which can then be molded to fit many different domains. First, there is some notation to be established. The notation formula_34 denotes all functions from formula_2 to formula_36. If formula_10 is such a function, we write formula_38. Let formula_39 denote the ordered pairs of the elements of formula_2 and formula_36 respectively, that is, the Cartesian product of formula_2 and formula_36. Here, formula_2 and formula_36 may be sets, or they may be types, or they may be other kinds of objects, as explored below.
Given a function
formula_46,
currying constructs a new function
formula_47.
That is, formula_28 takes an argument of type formula_2 and returns a function of type formula_50. It is defined by
formula_51
for formula_6 of type formula_2 and formula_54 of type formula_36. We then also write
formula_56
Uncurrying is the reverse transformation, and is most easily understood in terms of its right adjoint, the function formula_57
Set theory.
In set theory, the notation formula_58 is used to denote the set of functions from the set formula_2 to the set formula_36. Currying is the natural bijection between the set formula_61 of functions from formula_62 to formula_63, and the set formula_64 of functions from formula_65 to the set of functions from formula_66 to formula_63. In symbols:
formula_68
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 pair of functors: for every fixed set formula_66, the functor formula_70 is left adjoint to the functor formula_71.
In the category of sets, the object formula_58 is called the exponential object.
Function spaces.
In the theory of function spaces, such as in functional analysis or homotopy theory, one is commonly interested in continuous functions between topological spaces. One writes formula_73 (the Hom functor) for the set of "all" functions from formula_2 to formula_36, and uses the notation formula_58 to denote the subset of continuous functions. Here, formula_77 is the bijection
formula_78
while uncurrying is the inverse map. If the set formula_58 of continuous functions from formula_2 to formula_36 is given the compact-open topology, and if the space formula_36 is locally compact Hausdorff, then
formula_83
is a homeomorphism. This is also the case when formula_2, formula_36 and formula_58 are compactly generated,chapter 5 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 application map, usually called "evaluation" in this context, is continuous (note that eval is a strictly different concept in computer science.) That is,
formula_87
is continuous when formula_58 is compact-open and formula_36 locally compact Hausdorff. These two results are central for establishing the continuity of homotopy, i.e. when formula_2 is the unit interval formula_91, so that formula_92 can be thought of as either a homotopy of two functions from formula_36 to formula_94, or, equivalently, a single (continuous) path in formula_95.
Algebraic topology.
In algebraic topology, currying serves as an example of Eckmann–Hilton duality, and, as such, plays an important role in a variety of different settings. For example, loop space is adjoint to reduced suspensions; this is commonly written as
formula_96
where formula_97 is the set of homotopy classes of maps formula_98, and formula_99 is the suspension of "A", and formula_100 is the loop space of "A". In essence, the suspension formula_101 can be seen as the cartesian product of formula_2 with the unit interval, modulo an equivalence relation to turn the interval into a loop. The curried form then maps the space formula_2 to the space of functions from loops into formula_94, that is, from formula_2 into formula_106. Then formula_77 is the adjoint functor that maps suspensions to loop spaces, and uncurrying is the dual.
The duality between the mapping cone and the mapping fiber (cofibration and fibration)chapters 6,7 can be understood as a form of currying, which in turn leads to the duality of the long exact and coexact Puppe sequences.
In homological algebra, the relationship between currying and uncurrying is known as tensor-hom 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.
Domain theory.
In order theory, that is, the theory of lattices of partially ordered sets, formula_77 is a continuous function when the lattice is given the Scott topology. Scott-continuous functions were first investigated in the attempt to provide a semantics for lambda calculus (as ordinary set theory is inadequate to do this). More generally, Scott-continuous functions are now studied in domain theory, which encompasses the study of denotational semantics of computer algorithms. Note that the Scott topology is quite different than many common topologies one might encounter in the category of topological spaces; the Scott topology is typically finer, and is not sober.
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" refactored from one to the other.
Lambda calculi.
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. Consider a function formula_109 taking two arguments, and having the type formula_110, which should be understood to mean that "x" must have the type formula_2, "y" must have the type formula_36, and the function itself returns the type formula_94. The curried form of "f" is defined as
formula_114
where formula_115 is the abstractor of lambda calculus. Since curry takes, as input, functions with the type formula_116, one concludes that the type of curry itself is
formula_117
The → operator is often considered right-associative, so the curried function type formula_118 is often written as formula_119. Conversely, function application is considered to be left-associative, so that formula_120 is equivalent to
formula_121.
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.
Type theory.
In type theory, the general idea of a type system in computer science is formalized into a specific algebra of types. For example, when writing formula_38, the intent is that formula_2 and formula_36 are types, while the arrow formula_125 is a type constructor, specifically, the function type or arrow type. Similarly, the Cartesian product formula_39 of types is constructed by the product type constructor formula_127.
The type-theoretical approach is expressed in programming languages such as ML and the languages derived from and inspired by it: Caml, Haskell, and F#.
The type-theoretical 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 simply-typed 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 re-interpreted as logics (via Curry–Howard correspondence), and as other types of mathematical systems, as explored further, below.
Logic.
Under the Curry–Howard correspondence, the existence of currying and uncurrying is equivalent to the