This is a somewhat informal example; more precise definitions of what is meant by "object" and "function" are given below.
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.
For example, some analytical techniques can only be applied to functions with a single argument.
[14] All "ordinary" functions that might typically be encountered in mathematical analysis or in computer programming can be curried.
This property is inherited from lambda calculus, where multi-argument functions are usually represented in curried form.
[15] In the mathematical context, the principle can be traced back to work in 1893 by Frege.
David Turner says the word was coined by Christopher Strachey in his 1967 lecture notes Fundamental Concepts in Programming Languages,[16] 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.
[7] John C. Reynolds defined "currying" in a 1972 paper, but did not claim to have coined the term.
[8] Currying is most easily understood by starting with an informal definition, which can then be molded to fit many different domains.
We then also write Uncurrying is the reverse transformation, and is most easily understood in terms of its right adjoint, the function
In symbols: 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
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.)
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 where
is the adjoint functor that maps suspensions to loop spaces, and uncurrying is the dual.
[21] The duality between the mapping cone and the mapping fiber (cofibration and fibration)[17]: 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.
[22] 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).
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.
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.
The type-theoretical approach provides a natural complement to the language of category theory, as discussed below.
[23] The above notions of currying and uncurrying find their most general, abstract statement in category theory.
Currying is a universal property of an exponential object, and gives rise to an adjunction in cartesian closed categories.
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
there is a natural isomorphism: Here, Hom denotes the (external) Hom-functor of all morphisms in the category, while
[24] The difference between these two is that the product for cartesian categories (such as the category of sets, complete partial orders or Heyting algebras) is just the Cartesian product; it is interpreted as an ordered pair of items (or a list).
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 cobordisms in algebraic topology, and to string theory.
, applying each argument in turn to a single-argument function returned by the previous invocation.
Partial application can be seen as evaluating a curried function at a fixed point, e.g. given