(This is part 23 in a series on type systems. You can find part 22 here .)

Shoutout to my man Haskell Curry for being so instrumental for computer science that he gets not one but three programming languages named after him (Haskell being the most famous), as well as a functional programming concept (currying)! His most famous contribution to computer science is probably the Curry-Howard isomorphism, which connects mathematical logic with types and computer programs. Really unexpected stuff.

Propositions as Types

The Curry-Howard isomorphism states that we can take any proposition in logic, like “If it rains, the ground gets wet”, and interpret it as a type in a programming language. Now “If it rains, the ground gets wet” is not such a good example, because (cue Carl Sagan voice) to model rain, one must first invent the universe; so let’s pick a very simple logical proposition instead:

$$A \land B → A$$

The ^ symbol in logic means “and”, and the arrow is implication, so this proposition states that if both A and B are true, then A is true, given any A and B. This is of course ultra trivial.

Curry-Howard says we can map this proposition to a distinct type:

proposition :: A * B → A

That is, the “and” operator ^ in logic corresponds to the product type * (as discussed last post; it’s the tuple type), and the implication → in logic corresponds to the function type → in programming languages.

“Proving” that this proposition is true is as easy (or hard) as finding a value, any value, of this type. For our example this should be pretty easy right — the type signature looks like the first function that gives you the first element of a tuple.

type Pair<A, B> = { fst: A; snd: B };
const proof = <A, B>({ fst }: Pair<A, B>): A => fst;

That code typechecks, so the proposition is true!

---

The other common logical operators map similarly:

Logic	Programming Type
A ∧ B (and)	A * B (product)
A ∨ B (or)	A + B (sum)
A → B (implies)	A → B (function)
⊤ (true)	1 (top type)
⊥ (false)	0 (bottom type)

To prove a false proposition like A → ⊥ (if A then false), we would need to find a value of type

const falseProof = <A>(a: A): never => ...

But there is no way to implement this function, because you can never produce a value of type never. Checkmate, proposition is false! ¹

---

The Curry-Howard isomorphism is really cool and to me anyway came completely out of the blue when I first heard of it, like it’s two separate areas that I didn’t expect to be connected, coming from a typescript background.

It’s also really a really nice trick for toddlers like me who know programming but not logic. Whenever I come across a logical proposition in the wild, I usually map it to types and then I’m like “aah, I understand what this is saying now” :D

Of course, then there are the grown-ups who know both maths and programming, and they are interested in Curry-Howard for a totally different reason: All mathematical proof-finding is just an application of logic at the end of the day, so a type checker for any sufficiently expressive type system is also something that can prove (or verify) mathematical theorems for you!

Proof assistants like Coq or Agda use this fact to help mathematicians formalize and check their proofs by letting them write proofs as programs in a particularly strong variant of the lambda calculus — the Calculus of Constructions.

(This is part 23 in a series on type systems. You can find part 24 here .)

---

^{[1] There is a one concrete type A for which you could implement this function, namely when A is itself never. That maps to the proposition ⊥ → ⊥, which is true. But the original proposition as stated is not true, as A is generic.}