Haskell Curry

1900 – 1982 · Millis, Massachusetts · Penn State & Amsterdam · combinatory logic · the λ in Haskell is named for him

[[alonzo-church]]'s λ-calculus computes with functions and bound variables — and variables, it turns out, are a nuisance: they get captured, renamed, tangled. Curry asked a startling question: can you compute with no variables at all? His answer is combinatory logic. Take three fixed operators — I (do nothing), K (keep the first, throw the second away), and S (share an argument between two functions) — and that's the whole machine. No x, no λ, just these combinators copying, deleting, and rearranging whatever you feed them. It is exactly as powerful as the λ-calculus and the Turing machine. And his name marks logic's deepest bridge — the Curry–Howard correspondence: a proof is a program, a proposition is a type.

✓ STRONG

Foundational, and elegant. Combinatory logic is a complete, variable-free model of computation, provably equivalent to the λ-calculus; and the Curry–Howard correspondence (proofs = programs) is one of the deepest unifications in logic and computer science.

◐ SHARED CREDIT

Not solo. The combinators came first from Moses Schönfinkel (1924); Curry rediscovered and built the theory. And "Curry–Howard" is named for Curry's observation and William Howard's later formalisation — a bridge with two builders.

◔ A PARADOX, TOO

Curry's paradox. His name also attaches to a self-referential paradox ("if this sentence is true, then everything is") that threatens naïve logics — a reminder that combinatory systems, untyped, can express dangerous self-reference.

I · Compute with no variables — the combinator machine

Three rewrite rules, applied left-to-right, are the entire calculus. I x → x. K x y → x (keep x, discard y). S x y z → x z (y z) (give z to both x and y, then apply). Pick an expression and reduce it step by step. Watch the famous identity emerge: S K K, applied to anything, hands it straight back — the combinators build the do-nothing operator out of "keep" and "share," with not a variable in sight.

I x → xK x y → xS x y z → x z (y z)

Every step just rearranges symbols by a fixed rule — no thinking, no variables, no scope. Yet from S, K, I alone you can build every computable function (numbers, booleans, recursion, the lot). ⚑ This is [[alonzo-church]]'s λ-calculus stripped to its bones: it proves that binding variables is a convenience, not a necessity — computation is, at bottom, just substitution of fixed patterns. Combinatory logic runs inside the implementation of functional languages, and S/K/I are how a compiler can eliminate variables entirely.

"The combinators … enable us to dispense with bound variables altogether." — Haskell Curry

II · Proofs are programs — Curry–Howard

PROPOSITIONS = TYPES

The proposition "A implies B" corresponds exactly to the type of a function from A to B. To have a proof of A→B is to have a program that turns evidence of A into evidence of B.

PROOFS = PROGRAMS

A proof is a typed program; checking the proof is type-checking; simplifying the proof (cut-elimination) is running the program. Logic and computation are two views of one thing.

Curry noticed something uncanny: the rules for combinators and the rules for logical implication have the same shape — the type of K is exactly the logical axiom "A → (B → A)," the type of S is exactly "(A→(B→C)) → ((A→B)→(A→C))." That coincidence is no coincidence: it is the Curry–Howard correspondence, completed by William Howard, and it says that logic and programming are the same activity in different clothing. It is why [[gerhard-gentzen]]'s natural deduction is the design of a type system, why [[bertrand-russell]]'s types reappear in every compiler, and why the proof assistants that verify aircraft software are, literally, programming languages whose programs are proofs. Curry found the seam where the two halves of this lineage — the logic and the computation — turn out to be one cloth. ⚑ The deepest bridge in the field, and his name is on it.

III · The variable-killer

Gate kept on. The results are real and deep: combinatory logic is a complete, rigorous, variable-free model of computation equivalent to the λ-calculus, and the Curry–Howard correspondence is one of the most profound unifications in all of logic and computer science. The honest qualifications are about credit. The combinators themselves were first introduced by Moses Schönfinkel in 1924 (and anticipated by John von Neumann); Curry independently rediscovered them around 1927 and, crucially, spent his career building the systematic theory — combinatory logic as a foundation — so the field is genuinely his even if the spark was Schönfinkel's. The famous correspondence is named "Curry–Howard" for a reason: Curry observed the parallel between combinator types and logical axioms in the 1930s–50s, and William Alvin Howard extended it to full natural deduction in 1969 — two builders, one bridge. His name also marks Curry's paradox, a self-referential trap that shows why untyped combinatory/λ systems must be handled with care. The man: a quiet, careful American logician who worked at Penn State and Amsterdam, helped run one of the first electronic computers (the ENIAC era), and gave functional programming its bones — the language Haskell is named after him. ⚑ He proved you can throw away the variables and still compute everything; and he found the place where proving and programming are the same. [[alonzo-church]] ← · next → Emil Post."