In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments (or a tuple of arguments) into evaluating a sequence of functions, each with a single argument. Currying is related to, but not the same as, partial application.
Contents
- Motivation
- Partial application
- Illustration
- History
- Definition
- Set theory
- Function spaces
- Algebraic topology
- Domain theory
- Lambda calculi
- Type theory
- Logic
- Category theory
- Contrast with partial function application
- References
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; this is interesting because it 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. It 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 f whose return value is another function g, and yields a new function f′ 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.
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 category which does allow currying is the closed monoidal category.
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.
Partial application
Currying resembles the process of evaluating a function of multiple variables, when done by hand, on paper, being careful to show all of the steps.
For example, given the function
On paper, using classical notation, this is usually done all in one step. However, each argument can be replaced sequentially as well. Each replacement results in a function taking exactly one argument.
This example is somewhat flawed, in that currying, while similar to partial function application, is not the same (see below).
Illustration
Currying is a method for producing a chain of functions, each taking exactly one argument. The construction is achieved by "hiding" all but one argument in another, new, curried function, whose job it is to return functions of the remaining arguments. This is explicitly (but informally) illustrated next.
Given a function f that takes two arguments x and y, that is,
one may then construct a new function hx, related to the original f. This form takes only one argument, y, and, given that argument, hx(y) returns f(x,y). That is,
Here, it should be clear that the subscript x on h is a notational device used to hide or salt away one of the arguments, putting it to the side, so that one gets to work with a function having only one argument. Currying abstracts this notational trick.
To complete the trick, the following will use the common notation
Consider now erasing the subscript x on hx. This yields the curried form h. It is a function that, given x, returns, as its "value", a different function hx which happens to be the function
or, in different (but equivalent) notation,
The function h itself may be written as
Given the above, one may now define currying: it is the function that, given some arbitrary f, returns the corresponding h. That is,
or, equivalently
This illustrates the fundamental, essential nature of currying: it is a mechanism for relocating an argument, by bundling it into a function that returns a function. That is, given a function f that returns a "value", one "constructs" a new function h that returns a function. A different way of understanding currying is to realize that it is just an algebraic game, a syntactic rearranging of symbols. One does not ask what the "meaning" of the symbols are; one only agrees to the rules for their rearrangement. To see this, note that the original function f itself may be written as
Comparing to the function h above, one sees that the two forms involve a re-arrangement of parenthesis, together with the conversion of a comma into an arrow.
Returning to the earlier example,
one then has that,
as the curried equivalent of the example above. Adding an argument to g then gives
and
The peeling away of arguments might be better understood by considering a function of, say, four arguments:
Proceeding as above, one is led to the form
which can be applied to a triple to get
The curried form is then properly written as
By continuing to play the algebraic game of re-arranging symbols, one is eventually led to the fully curried form
It is commonly understood that the arrow operator is right-associative, and so most of the parenthesis above are superfluous, and can be removed without altering the meaning. Thus, it is common to write
for the fully curried form of f.
History
The name "currying", coined by Christopher Strachey in 1967, is a reference to logician Haskell Curry. The alternative name "Schönfinkelisation" has been proposed as a reference to Moses Schönfinkel. In the mathematical context, the principle can be traced back to work in 1893 by Frege.
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. Let
Given a function
Set theory
In set theory, the notation
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
while uncurrying is the inverse map. If the set
This result motivates the exponential notation
which is sometimes called the exponential law. 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,
is continuous when
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
where
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 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,
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
where
The → operator is often considered right-associative, so the curried function type
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
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 logical theorem
Category theory
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. That is, there is a natural isomorphism between the morphisms from a binary product
Here, hom is written lower case, to indicate that it is the internal hom functor, distinguishing it from the external (upper-case) Hom. For the category of sets, the two are the same. When the product is the cartesian product, then the internal hom
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 Heyting algebras) 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 types 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 vector spaces 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 cobordisms 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.
Contrast with partial function application
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 whose arity is greater than two.
Given a function of type
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
Intuitively, partial function application says "if you fix the first arguments 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