Hero image for "Haskell's Type System Encodes What You Know, Not Just What You Have"

Haskell's Type System Encodes What You Know, Not Just What You Have


Lesson 17: Why pure functional programming is a design philosophy, not a restriction


There's a moment in Simon Peyton Jones's recent interview on The Developing Dev where he explains functional programming by analogy to a spreadsheet. In a spreadsheet, he says, "you put in a cell the formula =A2 * A3 + 7. Well, then that's just the formula that is evaluated. It wouldn't make any sense to compute A1 from the old values of A2 and A3." No program counter. No mutation. Just values and their relationships.

Most programmers hear this and think: cute, but limited. The surprise — and the whole point — is that it isn't.


Purity Is a Constraint That Pays You Back

Peyton Jones is Haskell's co-creator, and his framing of functional programming cuts straight to the design decision that makes Haskell unusual: computation as values, not mutation. In his words, "functional programming is about programming with values instead of mutation." Where imperative code maintains a running total in a mutable cell — incrementing it, overwriting it, threading it through a sequence of steps — functional code describes what the answer is rather than how to arrive at it.

This sounds like a restriction. It is, deliberately. The discipline of purity — no hidden state, no side effects that escape the type signature — is what makes Haskell's type system so expressive. When a function can't secretly mutate global state, the type of that function tells you everything it can do. The type becomes a contract you can actually trust.

That's the design insight worth borrowing even if you never write a line of Haskell: types are most useful when they're complete. A type that says Int -> Int in a language with unrestricted side effects is a weak promise. The function might write to a database, throw an exception, or launch a network request. In Haskell, Int -> Int means exactly that and nothing else. Side effects are explicitly tracked in the type system — if a function does I/O, its type says so.


The Type System as Institutional Memory

Here's where this stops being academic. Mercury, a fintech that processed $248 billion in transaction volume in 2025, runs roughly two million lines of production Haskell. Most engineers who join the company have never written Haskell before. That last fact is the interesting one.

Ian Duncan, an engineer on Mercury's Stability team, wrote in March 2026 about why the architecture held up when Silicon Valley Bank collapsed in 2023 — an event that sent 8,700 new customers and roughly $2 billion in deposits through Mercury's systems in five days. His explanation wasn't about Haskell's elegance. It was about what the type system does for organizational knowledge: "things people knew walk out the door with them unless you have written them down somewhere. Ideally, you have written them down in a form that the compiler can read, because the compiler is much more disciplined than the average wiki page."

The specific example Duncan gives involves side effects that must happen transactionally — sending a notification, publishing an event. In most codebases, the rule "don't do this outside a transaction" lives in a README, or in the memory of whoever wrote the original code. In Haskell, you encode that constraint in the type. New engineers can't violate it accidentally. The compiler enforces what the senior engineer used to enforce by code review.

This is what purity actually buys at scale. It's not about mathematical elegance. It's about making implicit knowledge explicit in a form that doesn't degrade.


What Haskell Made Possible That Wasn't Possible Before

The POPL 2026 Haskell Interlude touched on something that connects Haskell's design to current research: the relationship between lazy linear types in Haskell and Rust's ownership model. Two languages that look nothing alike are converging on the same insight — that tracking how a value is used, not just what type it has, lets you enforce correctness properties that would otherwise require runtime checks or programmer discipline.

This is the thread that runs through Haskell's entire design history. The language was built as a research vehicle, a place to try ideas that were too risky for production languages. Purity, lazy evaluation, type classes, monads as a way to sequence effects without abandoning the pure model — each of these was an experiment in what you could express in a type system if you took the constraints seriously.

Peyton Jones is candid that Haskell is talked about more than it's used. He's even described the language's design goal as "avoiding success at all costs" — a joke with a real point behind it. A language optimized for research and correctness will make different tradeoffs than one optimized for hiring and ecosystem size.

But the ideas don't stay in Haskell. Type classes became traits in Rust. Monadic error handling became Result types in half a dozen modern languages. The effect-tracking that Haskell pioneered is showing up in research on Scala's capability system, in work on typestate via revocable capabilities published in the ACM proceedings.

The lesson isn't "use Haskell." The lesson is that purity is a design choice with consequences — and understanding those consequences makes you sharper about every type system you work in, including the ones that made different tradeoffs.