I’ve been making the case that types are practical tools, both for humans and for agents. They help us build tighter feedback loops and give agents faster, more precise insight into the programs they’re writing. But types aren’t just a feature of programming languages; they’re an entire mathematical system in their own right. And that system turns out to be the same system as logic.
Types in programming languages
Most of the time, we think about types as annotations that tell the typechecker what we expect a particular address in memory to hold. This allows the typechecker to watch for a common class of errors—“you said this was a 64-bit int and now you’re treating it like a 32-bit float.” Even better, it can help you avoid Tony Hoare’s billion-dollar mistake—“you said this thing could be null and now you’re treating it like it will always be there.”
Types are also messages to the compiler about what it can and can’t do with a particular piece of memory, which it can use to make optimizations. But because types are, in a way, just markup layered on top of raw bytes, some programming languages let you do horrible things to them.
int not_a_pointer = 42;
int sorry = *((int*)not_a_pointer);Many modern languages try to rein that in, but even Rust has an unsafe keyword to give programmers an escape hatch.
Types in type theory
In type theory, a type is defined by two things: how you construct its values, and how you use them. These are called introduction rules and elimination rules, and they’re all that matters—there’s no memory, no bytes, no machine.
Take pairs as an example. A programmer thinks: “(int, string) is two values packed together in memory.” A type theorist says: “If you have an A and a B, you can introduce a pair (A, B). If you have a pair (A, B), you can eliminate it by projecting out the first element or the second.”
That’s it. That’s the entire definition. The type is its rules.
This might seem like an academic distinction, but it has a practical consequence: if two types have the same introduction and elimination rules, they’re the same type—regardless of how they’re represented in memory. Structure is everything. Representation is nothing. (This idea gets taken even further by something called the univalence axiom—we’ll get to it later in the series.)
And here’s where it gets strange. Introduction and elimination rules for types turn out to follow exactly the same patterns as the rules of logic. Constructing a pair looks like proving “A and B.” Choosing between two types looks like proving “A or B.” A function from A to B looks like proving “if A, then B.” This isn’t a metaphor. It’s a formal correspondence, and this series will build toward it.
Why bother?
I’m assuming you’re already a programmer comfortable with types in code. Why bother with the theory?
My argument is similar to my argument for abstract math: as agents write more of our code, we become increasingly alienated from it. If all we have is the fuzzy human language of prose-heavy prompts, it’s hard to even see all of the pieces of an agent-written program, let alone understand how they fit together and, crucially, how they might break (in production, at 2am). The ability to conceptualize the problem you’re solving, define it in rigorous terms, and present it to the agent will be the defining skill of this era.
This isn’t just my pet theory. The UK’s Safeguarded AI project (£59 million, 60 researchers, heavy on category theorists) is building exactly this: software that lets you formally specify what you want, have an AI design it, and then verify that what the AI built actually meets your spec. The specification language isn’t English. It’s math.
Abstract math is one definition language. Type theory is another. The two have significant overlap. This series explores that space, and is intentionally paced to fit together with the abstract math series. When concepts overlap, each will look at that concept through its own lens.
Expect new posts every Friday.