Editing Currying (section)

=== 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.