Currying

Currying turns a function of several arguments into a chain of functions of one argument each: $f : A \times B \to C$ becomes $curry f : A \to (B \to C)$ . The two forms are in one-to-one correspondence, which in mathematics is the exponential law $C^{A \times B} ≅ (C^{B})^{A}$ . In OCaml and Haskell every function is curried, so partial application, supplying only some of a function's arguments to get a function of the rest, needs no special syntax.

§ 01

Overview

A function of two arguments can be seen as a function that takes the first argument and returns a function waiting for the second. That is how OCaml treats every multi-argument function: int -> int -> int means int -> (int -> int), because the arrow associates to the right, and add 1 2 means (add 1) 2, because application associates to the left. The compiler's inferred types show it:

Curried and uncurried functions, and the conversions between them.

let curry f a b = f (a, b)
let uncurry f (a, b) = f a b
 
let add a b = a + b
let add_pair (a, b) = a + b
let increment = add 1
let add3 a b c = a + b + c
let add3_partial = add3 1 2

What ocamlc -i infers.

val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
val add : int -> int -> int
val add_pair : int * int -> int
val increment : int -> int
val add3 : int -> int -> int -> int
val add3_partial : int -> int

add 1 is a complete value of type int -> int, and add3 1 2 of type int -> int. The tupled add_pair has to be given both components at once.

§ 02

Definition

curry : (A \times B \to C) \to (A \to B \to C) curry f = λa . λb . f (a, b)

uncurry : (A \to B \to C) \to (A \times B \to C) uncurry g = λ (a, b) . g a b

The two are inverses, $uncurry \circ curry = id$ and $curry \circ uncurry = id$ , so they give a bijection between the two function spaces. The same construction repeats for more arguments: a function of $n$ arguments becomes $n$ nested functions of one argument.

Partial application

Partial application is supplying fewer arguments than a function takes and getting a function of the remaining ones. It is related to currying but not the same thing: currying changes the type of a function, and partial application uses a curried function. Languages without curried functions provide it separately, for example Python's functools.partial and C++'s std::bind_front.

Partial application with positional, labelled and optional arguments.

let add a b = a + b
let increment = add 1
 
(* Partial application makes small functions out of general ones. *)
let scaled = List.map (( * ) 10) [ 1; 2; 3 ]
let evens = List.filter (fun n -> n mod 2 = 0)
 
(* Labelled arguments can be supplied in any order, and partially. *)
let rectangle ~width ~height = width * height
let tall = rectangle ~height:10                  (* still waiting for ~width *)
 
(* An optional argument is erased once a positional argument after it is given. *)
let greet ?(greeting = "Hello") name = greeting ^ ", " ^ name

Running it.

increment 41                 ->  42
List.map (( * ) 10) [1;2;3]  ->  [10; 20; 30]
evens [1; 2; 3; 4]           ->  [2; 4]
tall ~width:3                ->  30
greet "Ada", greet ~greeting:"Hi" "Ada"  ->  Hello, Ada | Hi, Ada

OCaml's labelled arguments can be supplied in any order, so a function can be partially applied to any subset of them: rectangle ~height:10 is a function waiting for ~width. An optional argument is filled with its default once a positional argument that follows it is supplied, which is why optional arguments are written before at least one positional one^[8].

§ 03

Mathematics

The exponential law

Write $C^{A}$ for the set of functions from $A$ to $C$ . Currying is the bijection

C^{A \times B} ≅ (C^{B})^{A}

which for finite sets is the law of exponents: $∣ C ∣^{∣ A ∣ \cdot ∣ B ∣} = (∣ C ∣^{∣ B ∣})^{∣ A ∣}$ . With booleans there are $2^{2 \cdot 2} = 16$ functions of each kind, and currying pairs them up exactly:

Every function bool * bool -> bool, curried, and checked against the original.

(* Every function bool * bool -> bool, as its table of four outputs. *)
let inputs = [ (false, false); (false, true); (true, false); (true, true) ]
let all_uncurried =
  List.init 16 (fun bits -> fun (a, b) ->
      let i = (if a then 2 else 0) + if b then 1 else 0 in
      bits land (1 lsl i) <> 0)
 
let curry f a b = f (a, b)
let uncurry f (a, b) = f a b
 
(* Two functions bool -> bool -> bool are equal if they agree everywhere. *)
let table_c g = List.map (fun (a, b) -> g a b) inputs
let table_u f = List.map f inputs

Running it.

functions bool * bool -> bool          :  16
distinct curried images                :  16
uncurry (curry f) = f for all of them  :  true

Cartesian closed categories

In category theory, a category with finite products has exponentials when for every pair of objects $B, C$ there is an object $C^{B}$ with an evaluation arrow $ev : C^{B} \times B \to C$ , such that every $f : A \times B \to C$ factors through it uniquely:

f = ev \circ (Λ f \times id_{B}) Λ f : A \to C^{B}

$Λ f$ is the curried form of $f$ , and the uniqueness says the correspondence is bijective. Equivalently, there is an isomorphism natural in $A$ and $C$ , which makes $- \times B$ left adjoint to $(-)^{B}$ :

Hom (A \times B, C) ≅ Hom (A, C^{B})

A category with finite products and all exponentials is cartesian closed. Types and functions form one, and the simply typed λ-calculus is its internal language: typed λ-terms and arrows of cartesian closed categories correspond^[6]^[5].

Logic

Under the Curry–Howard correspondence, where types are propositions and programs are proofs, currying is the logical equivalence called exportation:

(A \land B \Rightarrow C) ⟺ (A \Rightarrow (B \Rightarrow C))

and curry and uncurry, read as proofs, are the two directions.

§ 04

In programming languages

In the λ-calculus every function takes one argument, and $λ x y . e$ is shorthand for $λ x . λ y . e$ . ML, OCaml and Haskell inherit this: functions are curried by default, and a tuple argument is the exception, used when the arguments belong together.

Curried functions do not make calls slower. Compilers record each function's arity, a call that supplies every argument goes directly to the function's code, and only a partial application allocates a closure to hold the arguments given so far. Marlow and Peyton Jones compared the two ways of implementing this, push/enter and eval/apply^[7].

Elsewhere currying is by hand. In JavaScript a curried function is a chain of arrow functions, a => b => a + b. Scala allows several parameter lists, def add(a: Int)(b: Int), each of which can be supplied separately.

§ 05

History

Frege used the reduction of functions of several arguments to functions of one in 1893^[1], and Schönfinkel made it systematic in 1924 in his work on combinatory logic^[2]. Curry used it throughout combinatory logic^[3], and the name currying is usually credited to Strachey, who used it in lecture notes in 1967^[4]. Schönfinkelisation has been proposed as the more accurate name.