imagery

Pluralities of Ideas

Let’s try a short post for once!

In the shower this morning I had an idea for a blog post. I imagined myself writing this blog post, and some interesting issues came up, and… suddenly I had ideas for two blog posts! I internally debated with myself for a moment before deciding that the second was more interesting, so I dropped the first line of thought and started imagining myself writing the second. Surprise! Another interesting thought, and now I’m trying to hold three blog posts in my head!1

This isn’t just about blog posts. Finding an idea (whether it’s an idea for a program/game/app of some kind, an interesting mathematical notion you’d like to explore more deeply, or just some kind of question) is a lot easier than carrying the idea through to its completion. It is not realistic to ever expect to have “caught up with your backlog” of cool ideas you’ve been wanting to follow up on.

We can look at this pessimistically or optimistically.

On the one hand… there’s this mountain of work growing in your brain, and you’re trying to pull off manageable pieces and get them done but deep down in your bones you know it’s growing too fast for you to keep up, and worse, this is the kind of deep-down-in-your-bones feeling that gets confirmed, not refuted, by rational thought.

On the other hand… maybe it’s not work, but new space to explore. Maybe you’re a mountain climber, and you’re exploring things as fast as you feel like, secure in the knowledge that you’ll never need to slow down to conserve the wilderness. You’ll never run out of new places to go. And this is the kind of security that gets confirmed, not refuted, by rational thought.

(Of course, even if you take the optimistic view, there’s sometimes the worry that you’re not a good explorer. But that is a subject for another day.)

  1. It is probably a good idea to write these down, so. 1) Some Haskell people think there are problems with trying to give a rigorous semantics to IO, and I want to flail around developing a mental model and maybe independently derive their objections. 2) Loosely, monoids are things that can be “smooshed together”, but slightly more rigorously they can be smooshed together in exactly two ways (ab versus ba). What structure might we get by imagining that we can smoosh things together in several ways, or even something like Legos? 3) “Accessible” terminology and some (surmountable?) problems thereof. ↩

Sublime Machines

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.

  1. 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)”. ↩