Currying

And what about a function of two variables? Do those even exist? Simple answer: no, they don't. All right, all right, I'm kidding. They do — they're just wrapped in layers like an onion, and that concept is called currying, after Haskell Curry. Yes, that very Haskell Curry, the one the Haskell language is named after too.

f(x,y)\displaystyle f(x, y) \quad f\displaystyle \rightsquigarrow\quad f =λx.λy.M,fab\displaystyle = \lambda x.\,\lambda y.\,M, \qquad f\,a\,b =(fa)b\displaystyle = (f\,a)\,b
(1.9)

Formally this is an isomorphism, that is, a bijection between two sets of functions.

Hom(A×B,C)  \displaystyle \mathrm{Hom}(A \times B,\, C) \;   Hom(A,Hom(B,C))\displaystyle \cong\; \mathrm{Hom}(A,\, \mathrm{Hom}(B,\, C))
(1.10)

On the left of the formula are functions from the pair A×BA \times B to CC; on the right, functions from AA to functions from BB to CC. To each two-argument function g ⁣:A×Bg \colon A \times B C\to C corresponds exactly one curried g^ ⁣:A\hat g \colon A (BC)\to (B \to C) by the rule g^(a)(b)\hat g(a)(b) =g(a,b)= g(a, b), and conversely — g(a,b)g(a, b) =g^(a)(b)= \hat g(a)(b). These two passages are mutually inverse, losing and adding nothing, so the two sets of functions are simply indistinguishable.

A few examples from Haskell:

-- the type of a multi-argument function is a right-associative chain of arrows
f :: a -> b -> c   -- the same as a -> (b -> c)

-- partial application: add 2 is an "under-applied" function
add :: Int -> Int -> Int
add x y = x + y
add2 :: Int -> Int
add2 = add 2
map add2 [1, 2, 3]  -- [3, 4, 5]

-- curry and uncurry are the witnesses of the isomorphism
curry   :: ((a, b) -> c) -> a -> b -> c
uncurry :: (a -> b -> c) -> (a, b) -> c

-- operator sections are the same partial application
(+3)  :: Num a => a -> a
(*2)  :: Num a => a -> a