Sunday, March 30, 2014
OKR 3 - Type Theory Weary
Previous entries in this series:
- On Knowledge Representation
- OKR 2 - Examples of Intuitive Reasoning
What is "type"? What is the difference between an integer and a string? If I have two lists of different lengths, are they the same type? If integers are a distinct type from reals, then are prime numbers a distinct type too? What's the connection between types and classes? Are primes a subclass of integers (and integers of reals)? What are type systems, type theory, type inference all about?
If you look at existing Type Theory you might conclude that there's something very fundamental about the concept of type--that there's a good reason we've fussed over it in such depth for over a hundred years, resulting in stuff like this:
Turns out, nah.
Well, there's a reason, but it's not exactly good. Type theory is an attempt to recover from excessive reductionism of the atomic, platonic value paradigm (and associated computational models)--something like the study of juggling with your hands tied behind your back.
Let's see what we can do with free hands.
If you recall a central idea in OKR is that rather than thinking in terms of (usually platonic, atomic) values held in variables, we can think in terms of predicate relations on and amongst variables. That is, rather than the variables being buckets that hold things, they are merely unique identifiers about which we know things. For the case of a simple value assignment, X=7 becomes 7(X), so we haven't lost that ability. But we can also, in the same manner, say things like Prime(X), GreaterThan(X, Y), and so on.
In effect, in an infinite and continuous space of all possible things, with each new relationship over some X we are carving away at the domain of where or what X can be. When that domain falls entirely within a single "value" partition (as implicitly defined by some type), then we say we know X's value (with respect to that type). For instance, if we know GreaterThan(X, 5), LessThan(X, 11), and Prime(X), then we can infer 7(X), aka X=7. These value partitions are not special constructs, but rather simply implied by the logic (tables) amongst mutual relations. For instance, 7(X), 3(Y), and Sum(X, Y, Z) implies 10(Z). That is, if we know X and Y down to single integer partitions, then we can infer their sum down to a single integer partition too. But it's also true that GreaterThan(X, Y), Positive(K), and Sum(X, K, Z) implies GreaterThan(Z, Y), which is exactly the same sort of inference, just on larger partitions. Furthermore, even these smallest partitions are not atomic--7(X) does not mean that X equals the platonic 7, but merely that X is one of the infinite number of things that fall within the 7 partition. To give a real world example of this, the IEEE floating point standard distinguishes +0 and -0. That is, while for most purposes 0(X) represents what we call a single value, for some purposes it represents two, and it is useful and important that our knowledge representation simultaneously and gracefully handle both of these interpretations.
By here it should be evident that a type declaration like Real(X) is just another domain reduction on X like any other, from which we can draw inferences just as we did above, as in: Real(X), Real(Y), and Sum(X, Y, Z) implies Real(Z). Presto--we have type inference. And oh by the way, we have dependent types as well, and pretty much all the other features of every type system out there too, because what those type systems are is an ad-hoc attempt to re-introduce the most important cases of general relational inference onto an impoverished model.
In sum, type is just the name we give the most general partitionings of our space of things, and value is the name we give the finest ones (and we largely avoid the vast and useful domain inbetween!). That they are qualitatively the same should be evident just from the fact that dynamically typed variables typically consist of a compound value which encodes both their type and their value within the domain of that type. I.e., the type is itself a part of the value (even if it is implicitly encoded as with statically typed languages).
Or, put the other way, values are just very specific types.
The bottom line is that value computation and type inference are both just examples of relational inference, far more alike than different despite traditionally being handled as independent and complementary domains. The reason the various programming language type systems out there feel essentially like little programming languages in themselves is because that's exactly what they are, and it is mainly through historical mishap and inertia that there is this huge abyss between values and types rather than an unbroken continuum. Object oriented programming, dependent types, first class types, and so on are all ad-hoc attempts to bridge this abyss--but using only what's left (i.e., starting with the values-in-containers paradigm and impoverished types).
Much easier just to not dig that abyss in the first place.