Currying and Function Types
Consider a function that adds three numbers, written `add(x, y, z)`. In many languages this is a single opaque operation. It consumes three arguments at once and refuses to run with fewer. But what if you only have `x`? What if you want to wait for `y` and `z` later? What if you want to build a new function `add5`? Suppose it always adds `5` to its input, reusing `add` without writing new code. These questions expose a fork in the road. They reveal how a language models multi-argument functions. Most functional languages answer with currying: every function takes exactly one argument. Functions of several arguments are simulated by functions that return functions. Currying is not a syntactic trick. It is a decision about the type of functions. This decision is baked into the The Simply-Typed Lambda Calculus itself. There, the only function type former is the single-argument arrow `A → B`. Multi-argument functions arise as a derived notion, `A → (B → C)`. They are not primitive, unlike `(A, B) → C`. This choice has real consequences. It makes partial application free and uniform. It lets Recursion and Higher-Order Functions be expressed with no special-casing on arity. It also explains why languages like Haskell and ML let you write `map (add 5)`. No special syntax is needed for "leave some slots blank." The idea matters far beyond academic lambda calculus. Every time a functional programmer writes `foldr (+) 0`, they exploit currying. The same is true when they chain `.filter(pred).map(f)`. It also applies when configuring a logging function with a fixed prefix. Compiler writers rely on the curried view for a clean, uniform typing rule for application. They also use it to justify optimizations, like argument-count specialization in call sites. Understanding currying precisely is a foundation for later work. This includes the isomorphism it rests on, how it interacts with evaluation order, and where it costs performance. It helps with reading type signatures in ML-family languages. It also prepares readers for topics such as Parametric Polymorphism and Closures. Currying sets up both of these naturally. This article gives the precise definition of curried function types. It offers a step-by-step account of how currying and partial application work operationally. It presents a formal correctness argument, the curry–uncurry isomorphism. It includes a full worked trace of a curried function under evaluation. It covers common pitfalls, especially around performance and mutable state. Finally, it introduces the historical figures who gave the technique its logical foundations, chief among them Schönfinkel and Curry.
- Currying rewrites a function of n arguments as a chain of n single-argument functions, each returning the next.
- The function type `A → B → C` means `A → (B → C)`: arrows associate to the right.
- Partial application — supplying some but not all arguments — falls out for free once functions are curried.
- Currying and "uncurrying" (using tuples instead) are provably equivalent: there is a bijection between `A → B → C` and `(A × B) → C`.
- In call-by-value languages, currying can introduce real overhead (intermediate closures) unless the compiler specializes multi-argument calls.
- The technique underlies higher-order idioms in ML, Haskell, and functional-style code in mainstream languages, and prepares the ground for polymorphic and closure-based reasoning.
A function of several arguments is really a function of one argument that returns another function — and this single idea gives partial application, composability, and a uniform typing rule for free.
The idea
In the The Simply-Typed Lambda Calculus, the only function types are of the form `A → B`: given one argument of type `A`, produce a result of type `B`. There is no primitive notion of a "two-argument function." To model `add : Int × Int → Int`, we instead write ``` add : Int → (Int → Int) ``` read as: `add` takes an `Int` and returns a function from `Int` to `Int`. Applying `add` to `3` yields a new function `add 3 : Int → Int`, and applying that to `4` yields `7`. By convention the arrow `→` is right-associative, so `Int → Int → Int` is parsed as `Int → (Int → Int)`, and function application is left-associative, so `add 3 4` is parsed as `(add 3) 4`. These two conventions are exactly matched to each other, which is why curried notation reads naturally without extra parentheses.
Currying is the general transformation that turns a function expecting a tuple of arguments, `f : A × B → C`, into a function expecting them one at a time, `curry(f) : A → B → C`. The reverse transformation, uncurrying, turns a chain back into a function on tuples, `uncurry(g) : A × B → C` from `g : A → B → C`. These two operations are mutually inverse, which is the precise sense in which "multi-argument functions" and "chains of one-argument functions" are the same thing, differing only in packaging.
Partial application is the practical payoff: because `add` really is a one-argument function, applying it to just `3` is not a special operation requiring default values or variadic tricks — it is ordinary function application, and the result, `add 3`, is an ordinary first-class function that can be passed around, stored, or applied later. This is what makes expressions like `map (add 3) xs` type-check and run without any additional machinery: `add 3` has type `Int → Int`, exactly what `map` expects as its function argument.
How it works
Curried abstraction and application. In the lambda calculus, a two-argument function is written as nested lambdas: ``` add = λx : Int. λy : Int. x + y ``` Applying `add` to two arguments is applying it to one, getting back a function, and applying that to the second: ``` add 3 4 ≡ (add 3) 4 ≡ ((λx. λy. x + y) 3) 4 ⟶ (λy. 3 + y) 4 -- β-reduce the outer application ⟶ 3 + 4 -- β-reduce the inner application ⟶ 7 ``` Each `λ` binds exactly one variable; "multi-argument" functions are simply several nested `λ`s. The typing rule for application in The Simply-Typed Lambda Calculus needs no special case for arity: ``` Γ ⊢ f : A → B Γ ⊢ a : A ───────────────────────────── (T-APP) Γ ⊢ f a : B ``` Apply this rule twice — once to `add`, once to `add 3` — and the whole curried call type-checks using the same single rule, which is precisely the uniformity currying buys the type system.
Currying and uncurrying as maps between types. Define two higher-order operations, for any types `A, B, C`: ``` curry : (A × B → C) → (A → B → C) curry(f) = λx. λy. f(x, y) uncurry : (A → B → C) → (A × B → C) uncurry(g) = λ(x, y). g x y ``` These are total, computable, and — crucially — inverse to each other: ``` uncurry(curry(f))(x, y) = curry(f)(x)(y) = f(x, y) for all x, y curry(uncurry(g))(x)(y) = uncurry(g)(x, y) = g(x)(y) for all x, y ``` So `curry` and `uncurry` witness a bijection between the two function types. This is often summarized as the type isomorphism ``` A → B → C ≅ (A × B) → C ``` which generalizes to any number of arguments by induction: an n-argument function is isomorphic to a chain of n single-argument functions, in either direction, with `curry`/`uncurry` composed pointwise.
Partial application, operationally. Because `curry(f)` is built from nested lambdas, applying it to one argument simply performs one β-reduction and stops — it does not need to know how many arguments will eventually arrive. The partial result is a closure over the first argument (see Closures), ready to accept the rest: ``` step 1: add : Int → Int → Int step 2: add 3 : Int → Int -- a closure holding x = 3 step 3: (add 3) 4 : Int -- fully applied, reduces to 7 ``` The algorithm below makes this precise as an evaluator for curried applications, together with the `curry`/`uncurry` transformations as explicit rewrite procedures. ``` // Evaluating a chain of curried applications e1 e2 e3 ... en // under call-by-value small-step semantics. function EVAL_APP_CHAIN(f, args[1..n]): result = f for i = 1 to n: result = APPLY(result, args[i]) // one β-reduction step // APPLY(λx.body, v) = substitute v for x in body, then evaluate if result is not a function and i < n: error "too many arguments: cannot apply a non-function" return result // Transform an n-ary tupled function into a curried chain of closures. function CURRY(f, arity n): // f expects a tuple (a1, ..., an) return build(collected = []): function build(collected): if length(collected) == n: return f(collected) // fully applied: run the body else: return λ(x): // return a new 1-argument closure build(collected ++ [x]) return build([]) // Transform a curried chain g : A1 -> A2 -> ... -> An -> R // into a function taking one tuple of n arguments. function UNCURRY(g, arity n): return λ(a1, ..., an): result = g for i = 1 to n: result = APPLY(result, a_i) return result ``` Both `CURRY` and `UNCURRY` are purely structural: they never inspect the values being passed, only shuffle how arguments are grouped and delivered. This is why the transformation is type-preserving and reversible — it is bookkeeping about arity, not a change in what is computed.
Complexity & correctness
Time. Evaluating a fully curried n-ary application `f a1 a2 ... an` performs n separate applications (β-reductions), each of which does whatever work the underlying function body does at that stage plus O(1) overhead to build or enter a closure. So curried application costs ``` T(n) = O(n) extra closure-construction steps + T_body ``` compared to a single "native" n-ary call, which does the same body work with O(1) call overhead. The asymptotic class does not change — both are O(1) in n for fixed small arity, and both scale identically in the size of the arguments and the body — but the constant factor is real: currying allocates n − 1 intermediate closures that a direct multi-argument call would not need. Compilers for curried languages (the ML family, Haskell) routinely detect saturated applications (all arguments present at the call site) and compile them to a single direct call with no intermediate closures, recovering the performance of native multi-argument calls; the curried representation is then a typing and semantics device rather than a literal execution strategy.
Space. Each partial application `f a1 ... ak` (for `k < n`) that escapes its call site — i.e., is stored, returned, or passed onward — requires a heap-allocated closure holding the captured arguments `a1, ..., ak` plus a pointer to the remaining code. In the worst case (all `n − 1` partial applications are separately retained), this is O(n) additional space over a direct call, each closure of size O(k). If no partial application escapes (the common case of a fully saturated call), a compiler can prove the closures are dead immediately after use and elide them, giving O(1) extra space.
Correctness — the curry/uncurry isomorphism. The central correctness claim is that currying is sound and complete as a representation of multi-argument functions: nothing is gained or lost by moving between `A → B → C` and `(A × B) → C`. This is proved by exhibiting `curry` and `uncurry` as defined above and checking the two round-trip equations by direct calculation with the β-rule: ``` Claim 1: uncurry(curry(f)) = f (as functions on A × B) Proof: uncurry(curry(f))(x, y) = curry(f)(x)(y) by definition of uncurry = (λy. f(x, y))(y) by definition of curry, after applying to x = f(x, y) by β-reduction Since this holds for all (x, y) ∈ A × B, the two functions are extensionally equal. ∎ Claim 2: curry(uncurry(g)) = g (as functions A → B → C) Proof: curry(uncurry(g))(x)(y) = uncurry(g)(x, y) by definition of curry = g(x)(y) by definition of uncurry Equality holds pointwise for all x, y, hence the functions (and their partial applications curry(uncurry(g))(x) and g(x)) agree everywhere. ∎ ``` Together, Claims 1 and 2 establish that `curry` and `uncurry` form a bijection between the hom-sets `Hom(A × B, C)` and `Hom(A, B → C)` — this is precisely the statement, familiar from the Recursion and Higher-Order Functions treatment of function spaces, that function types satisfy an exponential law analogous to `(C^B)^A ≅ C^(A×B)` for sets, with `→` playing the role of exponentiation and `×` the role of product. This is not a coincidence: it is the type-theoretic shadow of currying in the category of sets (and, under the Curry–Howard correspondence, a proof-theoretic fact about implication and conjunction: `A ⇒ (B ⇒ C)` is logically equivalent to `(A ∧ B) ⇒ C`).
Well-typedness is preserved. If `f : A × B → C` is well-typed, then `curry(f) : A → (B → C)` is well-typed by two applications of the abstraction rule for `→`-introduction; conversely if `g : A → B → C` is well-typed then `uncurry(g) : (A × B) → C` is well-typed by pattern-matching the pair and applying `g` twice. So the transformation is type-safe in both directions — no ill-typed term can be produced from a well-typed one.
Worked example
Trace `mkAdder = λx. λy. λz. x + y + z` — a three-argument curried adder — applied step by step to `3`, `4`, `5`, under call-by-value evaluation, alongside its uncurried counterpart.
| Step | Expression | Action | Resulting value / type |
|---|---|---|---|
| 0 | `mkAdder` | — | `Int → Int → Int → Int` |
| 1 | `mkAdder 3` | β-reduce outermost λ, substitute `x := 3` | closure `λy. λz. 3 + y + z` : `Int → Int → Int` |
| 2 | `(mkAdder 3) 4` | β-reduce next λ, substitute `y := 4` | closure `λz. 3 + 4 + z` : `Int → Int` |
| 3 | `((mkAdder 3) 4) 5` | β-reduce last λ, substitute `z := 5` | expression `3 + 4 + 5` |
| 4 | `3 + 4 + 5` | evaluate primitive addition | `12 : Int` |
Now suppose we partially apply and reuse: ``` addTo7 = mkAdder 3 4 -- a stored closure : Int -> Int, captures x=3, y=4 addTo7 5 ⟶ 12 addTo7 100 ⟶ 107 ``` The closure `addTo7` is built exactly once (step 2 above) and reused for many final arguments — this is the concrete payoff of currying: `mkAdder 3 4` is an ordinary value of type `Int → Int`, storable in a variable, passed to `map`, or returned from another function, with no special "partial call" syntax required. Compare with the uncurried version, `mkAdder' : (Int × Int × Int) → Int`, `mkAdder'(x, y, z) = x + y + z`. To get the effect of `addTo7`, one must manually build a new closure: ``` addTo7' = λz. mkAdder'(3, 4, z) -- must write this by hand addTo7' 5 ⟶ 12 ``` Both computations reach `12`, confirming `uncurry(mkAdder)(3,4,5) = mkAdder(3)(4)(5)`, exactly as the isomorphism predicts — but the curried version got partial application "for free" from the general application rule, while the uncurried version needed an explicit `λ` wrapper for every partial-application site.
Common pitfalls & traps
| Pitfall | Why it happens | Fix |
|---|---|---|
| Assuming curried and uncurried calls always have identical performance | Curried chains can allocate an intermediate closure per argument unless the compiler saturates the call | Rely on saturation-aware compilation (ML/Haskell backends) or benchmark before assuming zero cost |
| Confusing "partial application" with "default arguments" | Both leave arguments unspecified, but partial application returns a genuine function value, not a call with fillers | Check the type: `add 3 : Int → Int` is a first-class function, not a pending call |
| Off-by-one in arrow associativity when reading types | `A → B → C` is easy to misparse as `(A → B) → C` instead of `A → (B → C)` | Remember `→` is right-associative; only the last type is the ultimate result |
| Assuming currying works the same in call-by-value and call-by-name languages | Evaluation order affects when side effects inside partial applications fire | Trace each β-reduction explicitly when arguments have side effects |
| Currying functions with mutable/aliased state and expecting independent partial applications | Closures capture references, not always fresh copies, so two "partial applications" may share mutable state unexpectedly | Ensure captured variables are immutable, or copy state explicitly before creating closures |
| Forgetting that uncurried tuple types are eager to allocate a tuple value | `(A × B) → C` needs a constructed pair before calling, which is itself an allocation | Weigh tuple-construction cost against closure-chain cost — neither is free |
Pioneers & history
The mathematical foundation for currying predates its name by decades and was independently discovered in the search for minimal foundations of logic and computation.
Origins · 1 minMoses Schönfinkel and how this was discovered
Schönfinkel introduced the technique of reducing multi-argument functions to chains of one-argument functions in a 1924 lecture that founded combinatory logic, aiming to eliminate bound variables from logic entirely by building all functions from a tiny set of combinators.
Curry developed and systematized the technique decades later, connecting it to the study of function types and to what became the Curry–Howard correspondence between proofs and programs; the transformation was later named "currying" in his honor, though he attributed the core idea to Schönfinkel.
Where this matters
Curried function types are the default calling convention in the ML family (Standard ML, OCaml, F#) and in Haskell, where every function definition `f x y z = ...` desugars to nested single-argument lambdas and every type signature `f : A -> B -> C -> D` is read with right-associative arrows. This is why idioms like `List.map (f 3)`, point-free composition `(.) g f`, and partially-applied operators (`(+ 1)` in Haskell) are completely ordinary rather than special syntax. Build tools and parser combinator libraries lean heavily on partial application to assemble complex parsers from small curried pieces. Even in languages that are not curried by default — Python, JavaScript, Scala — libraries and idioms (`functools.partial`, `.bind`, and Scala's multiple parameter lists) exist precisely to recover currying's ergonomics, because the ability to "fix some arguments now, supply the rest later" is broadly useful for configuration, dependency injection, and building reusable higher-order combinators. Compiler backends for curried languages implement arity/saturation analysis specifically so this convenience does not cost performance, a direct practical consequence of the complexity discussion above. The isomorphism `A → B → C ≅ (A × B) → C` is also the seed of deeper ideas: once functions are seen as first-class values with precise types, it becomes natural to ask how those types can be made generic — the question answered by Parametric Polymorphism — and to ask what exactly a partially-applied function "remembers" between calls, the question answered by Closures.
Ask the tutor: How does currying interact with type inference when a partially applied function is passed to a polymorphic higher-order function like `map`?
Is currying the same thing as partial application?
No — they are related but distinct. Currying is the representation choice: modeling an n-argument function as a chain of n one-argument functions, `A1 -> A2 -> ... -> An -> R`, instead of a single function on a tuple. Partial application is the operational payoff of that representation: because each step in the chain is an ordinary one-argument function, you can apply it to fewer than all its arguments and get back a genuine, reusable function value. You can have partial application without full currying (e.g., via library helpers like `functools.partial` in Python), but in a genuinely curried language, partial application requires no special machinery — it is just application, stopped early.
Does currying change what a function computes, or only how it is called?
Only how it is called and typed. The curry/uncurry isomorphism guarantees that `uncurry(curry(f))` equals `f` exactly, and `curry(uncurry(g))` equals `g` exactly, for every input. No computation is added, removed, or reordered inside the function body — currying is purely a restructuring of the argument-passing interface, proven correct by the two round-trip equations shown in the correctness section.
Why do ML and Haskell use curried functions by default instead of tuples?
Largely for uniformity and ergonomics. With curried functions, application needs only one typing rule (`T-APP`) regardless of arity, partial application is free, and higher-order functions like `map`, `filter`, and `fold` can be composed with partially-applied functions without any special syntax. Tupled (uncurried) functions require constructing a tuple value before every call and offer no built-in way to supply "some but not all" arguments — you would have to write an explicit wrapper lambda each time, exactly as shown in the worked example.
Is currying free at runtime, or does it cost something?
It is not free in general, but it is often free in practice due to compiler optimization. If a curried function is called with all its arguments present at the call site — a "saturated" call — most compilers for curried languages compile it into a single direct call with no intermediate closures, matching the cost of a native multi-argument call. If the call is not saturated (some arguments are supplied later, and the partial result is stored or passed onward), each pending argument corresponds to a real heap-allocated closure, adding constant-factor overhead and garbage-collection pressure.
How does currying relate to logic and the Curry-Howard correspondence?
Under the Curry–Howard correspondence, types correspond to logical propositions and programs correspond to proofs. The function type `A -> B` corresponds to implication `A => B`, and the product type `A x B` corresponds to conjunction `A ^ B`. The curry/uncurry isomorphism `A -> B -> C ≅ (A x B) -> C` is then exactly the familiar logical tautology `A => (B => C) ≡ (A ^ B) => C` — "if A implies that B implies C, that is the same as A and B together implying C." Currying is thus not just a programming convenience but the computational shadow of a basic fact about implication.
Can every multi-argument function be curried, or are there exceptions?
In a language with first-class functions and the standard function-type former `A -> B`, every fixed-arity function can be curried, because the transformation is purely structural (nested lambda-building) and does not depend on what the function computes. The main practical exception is variadic functions — functions accepting an unbounded, statically-unknown number of arguments — which do not fit the fixed-arity `A1 -> ... -> An -> R` shape directly and usually need a different mechanism, such as accepting a list or using variadic-specific language features.
What is the difference between `A -> B -> C` and `(A -> B) -> C`?
They are different types describing very different functions. `A -> B -> C` (by right-associativity) is a curried two-argument function: give it an `A`, get back a `B -> C`, then give that a `B` to get a `C`. `(A -> B) -> C` is a higher-order one-argument function: it takes an entire function of type `A -> B` as its single argument and produces a `C` — for example, applying a given function to a fixed input, or composing it with something else. Misreading the associativity of `->` is a classic source of confusion when first reading curried type signatures.