Currying

What Is Currying?

In lambda calculus, every function takes exactly one argument. To handle multiple arguments, we nest abstractions:

λx.λy.M

This is a function that takes an argument for x, and returns a new function that takes an argument for y. The arguments are consumed one at a time, not as a pair.

This technique is called currying (after logician Haskell Curry).

Two-Argument Function

When you see λx.λy.M, read it as: "a function that takes x, then takes y, and produces M."

The outer λx binds the first argument. The inner λy binds the second. The body M can use both x and y.

Examples:

• λx.λy.x -- takes two arguments, returns the first
• λx.λy.y -- takes two arguments, returns the second
• λx.λy.x y -- takes two arguments, applies the first to the second

First Argument

When a curried function receives its first argument, beta reduction fills the outer parameter and leaves the inner abstraction intact.

(λx.λy.x) a →β λy.a

The x in the body is replaced by a. The inner λy remains -- the result is a new function that still expects one more argument.

Second Argument

After the first argument has been applied, the result is a simpler function. Applying the second argument completes the computation.

(λy.a) b →β a

The body is a, which contains no y. The substitution a[y := b] leaves a unchanged -- y does not appear free in a, so there is nothing to replace. The second argument b is discarded.

Full Application

Applying a curried function to all its arguments requires multiple beta reductions, one per argument. Application is left-associative, so (λx.λy.x) a b means ((λx.λy.x) a) b.

• Step 1: ((λx.λy.x) a) b →β (λy.a) b
• Step 2: (λy.a) b →β a

The final result is a -- the first of the two arguments.

Why Nested Lambdas?

Lambda calculus could have been designed with multi-parameter abstractions like λ(x, y).M. But it was not. Instead, every abstraction binds exactly one parameter, and multiple arguments are handled by nesting: λx.λy.M.

This is not a limitation. Nesting gives us everything multi-parameter syntax would, without adding any new grammar rules. The calculus stays minimal: three term forms, one computation rule.

The tradeoff is simple: one extra reduction step per additional argument, in exchange for a simpler formal system.

Three Arguments

The nesting pattern extends naturally. Three parameters means three nested abstractions:

λx.λy.λz.M

This takes x first, then y, then z. Each application peels off one layer. After all three arguments are supplied, the body M (with all substitutions applied) is the result.

There is no limit to how deep the nesting can go. Four arguments, five, a hundred -- each is just one more layer of λ.

Currying Definition

Currying is the technique of expressing a function that takes multiple arguments as a chain of functions that each take one argument.

A function f(x, y) = M becomes λx.λy.M -- a function that takes x and returns a function that takes y.

The term honors logician Haskell Curry, though the idea was used earlier by Moses Schönfinkel and Gottlob Frege.

In lambda calculus, currying is not an optional technique -- it is the only way to handle multiple arguments, because every abstraction binds exactly one parameter.

One at a Time

Currying does more than simulate multi-argument functions. Because each argument is consumed separately, you can supply some arguments and stop. The result is a new, specialized function.

(λx.λy.x y) f →β λy.f y

You gave one argument (f) and got back a function that applies f to whatever it receives next. This intermediate result is useful on its own -- you can pass it around, apply it later, or give it to another function.

A multi-parameter system like λ(x, y).M would require all arguments at once. Currying gives you this flexibility for free.

Reading Curried Functions

Reading a curried function: count the nested λs to see how many arguments it expects, and read the body to see what it does with them.

λf.λx.λy.f x y

Three λs, so three arguments: f, x, y. The body f x y applies f to x, then applies the result to y.

Read it as: "takes a function f, a value x, and a value y, then applies f to x and y."

The outermost λ binds the first argument. The innermost λ binds the last argument. Arguments are consumed from outside in.