Slide 12.6: Curried functions
Slide 12.8: Lambda reduction
Home

Curried Functions (Cont.)

The operations of currying and uncurrying a function can be expressed in the lambda calculus as 
     define   Curry = λf . λx . λy . f <x,y>
     define Uncurry = λf . λp . f (head p) (tail p)
provided the pairing operation <x,y> = (cons x y) and the functions (head p) and (tail p) are available. Therefore the two versions of the addition operation are related as follows: 
     Curry sum = add   and   Uncurry add = sum
One advantage of currying is that it permits the “partial application” of a function. Consider an example using Twice that takes advantage of the currying of functions: 
    define Twice = λf . λx . f (f x)
If D is any domain, the syntax (or signature) for Twice can be described as 
    Twice: (D → D) → D → D
Given the square function, sqr: N→N where N stands for the natural numbers, it follows that 
    (Twice sqr): N → N
is itself a function. This new function can be named 
    define FourthPower = Twice sqr
Observe that FourthPower is defined without any reference to its argument. Defining new functions in this way embodies the spirit of functional programming. Much of the power of a functional programming language lies in its ability to define and apply higher-order functions