Editing Currying (section)

== 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. The notation <math>X \to Y </math> denotes all [[Function (mathematics)|functions]] from <math>X</math> to <math>Y</math>. If <math>f</math> is such a function, we write <math>f \colon X \to Y </math>. Let <math>X \times Y</math> denote the [[ordered pair]]s of the elements of <math>X</math> and <math>Y</math> respectively, that is, the [[Cartesian product]] of <math>X</math> and <math>Y</math>. Here, <math>X</math> and <math>Y</math> may be sets, or they may be types, or they may be other kinds of objects, as explored below.

Given a function

:<math>f \colon (X \times Y) \to Z </math>,

'''currying''' constructs a new function

:<math>g \colon X \to (Y \to Z) </math>.

That is, <math>g</math> takes an argument of type <math>X</math> and returns a function of type <math>Y\to Z</math>. It is defined by

:<math>g(x)(y)=f(x,y)</math>

for <math>x</math> of type <math>X</math> and <math>y</math> of type <math>Y</math>. We then also write

:<math>\text{curry}(f)=g.</math>

'''Uncurrying''' is the reverse transformation, and is most easily understood in terms of its right adjoint, the [[apply|function <math>\operatorname{apply}.</math>]]

=== Set theory ===
In [[set theory]], the notation <math>Y^X</math> is used to denote the [[set (mathematics)|set]] of functions from the set <math>X</math> to the set <math>Y</math>. Currying is the [[natural equivalence|natural bijection]] between the set <math>A^{B\times C}</math> of functions from <math>B\times C</math> to <math>A</math>, and the set <math>(A^C)^B</math> of functions from <math>B</math> to the set of functions from <math>C</math> to <math>A</math>. In symbols:

:<math>A^{B\times C}\cong (A^C)^B</math>

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 functors|adjoint pair of functors]]: for every fixed set <math>C</math>, the functor <math>B\mapsto B\times C</math> is left adjoint to the functor <math>A \mapsto A^C</math>.

In the [[category of sets]], the [[Mathematical object|object]] <math>Y^X</math> is called the [[exponential object]].

=== Function spaces ===
In the theory of [[function space]]s, such as in [[functional analysis]] or [[homotopy theory]], one is commonly interested in [[continuous function]]s between [[topological space]]s. One writes <math>\text{Hom}(X,Y)</math> (the [[Hom functor]]) for the set of ''all'' functions from <math>X</math> to <math>Y</math>, and uses the notation <math>Y^X</math> to denote the subset of continuous functions. Here, <math>\text{curry}</math> is the [[bijection]]

:<math>\text{curry}:\text{Hom}(X\times Y, Z) \to \text{Hom}(X, \text{Hom}(Y,Z)) ,</math>

while uncurrying is the inverse map. If the set <math>Y^X</math> of continuous functions from <math>X</math> to <math>Y</math> is given the [[compact-open topology]], and if the space <math>Y</math> is [[locally compact Hausdorff]], then

:<math>\text{curry} : Z^{X\times Y}\to (Z^Y)^X</math>

