Currying - Mathematical View

Mathematical View

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.

In a set-theoretic paradigm, currying is the natural correspondence between the set of functions from to, and the set of functions from to the set of functions from to . In category theory, currying can be found in the universal property of an exponential object, which gives rise to the following adjunction in cartesian closed categories: There is a natural isomorphism between the morphisms from a binary product and the morphisms to an exponential object . In other words, currying is the statement that product and Hom are adjoint functors; that is there is a natural transformation:

This is the key property of being a Cartesian closed category, and more generally, a closed monoidal category. The latter, though more rarely discussed, is interesting, as it is the suitable setting for quantum computation, whereas the former is sufficient for classical logic. The difference is that the Cartesian product can be interpreted simply as a pair of items (or a list), whereas the tensor product, used to define a monoidal category, is suitable for describing entangled quantum states.

Under the Curry–Howard correspondence, the existence of currying and uncurrying is equivalent to the logical theorem, as tuples (product type) corresponds to conjunction in logic, and function type corresponds to implication.

Curry is a continuous function in the Scott topology.