Currying

Turning a function of several arguments into a function of the first argument that returns a function of the rest: f : A * B -> C becomes curry f : A -> (B -> C). In OCaml and Haskell every function is curried, so applying it to fewer arguments than it takes, partial application, is ordinary.

The two are inverse, and together they are an isomorphism between function spaces:

For finite sets the cardinalities agree, $|C{|}^{|A||B|}=(|C{|}^{|B|}{)}^{|A|}$. In category theory this isomorphism, natural in $A$, is what it means to be cartesian closed: $\mathrm{Hom}(A\times B,C)\cong \mathrm{Hom}(A,C^B)$, so $-\times B$ is left adjoint to $(-{)}^B$.

let curry f a b = f (a, b)
let uncurry f (a, b) = f a b
 
(* Every OCaml function takes one argument: this is int -> (int -> int). *)
let add a b = a + b
let add_pair (a, b) = a + b
 
let increment = add 1                      (* partial application *)
let add' = curry add_pair                  (* same type as add *)
let add_pair' = uncurry add                (* same type as add_pair *)

increment 41                 ->  42
add' 2 3, add_pair' (2, 3)   ->  5, 5
List.map (add 10) [1; 2; 3]  ->  [11; 12; 13]

Partial application is what makes combinators like List.map (add 10) short. It does not make ordinary calls slow: the native compiler records each function's arity, a call that supplies all the arguments builds no intermediate closures, and only a partial application allocates one, to hold the arguments given so far.

The idea is Frege's and Schönfinkel's, who used it to reduce many-place functions to one-place ones in logic;^[1] the name comes from Haskell Curry, who used it throughout combinatory logic.^[2]

• ClosureA function value together with the environment it was defined in: the values of the free variables its body refers to. Closures are what make functions first-class in a lexically scoped language, and closure conversion is the compiler pass that turns them into ordinary data: a code pointer and a record of captured values.
• SKI combinatorsThree combinators, S x y z = x z (y z), K x y = x and I x = x, from which every closed lambda term can be built by application alone, with no variables. I is redundant, since S K K x = x. The translation from lambda terms is called bracket abstraction.
• Church encodingRepresenting data as functions in the pure lambda calculus: the numeral n applies its argument n times, true and false choose between two arguments, and a pair waits for a selector. Addition, multiplication and exponentiation are one line each; the predecessor needs a trick and takes time linear in n.
• Algebraic data typeA type built from sums (a value is one of several cases) and products (a value has several fields at once), possibly recursively. The name comes from counting: the number of values of a sum is the sum of the counts, and of a product the product, so types obey the laws of algebra.

1. [1]M. Schönfinkel, “Über die Bausteine der mathematischen Logik”, Mathematische Annalen 92 (1924).
2. [2]H. B. Curry, R. Feys, Combinatory Logic, Vol. I, North-Holland (1958).
3. [3]S. Mac Lane, Categories for the Working Mathematician, ch. IV, Springer (2nd ed., 1998).