is a [[homeomorphism]]. This is also the case when <math>X</math>, <math>Y</math> and <math>Y^X</math> are [[Compactly generated space|compactly generated]],<ref name="may">{{Cite book |last=May |first=Jon Peter |url=http://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf |title=A concise course in algebraic topology |date=1999 |publisher=University of Chicago Press |isbn=0-226-51183-9 |edition= |series=Chicago lectures in mathematics |location=Chicago, Ill. |pages=39–55 |oclc=41266205}}</ref>{{rp|at=chapter 5}}<ref>{{Cite web |date=28 May 2023 |title=compactly generated topological space |url=https://ncatlab.org/nlab/show/compactly+generated+topological+space |access-date= |website=nLab}}</ref> although there are more cases.<ref>{{Cite journal |last1=Tillotson |first1=J. |last2=Booth |first2=Peter I. |orig-date=Received 2 October 1978, revised 29 June 1979, published 1 May 1980 |title=Monoidal closed, Cartesian closed and convenient categories of topological spaces |url=https://msp.org/pjm/1980/88-1/pjm-v88-n1-p03-s.pdf |journal=Pacific Journal of Mathematics |location=Memorial University of Newfoundland |publisher=Mathematical Sciences Publishers |publication-place=Berkeley, California |publication-date=March 1980 |volume=88 |issue=1 |pages=35–53 |doi=10.2140/pjm.1980.88.35 |issn=0030-8730 |eissn=1945-5844}}</ref><ref>{{Cite web |date=11 August 2023 |title=convenient category of topological spaces |url=https://ncatlab.org/nlab/show/convenient+category+of+topological+spaces |access-date= |website=nLab}}</ref>

One useful corollary is that a function is continuous [[if and only if]] its curried form is continuous. Another important result is that the [[apply|application map]], usually called "evaluation" in this context, is continuous (note that [[eval]] is a strictly different concept in computer science.) That is,

<math>\begin{align} &&\text{eval}:Y^X \times X \to Y \\
                     && (f,x) \mapsto f(x) \end{align}</math>

is continuous when <math>Y^X</math> is compact-open and <math>Y</math> locally compact Hausdorff.<ref name="rotman">{{Cite book |last=Rotman |first=Joseph Jonah |url=https://books.google.com/books?id=waq9mwUmcQgC |title=An introduction to algebraic topology |date=1988 |publisher=Springer-Verlag |isbn=978-0-387-96678-6 |series=Graduate texts in mathematics; 119 |location=New York |chapter=Chapter 11 |oclc=17383909}}</ref> These two results are central for establishing the continuity of [[homotopy]], i.e. when <math>X</math> is the unit interval <math>I</math>, so that <math>Z^{I\times Y} \cong (Z^Y)^I</math> can be thought of as either a homotopy of two functions from <math>Y</math> to <math>Z</math>, or, equivalently, a single (continuous) path in <math>Z^Y</math>.

=== 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 suspension]]s; this is commonly written as
:<math>[\Sigma X,Z] \approxeq [X, \Omega Z]</math>
where <math>[A,B]</math> is the set of [[homotopy class]]es of maps <math>A \rightarrow B</math>, and <math>\Sigma A</math> is the [[Suspension (topology)|suspension]] of ''A'', and <math>\Omega A</math> is the [[loop space]] of ''A''. In essence, the suspension <math>\Sigma X</math> can be seen as the cartesian product of <math>X</math> with the unit interval, modulo an equivalence relation to turn the interval into a loop. The curried form then maps the space <math>X</math> to the space of functions from loops into <math>Z</math>, that is, from <math>X</math> into <math>\Omega Z</math>.<ref name=rotman/> Then <math>\text{curry}</math> is the [[adjoint functor]] that maps suspensions to loop spaces, and uncurrying is the dual.<ref name=rotman/>

The duality between the [[mapping cone (topology)|mapping cone]] and the mapping fiber ([[cofibration]] and [[fibration]])<ref name=may/>{{rp|at=chapters 6,7}} can be understood as a form of currying, which in turn leads to the duality of the [[long exact sequence|long exact]] and coexact [[Puppe sequence]]s.

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 (mathematics)|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 [[lattice (order)|lattices]] of [[partially ordered set]]s, <math>\text{curry}</math> is a [[continuous function]] when the lattice is given the [[Scott topology]].<ref>{{Cite book |last=Barendregt |first=Hendrik Pieter |title=The lambda calculus: its syntax and semantics |date=1984 |publisher=North-Holland, an imprint of Elsevier |isbn=978-0-444-87508-2 |edition=Rev. |series=Studies in logic and the foundations of mathematics |volume=103 |location= |chapter=Theorems 1.2.13, 1.2.14}}</ref> 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). More generally, Scott-continuous functions are now studied in [[domain theory]], which encompasses the study of [[denotational semantics]] of computer algorithms. Note that the Scott topology is quite different than many common topologies one might encounter in the [[category of topological spaces]]; the Scott topology is typically [[final topology|finer]], and is not [[sober space|sober]].

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" [[code refactoring|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 <math>f(x,y)</math> taking two arguments, and having the type <math>(X \times Y)\to Z</math>, which should be understood to mean that ''x'' must have the type <math>X</math>, ''y'' must have the type <math>Y</math>, and the function itself returns the type <math>Z</math>. The curried form of ''f'' is defined as

:<math>\text{curry}(f) = \lambda x.(\lambda y.(f(x,y)))</math>

where <math>\lambda</math> is the abstractor of lambda calculus. Since curry takes, as input, functions with the type <math>(X\times Y)\to Z</math>, one concludes that the type of curry itself is

:<math>\text{curry}:((X \times Y)\to Z) \to (X \to (Y \to Z))</math>

The → operator is often considered [[right-associative]], so the curried function type <math>X \to (Y \to Z)</math> is often written as <math>X \to Y \to Z</math>. Conversely, [[function application]] is considered to be [[Operator associativity|left-associative]], so that <math>f(x, y)</math> is equivalent to

:<math>((\text{curry}(f) \; x) \;y) = \text{curry}(f) \; x \;y</math>.

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 [[closure (computer science)|closure]]s; 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 <math>f \colon X \to Y </math>, the intent is that <math>X</math> and <math>Y</math> are [[type system|types]], while the arrow <math>\to</math> is a [[type constructor]], specifically, the [[function type]] or arrow type. Similarly, the Cartesian product <math>X \times Y</math> of types is constructed by the [[product type]] constructor <math>\times</math>.

The type-theoretical approach is expressed in programming languages such as [[ML (programming language)|ML]] and the languages derived from and inspired by it: [[Caml]], [[Haskell]], and [[F Sharp (programming language)|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 <math>((A \land B) \to C) \Leftrightarrow (A \to (B \to C))</math> (also known as [[Exportation (logic)|exportation]]), as [[tuple]]s ([[product type]]) corresponds to conjunction in logic, and function type corresponds to implication.

The [[exponential object]] <math>Q^P</math> in the category of [[Heyting algebra]]s is normally written as [[Material conditional|material implication]] <math>P\to Q</math>. Distributive Heyting algebras are [[Boolean algebra]]s, and the exponential object has the explicit form <math>\neg P \lor Q</math>, thus making it clear that the exponential object really is [[Material implication (rule of inference)|material implication]].<ref>{{Cite book |last1=Mac Lane |first1=Saunders |url= |title=Sheaves in Geometry and Logic: A First Introduction to Topos Theory |last2=Moerdijk |first2=Ieke |date=1992 |publisher=Springer-Verlag, part of Springer Science & Business Media |isbn=978-0-387-97710-2 |publication-place=New York |pages=48–57 |language=en |chapter=Chapter I. Categories of Functors; sections 7. Propositional Calculus, 8. Heyting Algebras, and 9. Quantifiers as Adjoints |chapter-url=https://books.google.com/books?id=SGwwDerbEowC&pg=PA48}}</ref>

=== 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 (category theory)|adjunction]] in [[cartesian closed category|cartesian closed categories]]. That is, there is a [[Natural transformation|natural]] [[isomorphism]] between the [[morphism (category theory)|morphisms]] from a [[product (category theory)|binary product]] <math>f \colon (X \times Y) \to Z </math> and the morphisms to an exponential object <math>g \colon X \to Z^Y </math>.

This generalizes to a broader result in [[closed monoidal category|closed monoidal categories]]: Currying is the statement that the [[monoidal category|tensor product]] and the [[internal Hom]] are [[adjoint functors]]; that is, for every object <math>B</math> there is a [[natural transformation|natural isomorphism]]:

:<math> \mathrm{Hom}(A\otimes B, C) \cong \mathrm{Hom}(A, B\Rightarrow C) .</math>

Here, ''Hom'' denotes the (external) Hom-functor of all morphisms in the category, while <math>B\Rightarrow C</math> denotes the internal hom functor in the closed monoidal category. For the [[category of sets]], the two are the same. When the product is the cartesian product, then the internal hom <math>B\Rightarrow C</math> becomes the exponential object <math>C^B</math>.

Currying can break down in one of two ways. One is if a category is not [[closed category|closed]], 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 not [[monoidal category|monoidal]], 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 of [[classical logic]]; the more general setting of closed monoidal categories is suitable for [[quantum computation]].<ref>{{Cite conference |last1=Abramsky |first1=Samson |last2=Coecke |first2=Bob |date=5 March 2007 |contribution=A categorical semantics of quantum protocols |doi=10.1109/LICS.2004.1319636 |title= Logic in Computer Science (LICS 2004): Proceedings, 19th Annual IEEE Symposium, Turku, Finland, 2004] |pages=415–425 |language=en |publisher=IEEE Computer Society Press |arxiv=quant-ph/0402130|isbn=978-0-7695-2192-3 }}</ref>

The difference between these two is that the [[product (mathematics)|product]] for cartesian categories (such as the [[category of sets]], [[complete partial order]]s or [[Heyting algebra]]s) 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 [[type system|types]] in the [[type theory]] of [[LISP]], [[scheme (programming language)|Scheme]] and many [[functional programming language]]s.

By contrast, the product for [[monoidal category|monoidal categories]] (such as [[Hilbert space]] and the [[vector space]]s 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 [[cobordism]]s in [[algebraic topology]], and to [[string theory]].<ref name="rosetta">{{Cite book |last1=Baez |first1=John C. |last2=Stay |first2=Mike |title=New Structures for Physics |chapter=Physics, Topology, Logic and Computation: A Rosetta Stone |date=6 June 2009 |editor-last=Coecke |editor-first=Bob |url=https://math.ucr.edu/home/baez/rosetta/rose3.pdf |series=Lecture Notes in Physics |publisher=Springer |publication-place=Berlin, Heidelberg |publication-date=5 July 2010 |volume=813: New Structures for Physics |pages=95–172 |arxiv=0903.0340 |doi=10.1007/978-3-642-12821-9_2 |isbn=978-3-642-12821-9 |s2cid=115169297 |archive-url=https://web.archive.org/web/20221205124044/https://math.ucr.edu/home/baez/rosetta/rose3.pdf |archive-date=5 December 2022}}</ref> The [[linear type system]], and [[linear logic]] are useful for describing [[synchronization primitive]]s, such as mutual exclusion locks, and the operation of vending machines.