Curry-Howard Correspondence

There is an idea so strange that most programmers who encounter it feel like the floor has shifted under them: every type is a proposition, every program is a proof, and your compiler is a theorem checker. This is the Curry-Howard correspondence, and once you see it, you can't unsee it.

The Core Insight

The correspondence works like this. A type like a -> a doesn't just describe "a function from a to a" — it's also the logical proposition "if a is true, then a is true." And the identity function \x -> x isn't just code — it's a proof of that proposition. The type checker, when it accepts your program, has verified the proof.¹

This sounds like a metaphor, but it isn't. It's an isomorphism — a structure-preserving map that works in both directions. Logical connectives map to type constructors: "and" becomes a pair type (a, b), "or" becomes a sum type Either a b, "implies" becomes the function arrow a -> b. False propositions correspond to uninhabited types (no values, no proofs). The principle of explosion — that from a false assumption you can prove anything — corresponds to the function absurd :: Void -> a, which is perfectly well-typed because you can never actually call it.²

Function composition (.) :: (b -> c) -> (a -> b) -> (a -> c) is the logical law of syllogism: if b implies c, and a implies b, then a implies c. Haskell's curry :: ((a, b) -> c) -> a -> b -> c literally is currying in the logical sense — it proves that a joint hypothesis can be decomposed into sequential assumptions. The pun in the name is not a coincidence; Haskell Curry is half the namesake of Curry-Howard.

Where It Breaks Down (and Where It Gets Interesting)

Haskell's type system doesn't correspond to a consistent logic. The value undefined :: a inhabits every type, which is logically equivalent to proving every proposition — including false ones. Unrestricted recursion is the culprit: let x = x in x has type a, and it's the logical equivalent of circular reasoning. You can prove anything if you're allowed to assume your conclusion.¹

This is why languages designed to be proof assistants — like Agda, Coq, and Lean — forbid general recursion. They require all functions to demonstrably terminate. In Dhall, a configuration language designed with Curry-Howard in mind, you literally cannot write an infinite loop. The tradeoff is real: you lose Turing completeness, but you gain a type checker that is also a sound proof checker.

The correspondence also reveals something subtle about classical versus intuitionistic logic. Most type systems correspond to intuitionistic logic, which does not assume the law of excluded middle — the principle that every proposition is either true or false. In type terms, you can't write a function forall a. Either a (a -> Void) — one that, for any type, either produces a value of that type or proves it's uninhabited. You'd need to be able to decide the inhabitation question for all types, which is undecidable in general.¹

This isn't a limitation — it's a feature. Intuitionistic logic is the logic of computation: it says a proposition is true only when you can construct a witness. Classical logic lets you prove existence by contradiction ("assume it doesn't exist, derive absurdity, therefore it exists") without ever producing the thing. Intuitionistic logic demands you actually build it. The constructive flavor of intuitionistic proofs is precisely what makes them programs.

Proof Assistants and the Formalization of Mathematics

The Curry-Howard correspondence isn't just a theoretical curiosity — it's the foundation of a revolution in how mathematics is done. Proof assistants like Lean, Coq, and Agda use dependent type theories where the correspondence runs deep enough to express real mathematical theorems as types and mechanically verify their proofs.

Lean's mathlib project is the most ambitious example. A community of mathematicians is systematically encoding mathematical knowledge into a single coherent library — definitions, theorems, and machine-checked proofs all the way down to the axioms. As of 2020, mathlib contained over 18,000 definitions and 38,000 theorems, covering most of an undergraduate curriculum. Mathematicians describe the experience as addictive, like a video game with constant positive reinforcement.³

The Liquid Tensor Experiment brought this into the realm of cutting-edge research. Peter Scholze, a Fields Medalist, challenged the Lean community to formalize a key theorem from his work on condensed mathematics — a proof he himself wasn't fully confident was correct. Within six months, the critical part of the argument had been verified. Scholze's reaction was telling: "I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research."⁴

What's striking is how the formalization proceeded. Rather than first digesting the proof into small lemmas and then formalizing, the team typed proofs directly into Lean, letting the proof assistant guide them step by step. Lean's clear presentation of proof goals at each step served as a navigation aid through what Scholze described as a proof "where the way leads through a large detour, to attack the mountain from the other side, where it is dark and slippery." The de Bruijn factor — the ratio of formal proof length to informal proof — came out around 20, far lower than expected.⁴

The formalization even produced mathematical insights. Johan Commelin discovered that an abstract construction in the proof (a Breen-Deligne resolution, whose existence depended on stable homotopy theory) could be replaced by a completely explicit object satisfying the same axioms — making the entire proof more elementary. The assistant didn't just check the proof; it helped improve it.

Beyond Simple Types

The most interesting developments in type theory push the correspondence further. Dependent types allow types to depend on values — the type of "a list of exactly n elements" or "a proof that n is prime." This moves us from propositional logic into predicate logic, enormously expanding what can be expressed.⁵

LiquidHaskell takes a different approach: refinement types annotate existing Haskell types with logical predicates that are checked by an SMT solver. You can express things like "this function takes a natural number and returns a natural number" or "fibonacci is monotonically increasing" and have the machine verify it. The proofs are ordinary Haskell functions.⁶

Substructural type systems open yet another dimension. Rust's ownership model corresponds not to classical or intuitionistic logic but to affine logic, where every resource can be used at most once. Linear logic, where every resource must be used exactly once, yields linear types — and maps naturally onto stack machines, where Forth's dup and drop are the explicit contraction and weakening operators of the logic. For every logic system, you get a type system for free — and there are more logic systems in the literature than type systems that have been implemented. As the Curry-Howard correspondence suggests, there are many powerful type systems waiting to be built.¹

Typeclasses as Type-Level Functions

One of the most practical applications of Curry-Howard in everyday Haskell is typeclass metaprogramming — using typeclasses as functions from types to terms. The simplest version: a typeclass with a method that takes no value-level argument, just a type parameter. The instance resolution mechanism then becomes a type-level interpreter, pattern-matching on types and producing term-level code. You can define Peano naturals as uninhabited types (Z, S Z, S (S Z), ...) and write a typeclass that reifies them to runtime values, even though no value of these types can ever exist.⁷

This isn't a trick — it's Curry-Howard working in reverse. Instead of interpreting programs as proofs, you're using the proof-search mechanism (instance resolution) to generate programs from type-level specifications. The Servant web framework uses this technique pervasively: you describe your API as a type, and the framework generates both server handlers and client functions from it. GHC's generics system uses it to derive serialization, traversal, and comparison code from the structure of your data types.

The technique works because Haskell's typeclass resolution is essentially a Prolog-style logic program operating on types. Each instance declaration is a logic rule; the constraint solver does backward chaining to find a derivation. This is another face of the Curry-Howard correspondence: the type checker isn't just verifying proofs, it's searching for them, and the proofs it finds are the programs you want.

The deep lesson of Curry-Howard is that computation and reasoning are not just analogous — they are, in a precise mathematical sense, the same thing seen from two angles. Your compiler is doing philosophy, whether you asked it to or not.