I really like type theories, and I can go on and on about all the theoretical properties they have, but the real reason they’ve burned themselves into my brain is the analogies I use for them in my head.
The straightforward way to define a type theory gives rise to something that obeys constructive logic, a stricter proof system than classical logic. Classical logic is the familiar thing you’ve learned in school, with all of its attendent boolean-algebra-based rules. Constructive logic is stricter: to prove a disjunction (“or”), you have to know which branch of the disjunction is true. To prove an existential quantification, you need to give an example. Proof by contradiction is not valid1, because double negation doesn’t reduce to a positive statement.
This exacting discipline, to me, paints a breathtaking picture. Logic — the art of proving things — is a vast machine, a machine that transforms proofs into other proofs — and no proof is a hypothetical, all of them are physical objects, examples of the things we’d like to prove. Nothing is proved by idle speculation, you can’t just conclude that things “couldn’t be any other way”. You have to produce a physical avatar of the proof you claim. The false proposition, or the empty type, are not actually falsehood but more like oblivion, apocalypse, the destruction of all things — or rather the realization that nothing was ever real in the first place. Proofs of contradictions — avatars of this oblivion — are infinite voids, all-encompassing pits of nothingness that we’re trapped in right now if any of them exist. To say that a proposition is false is to claim that you could create a void if it was true — to claim that you could build a machine that can turn avatars of this supposedly false statement into voids. To disprove the statement is to actually build a hypothetical doomsday machine: a machine that can never be used, but if it could, that would destroy the world.
Recently I’ve been studying observational type theory1. It’s an alternate universe in which it’s possible to build the coveted machine called Extensionality.
In the standard universe of sublime machines, it’s not possible to look inside a machine that’s already been constructed. If you built one with your own two hands, then you know what’s inside it, and if you receive a machine from someone who knows how it works then you can ask them. But if you find a machine and can’t find its creator, there’s no way to probe its mechanisms. Even if you know that two machines behave the same way on every possible input, they could have completely different designs as far as you know.
Extensionality’s function is to solve this problem. Given an avatar of the fact that two machines transform identical inputs to identical outputs, Extensionality can transform the internals of one machine into the other — can make them the same. In other words, if you have a way that an unknown machine could work (and an avatar of the fact that it could work this way) — then you need only say the word, and your unknown machine does work that way, its internal mechanisms are exactly as your blueprints show. The power of Extensionality, if we had it, could strip away the skins of machines and let us work with the ineffable core.
I dream of incarnating Extensionality into a dimension of our world — first a tiny pocket realm of my own devising, and then to the land called Idris, and then… who knows? Wherever I can spread it, I will.
- to be precise: you can do things like “Suppose P. But then we have a contradiction, so we know that not P.” What you can’t do is say “Suppose not P. Then we have a contradiction, so we know that P.” This line of reasoning would only let you conclude that “not (not P)”. ↩