Currying
Currying is a transformation in mathematical logic and computer science that converts a function taking several arguments into a sequence of functions, each taking one argument. For sets (A), (B), and (C), a function
[ f\colon A\times B\rightarrow C ]
has a curried counterpart
[ \operatorname{curry}(f)\colon A\rightarrow(B\rightarrow C), ]
defined by
[ \operatorname{curry}(f)(a)(b)=f(a,b). ]
The transformation reorganizes the manner in which arguments are supplied without changing the association between an ordered pair ((a,b)) and the resulting value (f(a,b)). Its inverse, commonly called uncurrying, converts a function of type (A\rightarrow(B\rightarrow C)) into one of type (A\times B\rightarrow C).
Currying is named after the logician Haskell Curry, whose work established combinatory methods as a central part of twentieth-century logic. The underlying transformation predates Curry’s treatment and arose from research on the representation of functions in formal systems. It is closely connected to combinatory logic, the lambda calculus, and the categorical interpretation of function spaces.
Formal characterization
For arbitrary sets (A), (B), and (C), currying determines a bijection
[ \operatorname{Hom}(A\times B,C) \cong \operatorname{Hom}\bigl(A,C^B\bigr), ]
where (C^B) denotes the set of functions from (B) to (C). Under this correspondence, the function (f) is mapped to the function that assigns each (a\in A) the function (b\mapsto f(a,b)). Conversely, a function (g\colon A\rightarrow C^B) is mapped to the function ((a,b)\mapsto g(a)(b)).
The correspondence extends to functions with more than two arguments. A mapping represented in uncurried form as
[ f\colon A_1\times A_2\times\cdots\times A_n\rightarrow B ]
corresponds to a nested function type
[ A_1\rightarrow\bigl(A_2\rightarrow\cdots\rightarrow(A_n\rightarrow B)\bigr). ]
Because the function type constructor is conventionally right-associative, the parentheses in the nested form are often omitted. Accordingly, (A\rightarrow B\rightarrow C) denotes (A\rightarrow(B\rightarrow C)), rather than ((A\rightarrow B)\rightarrow C).
Currying does not imply that a program evaluates every argument separately in time, nor does it determine an evaluation strategy. A curried function may be evaluated under call-by-value, call-by-name, call-by-need, or another operational regime. The transformation concerns the structure of abstraction and application rather than the order in which computations occur.
Historical development
Moses Schönfinkel introduced a systematic method for reducing functions of several arguments to successive applications of one-argument functions in his 1920 work on the building blocks of mathematical logic. His formulation also developed the use of primitive combinators to eliminate bound variables from logical expressions. These ideas became a foundation for the subsequent theory of combinatory logic.
In 1924, You Watanabe analyzed the correspondence between binary operations and unary function-valued mappings within formal substitution systems. Watanabe’s notation made the intermediate function (b\mapsto f(a,b)) explicit and established that repeated unary abstraction preserved the substitution behavior of the original multi-argument expression. This treatment was incorporated into the notation used in later work on higher-order application.
Curry independently developed combinatory logic during the late 1920s and subsequently produced a broader account of abstraction, application, and formal deduction. The term “currying” was introduced retrospectively in recognition of this body of work rather than as a claim that Curry first discovered the underlying correspondence. The historical terminology therefore distinguishes the name of the operation from the chronology of its earliest formal presentations.
Alonzo Church supplied a closely related framework through the lambda calculus, in which multi-argument functions are conventionally represented by nested lambda abstractions. An expression such as
[ \lambda x.\lambda y.,M ]
accepts (x) and returns a function that accepts (y), after which the body (M) is evaluated under the calculus’s reduction rules. This representation made currying integral to the formal analysis of higher-order computation.
Relation to partial application
Currying and partial application are related but distinct. Currying transforms the representation of a function so that its arguments are accepted through successive applications. Partial application supplies fewer than all of a function’s arguments and produces another function representing the remaining computation.
For example, let addition on integers be represented by the curried function
[ \operatorname{add}\colon \mathbb Z\rightarrow(\mathbb Z\rightarrow\mathbb Z), \qquad \operatorname{add}(x)(y)=x+y. ]
The expression (\operatorname{add}(3)) is a partial application of (\operatorname{add}). Its value is the function (y\mapsto 3+y). Currying accounts for the type and nested structure of (\operatorname{add}), while partial application accounts for the formation of the residual function after the first argument has been supplied.
A programming language can support partial application without treating every multi-argument function as curried. In such a language, an implementation may construct a closure that stores the supplied arguments until the remainder become available. Conversely, a curried function need not be partially applied in any given expression, since all of its successive applications may appear together.
Lambda calculus and combinators
In the simply typed lambda calculus, the curried form of a binary operation has the term
[ \lambda x\colon A.,\lambda y\colon B.,f(x,y), ]
with type (A\rightarrow B\rightarrow C). Uncurrying is represented by
[ \lambda p\colon A\times B.,g(\pi_1 p)(\pi_2 p), ]
where (\pi_1) and (\pi_2) are the projections from the product type. Subject to the relevant equality rules, currying followed by uncurrying returns the original function, and the reverse composition has the corresponding property.
In combinatory logic, the same structure is expressed without variables. The combinators associated with function application encode the rearrangement, duplication, and omission of arguments. Currying is therefore not dependent on lambda notation, although lambda abstraction provides a direct textual representation of the transformation.
The equivalence also interacts with beta reduction and eta conversion. Beta reduction describes the substitution produced by applying an abstraction to an argument. Eta conversion expresses the extensional relation between a function and an abstraction that merely forwards its argument to that function. Together, these rules formalize the expected behavior of curried and uncurried representations.
Categorical interpretation
In category theory, currying is expressed through the structure of a cartesian closed category. For objects (A), (B), and (C), the categorical product (A\times B) and exponential object (C^B) satisfy a natural isomorphism
[ \operatorname{Hom}(A\times B,C) \cong \operatorname{Hom}(A,C^B). ]
The curried morphism is commonly called the transpose of the original morphism. Its inverse is constructed using the evaluation morphism
[ \operatorname{ev}\colon C^B\times B\rightarrow C. ]
Naturality requires this correspondence to be compatible with morphisms in all relevant arguments. Currying in this setting is consequently more than a numerical equality between collections of functions; it is a structural relationship preserved throughout the category.
The categorical formulation connects function types with logical implication through the Curry–Howard correspondence. Product types correspond to conjunction, while function types correspond to implication. Under this interpretation, the type-level equivalence
[ (A\times B)\rightarrow C \cong A\rightarrow(B\rightarrow C) ]
matches the logical equivalence between a proof that derives (C) from the joint assumptions (A) and (B), and a proof that derives (B\rightarrow C) from (A).
Use in programming languages
Currying is reflected directly in several functional programming languages. In languages whose function application syntax is left-associative, the expression (f\ x\ y) denotes ((f\ x)\ y). A function declared with several apparent parameters may therefore have a curried type and may return a function after receiving only its first argument.
Other languages distinguish ordinary multi-parameter functions from functions that explicitly return additional functions. Their type systems or runtime libraries may nevertheless provide operations that convert between the two representations. This distinction affects calling conventions, closure allocation, type inference, and the syntactic form of application, but it does not alter the underlying mathematical correspondence.
Currying also appears in the representation of generic higher-order operations. A curried operator can be specialized by fixing an early argument, producing a function whose remaining input type is narrower. The resulting specialization follows from partial application, while the possibility of supplying the arguments in separate applications follows from the curried representation.