Currying

Inmathematicsandcomputer science,curryingis the technique of translating afunctionthat takes multipleargumentsinto a sequence of families of functions, each taking a single argument.
In the prototypical example, one begins with a functionf:(X×Y)→Z{\displaystyle f:(X\times Y)\to Z}that takes two arguments, one fromX{\displaystyle X}and one fromY,{\displaystyle Y,}and produces objects inZ.{\displaystyle Z.}The curried form of this function treats the first argument as a parameter, so as to create a family of functionsfx:Y→Z.{\displaystyle f_{x}:Y\to Z.}The family is arranged so that for each objectx{\displaystyle x}inX,{\displaystyle X,}there is exactly one functionfx.{\displaystyle f_{x}.}
In this example,curry{\displaystyle {\mbox{curry}}}itself becomes a function, that takesf{\displaystyle f}as an argument, and returns a function that maps eachx{\displaystyle x}tofx.{\displaystyle f_{x}.}The proper notation for expressing this is verbose. The functionf{\displaystyle f}belongs to the set of functions(X×Y)→Z.{\displaystyle (X\times Y)\to Z.}Meanwhile,fx{\displaystyle f_{x}}belongs to the set of functionsY→Z.{\displaystyle Y\to Z.}Thus, something that mapsx{\displaystyle x}tofx{\displaystyle f_{x}}will be of the typeX→[Y→Z].{\displaystyle X\to [Y\to Z].}With this notation,curry{\displaystyle {\mbox{curry}}}is a function that takes objects from the first set, and returns objects in the second set, and so one writescurry:[(X×Y)→Z]→(X→[Y→Z]).{\displaystyle {\mbox{curry}}:[(X\times Y)\to Z]\to (X\to [Y\to Z]).}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 functionapply{\displaystyle {\mbox{apply}}}that takes the pairf{\displaystyle f}andx{\displaystyle x}together as arguments, and returnsfx.{\displaystyle f_{x}.}Using the same notation as above, partial application has the signatureapply:([(X×Y)→Z]×X)→[Y→Z].{\displaystyle {\mbox{apply}}:([(X\times Y)\to Z]\times X)\to [Y\to Z].}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. Infunctional programminglanguages, and many others, it provides a way of automatically managing how arguments are passed to functions and exceptions. Intheoretical 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 theclosed monoidal categories, which underpins a vast generalization of theCurry–Howard correspondenceof proofs and programs to a correspondence with many other structures, including quantum mechanics, cobordisms and string theory.
The concept of currying was introduced byGottlob Frege,developed byMoses Schönfinkel,and further developed byHaskell Curry.
Uncurryingis thedualtransformation to currying, and can be seen as a form ofdefunctionalization. It takes afunctionf{\displaystyle f}whose return value is another functiong{\displaystyle g}, and yields a new functionf′{\displaystyle f'}that takes as parameters the arguments for bothf{\displaystyle f}andg{\displaystyle g}, and returns, as a result, the application off{\displaystyle f}and subsequently,g{\displaystyle g}, to those arguments. The process can be iterated.
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, someanalytical techniquescan only be applied tofunctionswith a single argument. Practical functions frequently take more arguments than this.Fregeshowed 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 inmathematical analysisor incomputer programmingcan be curried.  However, there are categories in which currying is not possible; the most general categories which allow currying are theclosed monoidal categories.
Someprogramming languagesalmost always use curried functions to achieve multiple arguments; notable examples areMLandHaskell, where in both cases all functions have exactly one argument. This property is inherited fromlambda calculus, where multi-argument functions are usually represented in curried form.
Currying is related to, but not the same aspartial application.In practice, the programming technique ofclosurescan be used to perform partial application and a kind of currying, by hiding arguments in an environment that travels with the curried function.
The "Curry" in "Currying" is a reference to logicianHaskell Curry, who used the concept extensively, butMoses Schönfinkelhad 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 byFrege.
The originator of the word "currying" is not clear.David Turnersays the word was coined byChristopher Stracheyin his 1967 lecture notesFundamental 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. Reynoldsdefined "currying" in a 1972 paper, but did not claim to have coined the term.
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 notationX→Y{\displaystyle X\to Y}denotes allfunctionsfromX{\displaystyle X}toY{\displaystyle Y}. Iff{\displaystyle f}is such a function, we writef:X→Y{\displaystyle f\colon X\to Y}. LetX×Y{\displaystyle X\times Y}denote theordered pairsof the elements ofX{\displaystyle X}andY{\displaystyle Y}respectively, that is, theCartesian productofX{\displaystyle X}andY{\displaystyle Y}. Here,X{\displaystyle X}andY{\displaystyle Y}may be sets, or they may be types, or they may be other kinds of objects, as explored below.
Given a function
curryingconstructs a new function
That is,g{\displaystyle g}takes an argument of typeX{\displaystyle X}and returns a function of typeY→Z{\displaystyle Y\to Z}. It is defined by
forx{\displaystyle x}of typeX{\displaystyle X}andy{\displaystyle y}of typeY{\displaystyle Y}. We then also write
Uncurryingis the reverse transformation, and is most easily understood in terms of its right adjoint, thefunctionapply.{\displaystyle \operatorname {apply} .}
Inset theory, the notationYX{\displaystyle Y^{X}}is used to denote thesetof functions from the setX{\displaystyle X}to the setY{\displaystyle Y}. Currying is thenatural bijectionbetween the setAB×C{\displaystyle A^{B\times C}}of functions fromB×C{\displaystyle B\times C}toA{\displaystyle A}, and the set(AC)B{\displaystyle (A^{C})^{B}}of functions fromB{\displaystyle B}to the set of functions fromC{\displaystyle C}toA{\displaystyle A}. In symbols:
Indeed, it is this natural bijection that justifies theexponential notationfor the set of functions. As is the case in all instances of currying, the formula above describes anadjoint pair of functors: for every fixed setC{\displaystyle C}, the functorB↦B×C{\displaystyle B\mapsto B\times C}is left adjoint to the functorA↦AC{\displaystyle A\mapsto A^{C}}.
In thecategory of sets, theobjectYX{\displaystyle Y^{X}}is called theexponential object.
In the theory offunction spaces, such as infunctional analysisorhomotopy theory, one is commonly interested incontinuous functionsbetweentopological spaces. One writesHom(X,Y){\displaystyle {\text{Hom}}(X,Y)}(theHom functor) for the set ofallfunctions fromX{\displaystyle X}toY{\displaystyle Y}, and uses the notationYX{\displaystyle Y^{X}}to denote the subset of continuous functions. Here,curry{\displaystyle {\text{curry}}}is thebijection
while uncurrying is the inverse map. If the setYX{\displaystyle Y^{X}}of continuous functions fromX{\displaystyle X}toY{\displaystyle Y}is given thecompact-open topology, and if the spaceY{\displaystyle Y}islocally compact Hausdorff, then
is ahomeomorphism. This is also the case whenX{\displaystyle X},Y{\displaystyle Y}andYX{\displaystyle Y^{X}}arecompactly generated,although there are more cases.
One useful corollary is that a function is continuousif and only ifits curried form is continuous. Another important result is that theapplication map, usually called "evaluation" in this context, is continuous (note thatevalis a strictly different concept in computer science.) That is,
eval:YX×X→Y(f,x)↦f(x){\displaystyle {\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}}
is continuous whenYX{\displaystyle Y^{X}}is compact-open andY{\displaystyle Y}locally compact Hausdorff.These two results are central for establishing the continuity ofhomotopy, i.e. whenX{\displaystyle X}is the unit intervalI{\displaystyle I}, so thatZI×Y≅(ZY)I{\displaystyle Z^{I\times Y}\cong (Z^{Y})^{I}}can be thought of as either a homotopy of two functions fromY{\displaystyle Y}toZ{\displaystyle Z}, or, equivalently, a single (continuous) path inZY{\displaystyle Z^{Y}}.
Inalgebraic topology, currying serves as an example ofEckmann–Hilton duality, and, as such, plays an important role in a variety of different settings. For example,loop spaceis adjoint toreduced suspensions; this is commonly written as
where[A,B]{\displaystyle [A,B]}is the set ofhomotopy classesof mapsA→B{\displaystyle A\rightarrow B}, andΣA{\displaystyle \Sigma A}is thesuspensionofA, andΩA{\displaystyle \Omega A}is theloop spaceofA. In essence, the suspensionΣX{\displaystyle \Sigma X}can be seen as the cartesian product ofX{\displaystyle X}with the unit interval, modulo an equivalence relation to turn the interval into a loop. The curried form then maps the spaceX{\displaystyle X}to the space of functions from loops intoZ{\displaystyle Z}, that is, fromX{\displaystyle X}intoΩZ{\displaystyle \Omega Z}.Thencurry{\displaystyle {\text{curry}}}is theadjoint functorthat maps suspensions to loop spaces, and uncurrying is the dual.
The duality between themapping coneand the mapping fiber (cofibrationandfibration)can be understood as a form of currying, which in turn leads to the duality of thelong exactand coexactPuppe sequences.
Inhomological algebra, the relationship between currying and uncurrying is known astensor-hom adjunction. Here, an interesting twist arises: theHom functorand thetensor productfunctor might notliftto anexact sequence; this leads to the definition of theExt functorand theTor functor.
Inorder theory, that is, the theory oflatticesofpartially ordered sets,curry{\displaystyle {\text{curry}}}is acontinuous functionwhen the lattice is given theScott topology.Scott-continuous functions were first investigated in the attempt to provide a semantics forlambda calculus(as ordinary set theory is inadequate to do this). More generally, Scott-continuous functions are now studied indomain theory, which encompasses the study ofdenotational semanticsof computer algorithms. Note that the Scott topology is quite different than many common topologies one might encounter in thecategory of topological spaces; the Scott topology is typicallyfiner, and is notsober.
The notion of continuity makes its appearance inhomotopy 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"refactoredfrom one to the other.
Intheoretical computer science, currying provides a way to study functions with multiple arguments in very simple theoretical models, such as thelambda calculus, in which functions only take a single argument. Consider a functionf(x,y){\displaystyle f(x,y)}taking two arguments, and having the type(X×Y)→Z{\displaystyle (X\times Y)\to Z}, which should be understood to mean thatxmust have the typeX{\displaystyle X},ymust have the typeY{\displaystyle Y}, and the function itself returns the typeZ{\displaystyle Z}. The curried form offis defined as
whereλ{\displaystyle \lambda }is the abstractor of lambda calculus. Since curry takes, as input, functions with the type(X×Y)→Z{\displaystyle (X\times Y)\to Z}, one concludes that the type of curry itself is
The → operator is often consideredright-associative, so the curried function typeX→(Y→Z){\displaystyle X\to (Y\to Z)}is often written asX→Y→Z{\displaystyle X\to Y\to Z}. Conversely,function applicationis considered to beleft-associative, so thatf(x,y){\displaystyle 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 anyprogramming languagethat supportsclosures; 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.
Intype theory, the general idea of atype systemin computer science is formalized into a specific algebra of types. For example, when writingf:X→Y{\displaystyle f\colon X\to Y}, the intent is thatX{\displaystyle X}andY{\displaystyle Y}aretypes, while the arrow→{\displaystyle \to }is atype constructor, specifically, thefunction typeor arrow type. Similarly, the Cartesian productX×Y{\displaystyle X\times Y}of types is constructed by theproduct typeconstructor×{\displaystyle \times }.
The type-theoretical approach is expressed in programming languages such asMLand the languages derived from and inspired by it:Caml,Haskell, andF#.
The type-theoretical approach provides a natural complement to the language ofcategory theory, as discussed below. This is because categories, and specifically,monoidal categories, have aninternal language, withsimply-typed lambda calculusbeing 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 (viaCurry–Howard correspondence), and as other types of mathematical systems, as explored further, below.
Under theCurry–Howard correspondence, the existence of currying and uncurrying is equivalent to the logical theorem((A∧B)→C)⇔(A→(B→C)){\displaystyle ((A\land B)\to C)\Leftrightarrow (A\to (B\to C))}(also known asexportation), astuples(product type) corresponds to conjunction in logic, and function type corresponds to implication.
Theexponential objectQP{\displaystyle Q^{P}}in the category ofHeyting algebrasis normally written asmaterial implicationP→Q{\displaystyle P\to Q}. Distributive Heyting algebras areBoolean algebras, and the exponential object has the explicit form¬P∨Q{\displaystyle \neg P\lor Q}, thus making it clear that the exponential object really ismaterial implication.
The above notions of currying and uncurrying find their most general, abstract statement incategory theory. Currying is auniversal propertyof anexponential object, and gives rise to anadjunctionincartesian closed categories. That is, there is anaturalisomorphismbetween themorphismsfrom abinary productf:(X×Y)→Z{\displaystyle f\colon (X\times Y)\to Z}and the morphisms to an exponential objectg:X→ZY{\displaystyle g\colon X\to Z^{Y}}.
This generalizes to a broader result inclosed monoidal categories: Currying is the statement that thetensor productand theinternal Homareadjoint functors; that is, for every objectB{\displaystyle B}there is anatural isomorphism:
Here,Homdenotes the (external) Hom-functor of all morphisms in the category, whileB⇒C{\displaystyle B\Rightarrow C}denotes the internal hom functor in the closed monoidal category. For thecategory of sets, the two are the same. When the product is the cartesian product, then the internal homB⇒C{\displaystyle B\Rightarrow C}becomes the exponential objectCB{\displaystyle C^{B}}.
Currying can break down in one of two ways. One is if a category is notclosed, 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 notmonoidal, 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 ofclassical logic; the more general setting of closed monoidal categories is suitable forquantum computation.
The difference between these two is that theproductfor cartesian categories (such as thecategory of sets,complete partial ordersorHeyting algebras) is just theCartesian product; it is interpreted as anordered pairof items (or a list).Simply typed lambda calculusis theinternal languageof cartesian closed categories; and it is for this reason that pairs and lists are the primarytypesin thetype theoryofLISP,Schemeand manyfunctional programming languages.
By contrast, the product formonoidal categories(such asHilbert spaceand thevector spacesoffunctional analysis) is thetensor product. The internal language of such categories islinear logic, a form ofquantum logic; the correspondingtype systemis thelinear type system. Such categories are suitable for describingentangled quantum states, and, more generally, allow a vast generalization of theCurry–Howard correspondencetoquantum mechanics, tocobordismsinalgebraic topology, and tostring theory.Thelinear type system, andlinear logicare useful for describingsynchronization primitives, such as mutual exclusion locks, and the operation of vending machines.
Currying and partial function application are often conflated.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 whosearityis greater than two.
Given a function of typef:(X×Y×Z)→N{\displaystyle f\colon (X\times Y\times Z)\to N}, currying producescurry(f):X→(Y→(Z→N)){\displaystyle {\text{curry}}(f)\colon X\to (Y\to (Z\to N))}. That is, while an evaluation of the first function might be represented asf(1,2,3){\displaystyle f(1,2,3)}, evaluation of the curried function would be represented asfcurried(1)(2)(3){\displaystyle f_{\text{curried}}(1)(2)(3)}, applying each argument in turn to a single-argument function returned by the previous invocation. Note that after callingfcurried(1){\displaystyle 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 applicationrefers to the process of fixing a number of arguments to a function, producing another function of smaller arity. Given the definition off{\displaystyle f}above, we might fix (or 'bind') the first argument, producing a function of typepartial(f):(Y×Z)→N{\displaystyle {\text{partial}}(f)\colon (Y\times Z)\to N}. Evaluation of this function might be represented asfpartial(2,3){\displaystyle 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 firstargumentof the function, you get a function of the remaining arguments". For example, if functiondivstands for the division operationx/y, thendivwith the parameterxfixed at 1 (i.e.,div1) is another function: the same as the functioninvthat returns the multiplicative inverse of its argument, defined byinv(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 toplus_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. givenf:(X×Y×Z)→N{\displaystyle f\colon (X\times Y\times Z)\to N}anda∈X{\displaystyle a\in X}thencurry(partial(f)a)(y)(z)=curry(f)(a)(y)(z){\displaystyle {\text{curry}}({\text{partial}}(f)_{a})(y)(z)={\text{curry}}(f)(a)(y)(z)}or simplypartial(f)a=curry1(f)(a){\displaystyle {\text{partial}}(f)_{a}={\text{curry}}_{1}(f)(a)}wherecurry1{\displaystyle {\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 functionf(x,y){\displaystyle f(x,y)}, a functiong(y,x){\displaystyle g(y,x)}may be defined such thatg(y,x)=f(x,y){\displaystyle 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.