[<< | Prev | Index | Next | >>] Friday, August 14, 2026
Demystifying Type (and some Un-Paradoxing)
[programming language theory, type theory, epistemology]
This is more or less an addendum to Type Theory Weary so you might want to start there, but I'll try to keep this self-contained:
I've struggled roughly forever with what exactly "type" is, means, and adds. Eventually I realized it added nothing (to an adequate foundation)--hence my years of confusion. But there is one lingering thing that wouldn't go away, which occurred to me recently and I will outline below.
As for it adding (almost) nothing, the history of it is that academics in computer science and mathematics had constructed various systems which were either too restrictive or too presumptuous, and needed to bring in more machinery to fix the problems caused by that.
Russel's Paradox, for instance, ultimately spawns from a presumption that every formula you can write down has a well-defined value. This is nearly as silly as overlooking that "f(x) = not f(x)" is not resolvable, just one level of indirection/obfuscation removed.
The Curry-Howard correspondence, meanwhile, far from being a mysterious similarity between two previously unrelated things, is simply the observation that the type systems bolted on to programming languages were just re-introducing some of the relational logic that had been stripped from them.
The lesson in these unflattering summaries is: Better to look first for the cause of a problem. Undoing a previous mistake is always better than compensating for it.
Relevant for the concept of "type" because it has a lot of baggage (in part to solve the non-problems above). It seems to be very important, to carry a lot of weight, to be central to "correctness" and factoring (classes) and so on. So the implication that it's not needed or useful seems a bit preposterous on the surface.
But we just need to unwind some history and rebuild things more simply and we land on something much simpler and more general. (It's disturbing how much longer it takes to unlearn something than to learn it. I feel like I've spent my whole career scrubbing crap out of my brain that I was supposed to just take for granted.)
Firstly, as noted in Type Theory Weary, nearly all the functionality of "type" is trivially subsumed by a decent relational representation. That is to say, it's not so much that type is a useless concept as that it's an already existing one: Type, in its most general form, is synonymous with relational membership. I am mixing two paradigms there (relational logic, set membership) just to avoid over-constraining the point: Call it set membership, call it truth values on a predicate function, it doesn't matter--it's a common, intuitive idea. "fruit" is a "type". So is "values greater than Y". Why we tend to think of the former as a type far more often than the latter for mostly pragmatic reasons (to follow), but they are the same epistemic construct.
Historically the critical bifurcation between "value" and "type" came down to this: Value is what can be reliably computed when a program is run. Type is what can be reliably computed when a program is compiled. The key here is that the representation and rules of computation can be totally unified here (e.g. relational logic), but historically haven't been because of the pragmatically different roles of these two groups.
Furthermore, it follows, if we start to blur the line between compilation and execution, this pragmatic boundary also breaks down, and we're immediately better served by abandoning it entirely and sticking with a single, unified representation that draws no distinction between type and value.
So that is, in various ways, my argument against the need for type as a special construct: Everything we normally do with type still remains, just now as ordinary relational facts and rules, on the same footing as everything else.
But there is one important exception. And this, I think, is what has anchored the concept of type (as a special construct) from floating away long ago:
When we revisit my definition above, that type is what can be reliably computed when a program is compiled, this implies something else: It is what is known when the program is written. That is, it is what the programmer himself knows. To be sure, it is just a subset of that--which again strongly hints that we would do better to move to the more general representation. But it is, in particular, a very easy subset: type logic, in general, is pretty trivial (if we strip away all the code particulars except the type information, we are left with a very basic data flow problem, to the extent the types aren't already explicit everywhere). And this easy-to-infer (at code-writing or compile time) subset of our relational truths creates an implicit context for the code we write. And this context in turn provides the final, actual, somewhat trivial but truly special-construct function of "type": It lets us disambiguate language at the syntactic level.
That is, for instance, it lets us write the word "length" and to have the compiler--like the programmer himself or someone reading the code--know whether we mean a count or a geometric magnitude. And I should stress here that code that leaves this to the runtime should be un-compilable: If you don't know when you're writing the code which meaning of length you mean, then you don't know what you're writing and neither does the compiler. Do not confuse this with dispatch where we might do the calculation in various different ways depending on the particulars of the object. What we are resolving here is what (meaning) we are calculating, not how.
We see this in practice in, e.g., C++ or Java style static typing, and the value of it is simply compression of language: allowing us to re-use the same word for different (though often similar-ish) meanings.
What's important and useful to see here is this stark functional division:
Static type-based meaning disambiguation is entirely a convenience function for communication, syntactic sugar in effect, that lets us write a bit less by re-using tokens for different things in different contexts. It's a small bit of code compression, and that is all. And that is the one true special function that "type" serves.
But also, now seeing this, we no longer need to restrict what qualifies as type, outside of one property: That it be figurable at compile time (that it be evident in the code itself before we know the parameters/data). I.e., in principle we can use anything as a contextual disambiguator, and needn't restrict ourselves to neat type hierarchies or whatnot. That we do in general is just a pragmatic reality about what is usually easily figurable when a rule or procedure is conceived, and how our language (both natural and mathematical) is evolved around that.
Everything else--and all the of heavy lifting we usually attribute to types--is now just relational logic as usual. Not gone, not useless, just no longer a special case. All the same patterns apply, just now without the restrictive line down the middle.
2026-08-18 Q&A:
I think you're reinventing Curry-style "extrinsic" types? I think everyone in principle would love to take your approach, and the fields of refinement/liquid types are the main concrete efforts in these directions. But you quickly end up with undecidability and unpredictable compilers.E.g. (example from Fable): In your unified system, suppose length is disambiguated by context, and contexts are arbitrary relational facts. When the compiler sees length x where x is known to satisfy predicate P, and one meaning of length expects arguments satisfying Q, the compiler must decide whether P entails Q — at compile time, for arbitrary P and Q. What's the algorithm?
Also, would your algorithm reject Y = (Y → P) for arbitrary P? It doesn't contain a negation.
Finally, what's the type of Type?
Re. I think you're reinventing Curry-style "extrinsic" types?... Firstly, I'm proposing that "type" is, more or less, not a thing. As in you literally don't need it and it doesn't hurt you at all (besides losing a small amount of syntactic sugar) to get rid of it entirely as a formality. You can keep it as a notion, but as a notion it's just like lots of other notions that you freely use in programming via the existing tools. (That is, once your "existing tools" are general enough. My claim is that it exists as it does specifically to have filled in that gap in the meanwhile.) Is that the crux of extrinsic types?
Secondly, I think it's fine if your compiler can't compile every well-formed program. I think if it can, that's a sign your language isn't expressive enough. That constraint is driving the problem from the wrong side -- it should be driven firstly from the side of clarity of expression, and strictly after that from ease (but unlikely ever guarantees) of execution/realization.
My answer to the undecidable cases is rather simple: Don't do those. Why would you anyway? Our goal is to write programs that do useful stuff, easily. Not to write programs that befuddle our compiler (which almost certainly are programs that befuddle most or all humans too). If there's a genuinely useful case that has a clear answer to humans and not the compiler, almost certainly you can heuristic that in by whatever (meta?) logic humans use.
E.g., you say "What's the algorithm?" and I say: The compiler prints a message that says "What the matta you? Stop that." This is why most type systems are actually quite simple and unexpressive -- because the real function of them is just to track the most obvious contextual flows that allow humans to disambiguate language a bit. I.e., the human answer to your same question is: Don't do that. Natural language is evolved to allow ambiguity (more or less) only where it's consistently easily resolved. We just don't do the confusing/unresolvable cases. Furthermore, we adjust our writing to avoid them: On the occasion that normal language use leads us to an ambiguous statement, typically we notice it and choose a different wording. Worst case our editor sends the draft back with some markup to that affect -- same as the compiler rejecting our code for being ambiguous/unsolvable.
"Also, would your algorithm reject Y = (Y → P) for arbitrary P? It doesn't contain a negation." This inherently isn't a problem if you reject naive comprehension in the first place. It is Not an axiom of the language that anything you can express in the language is true (nor that any type you can express is consistent). In practical terms we come back to "Don't do that". In fact most code defines new terms, which can never go wrong: You write inconsistent code, you are simply defining a new name for False or the empty set. The foundation of logical deduction has to be entered carefully; "true=false" as a hypothesis is always allowed (it proves false); "true=false" as a rule requires privilege to claim, and breaks the language if you do. Essentially all daily programming only requires the former.
As for the type of type, there isn't just one. The concept of type is used for a number of different things, and they all just become those things. Sets, equality class, representation/implementation, etc. I would use set/domain membership for lexical disambiguation. Most (all?) of "type inference" is just a natural side effect of propagating relational/functional domains (which can be specified to an arbitrary level of precision, right up to compile-time evaluation, only the loosest of which we're used to calling "type").
--
It helps to understand the root of the popular supposed paradoxes: Based on the premise that any non-recursive, non-looping function terminates, it was presumed that any type definition written under those constraints was terminating and hence consistent/inhabited. But you can turn one of those into a recursive function after the fact by passing it to itself as a parameter, and boom. So the error is just the false premise in the first place. You don't need it.
[<< | Prev | Index | Next | >>]