Editing Currying (section)

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