[<< | 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 patch removed: The same machinery that prohibits "f(x) = not f(x)" from being submissible as a rule, if you bother to apply it, also prohibits Russel's formula. Worth note is that this reality is, conceptually, exactly the smart layman's typical first reaction to the problem--which the academic typically waves away with a bunch of obfuscation and indirection even though they are right. (The typical academic knows a number of convoluted, obfuscated, formal answers to the problem, which they fail to recognize, through their own obfuscation, as exactly the layman's first reaction.) Nothing to see here, move along.
The Curry-Howard correspondence, meanwhile, far from being a mysterious similarity between two previously unrelated things, is simply an admission 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.
[<< | Prev | Index | Next | >>]