Slide 12.5: Syntax of the lambda calculus (cont.)
Slide 12.7: Curried functions (cont.)
Home

Curried Functions

Lambda calculus as described above seems to permit functions of a single variable only. However, many useful functions, such as binary arithmetic operations, require more than one parameter; for example, sum(a,b) = a+b matches the syntactic specification sum: N×N→N, where N denotes the natural numbers. Lambda calculus admits two solutions to this problem:
  1. Allow ordered pairs as lambda expressions, say using the notation <x,y>, and define the addition function on pairs: 
         sum <a, b> = a + b
  2. Another method is Currying, which is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument.
The notion of Currying allows for functions of several variables to be interpreted simply as functions of a single variable returning functions of the remaining variables. Use the curried version of the function with the property that arguments are supplied one at a time: 
     add: N → N → N
   ≡ add: N → ( N → N )     (→ associates to the right)
where add a b = a + b. An application of add has the form add a b, and is equivalent to (add a) b, since function application associates to the left. In other words, applying add to one argument yields a new function which is then applied to the second argument. Now (add a): N→N is a function with the property that ((add a) b) = a + b. Using add, we can define inc: 
     inc = add 1