14 December 2011

There Are Only Types

I never liked object-oriented programming. I started programming half a lifetime ago, and I found object-oriented languages early on, because of their popularity. For the most part I was uncomfortable with them, but it took some time to learn enough about programming to really understand why.

So I became proficient in Java and C++ and what have you, and I acknowledge that these languages can be useful for some things. If a language has some library that lets you get your task done quicklier or at lower cost, then it’s probably safe to choose it over another language that might be better, in the usual sense of “good” = “expressive”. Quality isn’t the whole story when it comes to quality.

It wasn’t the many fanatical followers of what seemed more like a radical philosophy than an actual technology that ultimately turned me away from OOP. I realised at some point that the primary reason I disliked that world was the fact that I find it really difficult to decompose the world in terms of objects. Not because I found object-oriented programming difficult; just that I found it unnatural.

I’ll clarify. An object is an entity that responds to messages and has some internal information. But not all things conceptually talk to one another, nor have state; so I thought this was backward; why think about entities that manifest qualities, when you can just think about qualities themselves? Why would you declare the contracts (interfaces) between entities before you know if those contracts are true? And most importantly, why would you use two different languages to compute the values and types in one program?

This is how I—inadvertently—came to independently reinvent the concept of dependent type systems. Values depend on types, which can be verified and manipulated and so forth; but types, too, depend on values, and this reverse relationship is treated in exactly the same way. For a trivial example, in a dependent type system, you can encode the type “list of size N with elements of type T”, or “sorted list” or “balanced tree”. A dependent type system in an imperative language would obviate the need for a lot of explicit imperative implementations of contracts on data structures.

But I went a step further than that. Conceptually, types tend to be computed as a side-effect of computation on values. That is, almost any language you can name is interested in computing values, and only verifies types as something of an afterthought—assuming, of course, it verifies types at all. This is true even of languages with very rich type systems such as Haskell.

But what if, I thought, you were to turn that on its head? I became intrigued with this problem around +37 (2007), I think, and set about designing a language in which, essentially, all terms denote types and values are computed as a side-effect of reasoning about those types.

For example, the term “3” is not just the value 3, but a reference to the set of all underlying values that are equal to 3. By “underlying value”, I mean machine representation: every possible size and signedness of integer or floating-point number. But, since types were computed non-strictly, the singleton type of 3 could be represented with a regular old machine integer, which would be converted only as needed.

There are several advantages to dealing with singleton types rather than ordinary values. The first is that value equivalence becomes explicitly type- and context-sensitive, rather than implicitly so; type equivalence behaves similarly if you generalise to singleton kinds. And though it may not be immediately obvious, type checking within a type system based on singleton types is statically decidable, because singleton types are basically just equivalence classes, and subtypes form proper subsets of those classes. That means, essentially, that we can prove some kinds of extensional equality.

So singleton types have a few perks, and they coexist nicely with a dependent type system. Unfortunately, dependent types are not statically decidable, because you cannot, in general, prove that two functions are extensionally equal, which is what statically deciding dependent types would require.

But that’s actually not such a bad thing. In a system with singleton types, the types themselves contain enough information to provide more reasonable diagnostics in the event of a type error. And of course the compiler would not attempt to decide all types statically, but only those which are known to be decidable; the rest would be decided dynamically. Taking this view, static typing can be seen as a constant-folding optimisation, and likewise constant-folding can be seen as a form of static typing, for in this system types and values are one and the same.

I never did finish the language that would implement these ideas, but I fully intend to. And at the very least, exploring this field gave me some insight and informed my ability to write programs in existing languages. But to this day I have to shake my head at the languages I still use every day, from C++ to Haskell.

Because they don’t know that there are only types.