Haskell Curry

Haskell Curry

Logician and mathematician · 1900–1982 · United States

Combinatory logic asks how much can be expressed through application and a small collection of operators, without variable-binding notation. Curry developed this subject and investigated the relationship between types and deduction. The resulting ideas become clearer through explicit reductions than through the slogan that every program is a proof.

Historical bearings

Haskell Brooks Curry was born on 12 September 1900 and died on 1 September 1982. He graduated from Harvard in 1920 and received a master's degree in physics in 1924. His doctoral examination took place at Göttingen in 1929, with Hilbert as formal supervisor and Bernays providing close support. The dissertation appeared in 1930. It was not a Harvard doctorate awarded in 1930. MacTutor biography

Curry encountered Schönfinkel's earlier published work while at Princeton before going to Göttingen. He subsequently developed combinatory logic over decades, including books with Robert Feys and later J. Roger Hindley and Jonathan Seldin. Acknowledging predecessors does not diminish the scale of this development. Nor does the name “currying” establish that Curry first invented every form of argument transformation.

Application and reduction

Write application left-associatively: f x y means (f x) y. In untyped combinatory logic, basic reduction rules include

K x y   → x
S f g x → f x (g x)
I x     → x.

These are formal rewrite rules. The displayed letters are schematic metavariables standing for expressions, not variable-binding operators inside a closed combinatory term. I can be represented as S K K because

S K K x → K x (K x) → x.

Eliminating binding helps avoid capture errors when translating lambda expressions. It does not magically remove all complexity: translated expressions can grow, reduction order matters operationally, and untyped terms need not terminate. Confluence means that two reduction paths can be joined; it does not promise that every path reaches a normal form. Combinatory logic

Worked mechanism: construct composition from S and K

Define the composition combinator B by the behavior B f g x → f(g x). The expression S (K S) K realizes it. Trace every step:

S (K S) K f g x
→ (K S f) (K f) g x
→ S (K f) g x
→ (K f x) (g x)
→ f (g x).

The parentheses are essential. In the first step, the S rule distributes f to its two operands. K S f discards f and yields S. Later K f x discards x and yields f. The remaining application is exactly composition.

For an original numerical illustration, let f add 3 and g multiply by 2. Then B f g 5 = f(10)=13. Reversing f and g gives g(8)=16, so composition order is observable. These arithmetic functions are a semantic illustration of the reduction; the displayed combinator trace itself contains no built-in integer representation.

A suitable simple type for B is

(Btype → Ctype) → (Atype → Btype) → Atype → Ctype.

Here Btype names a type, distinct from the combinator B. The type tells us that g consumes an Atype value and produces what f needs. This is a check on composition's interface, not a guarantee that an arbitrary real program returns within a time limit.

Currying is a transformation, not every multiargument call

Given a function on a pair, h : (A×B)→C, currying produces curry(h) : A→(B→C) with curry(h)(a)(b)=h(a,b). Conversely, uncurrying turns a nested function into one consuming a pair. For pure total functions over ordinary sets, these transformations undo each other extensionally.

Partial application is then possible: supplying a to the curried function yields a function awaiting b. But a language call h(a,b) need not use a curried representation. Evaluation order, effects, exceptions, and nontermination can also make seemingly harmless reorganizations operationally significant. The Haskell report describes a particular non-strict language, not every language's calling convention. Haskell expressions

A proof-shaped term

In an appropriate typed calculus, implication corresponds to function type. The proposition (A→B)→((B→C)→(A→C)) has the term

lambda f. lambda g. lambda x. g(f(x))

This is mathematical lambda notation. The proof assumes f:A→B, g:B→C, and x:A. Applying f gives a B; applying g gives a C. Discharging assumptions yields the stated implication chain. Propositions as Types

The correspondence requires a specified logic and term calculus. Ordinary Haskell admits nonterminating definitions at any type. A definition such as loop = loop does not manufacture a constructive witness for every proposition merely because a typechecker accepts an assigned type. Proof systems enforce conditions appropriate to their foundations. Errors and nontermination in Haskell

Exercises

1. Reduce S K K z with explicit grouping. Then reduce K a (S K K b) using an outermost strategy. Explain what the result shows about arguments that are discarded.
2. Let h(a,b)=3a-b. Write its curried form, specialize the first argument to 4, and evaluate at 7. Explain why partial application differs from evaluating h with both arguments.
3. Construct a typed term for (A×B)→(B×A) using pair projections. Explain the proof it represents. Then explain why replacing the body with a diverging computation in a general-purpose language would not prove the same constructive assertion.

Compare your reasoning with the worked solutions

1. ((S K) K) z → (K z)(K z) → z. For the second expression, (K a)(S K K b) → a without reducing its second argument. The K rule discards that argument. This gives a terminating outermost path even when a discarded expression would be costly or nonterminating. It does not show that all evaluation strategies have identical termination behavior.
2. The curried form is lambda a. lambda b. 3a-b. At a=4 it returns lambda b. 12-b; at b=7 that returns 5. The first stage constructs a function representing a pending calculation, while the second supplies the remaining input and produces a number. A language can support this transformation without representing all its multiargument functions this way internally.
3. A term is lambda p. (second(p), first(p)). If p has type A×B, its second projection has type B and its first has type A; their ordered pair has type B×A. The logical proof extracts both conjuncts and rebuilds them in the opposite order. A diverging computation returns neither component. It can inhabit a general-purpose type system with bottom while failing to provide the normalizing proof term required by the constructive interpretation.

Reading the evidence

The reductions and exercises are original teaching examples. The scholarly sources distinguish the history of combinators from later type-theoretic developments. Neither an eponym nor a superficial similarity establishes a direct genealogy for every functional language or every static type system.