Martin-Löf and the Problem of Everything
(Or: How I Learned to Stop Worrying and Love the Lambda Cube)
I knew I was in too deep when I started sketching Π-types in the margins of my planner like they were protective sigils. Martin-Löf didn't just give us a logic. He gave us a nervous system for formal reasoning—and I'm not sure mine is firing correctly.
So, dependent type theory. For normal people: it’s a formal system where the types of expressions can depend on values. For masochists: it's what happens when logic, programming, and the dream of epistemic precision all go to group therapy together.
Imagine saying, “The type of this proof depends on the value we’re proving about.” That’s it. That’s the tweet. But it unlocks a universe of things you can express—like actual meaning in logic—and a universe of ways to collapse under the weight of that expressiveness.
It started with Curry-Howard. Propositions as types? Proofs as programs? A logic that doesn’t just describe reasoning but is reasoning? I was gone. Then the Π-type rules came in like hot coffee on a cold brain: you can quantify over families of types, model universal statements, and build real functional systems of thought. It’s so clean—until it isn’t.
But the cube. Oh god, the cube.
Each axis was supposed to help, right? Add polymorphism here, higher-order types there. But I got cocky. I looked into the Calculus of Inductive Constructions like it was a gentle stream and not a black hole where universes stare back. Suddenly I’m asking myself if equality is even meaningful anymore. My friend asks how I am. I say “non-trivial.”
Martin-Löf forces us to face what most logical systems don’t: that meaning and structure can’t always be separated. That our definitions aren’t passive. That logic isn’t just a game—it’s a model of knowing. And if our model collapses under its own weight? That’s still a kind of knowledge.
I drew the lambda cube on a Post-it. It’s crying. So am I.
But I’m going back in.
Recommended Readings
[1] Howard, William A. (1980). The Formulae-as-Types Notion of Construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism.
[2] Barendregt, H. P. (1991). Introduction to Generalized Type Systems. Journal of Functional Programming.
[3] Martin-Löf, Per. (1984). Intuitionistic Type Theory. Bibliopolis.
I knew I was in too deep when I started sketching Π-types in the margins of my planner like they were protective sigils. Martin-Löf didn't just give us a logic. He gave us a nervous system for formal reasoning—and I'm not sure mine is firing correctly.
So, dependent type theory. For normal people: it’s a formal system where the types of expressions can depend on values. For masochists: it's what happens when logic, programming, and the dream of epistemic precision all go to group therapy together.
Imagine saying, “The type of this proof depends on the value we’re proving about.” That’s it. That’s the tweet. But it unlocks a universe of things you can express—like actual meaning in logic—and a universe of ways to collapse under the weight of that expressiveness.
It started with Curry-Howard. Propositions as types? Proofs as programs? A logic that doesn’t just describe reasoning but is reasoning? I was gone. Then the Π-type rules came in like hot coffee on a cold brain: you can quantify over families of types, model universal statements, and build real functional systems of thought. It’s so clean—until it isn’t.
But the cube. Oh god, the cube.
Each axis was supposed to help, right? Add polymorphism here, higher-order types there. But I got cocky. I looked into the Calculus of Inductive Constructions like it was a gentle stream and not a black hole where universes stare back. Suddenly I’m asking myself if equality is even meaningful anymore. My friend asks how I am. I say “non-trivial.”
Martin-Löf forces us to face what most logical systems don’t: that meaning and structure can’t always be separated. That our definitions aren’t passive. That logic isn’t just a game—it’s a model of knowing. And if our model collapses under its own weight? That’s still a kind of knowledge.
I drew the lambda cube on a Post-it. It’s crying. So am I.
But I’m going back in.
Recommended Readings
[1] Howard, William A. (1980). The Formulae-as-Types Notion of Construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism.
[2] Barendregt, H. P. (1991). Introduction to Generalized Type Systems. Journal of Functional Programming.
[3] Martin-Löf, Per. (1984). Intuitionistic Type Theory. Bibliopolis.
Comments
Post a Comment