Type Constructor Polymorphism

I'm starting to dig type systems, which I have ignored for years. I'm still not able to make it through a single page of TAPL in one sitting, so my learning here is purely intuitional.

I think generics in Java are quite nice, surface issues aside. (In theory, that is. In practice, "Java seems to have been designed to strike a careful balance between making the type system as obstructive as possible while minimizing any actual guarantees of correctness" →. I think this is mostly due to Java's lack of RTTI for generics. C# doesn't have the same problems, except in places where they intentionally copied Java.)

My first nice discovery was that there's a beautifully simple theory behind generics: F-bounded polymorphism. (Reassuringly, it wasn't developed in academia, but by practitioners at HP Labs.)

In ordinary bounded polymorphism, you can give bounds to your type parameters: A <: Foo. The bound here is Foo, which means that all actual As must be subtypes of Foo.

F-bounded polymorphism is a simple extension of ordinary bounded polymorphism, in which the bound may recursively contain the type it bounds: B <: Bar<B>. It turns out that with this simple (but at first somewhat confusing) concept, we can statically typecheck the expression problem, which is a standard measure of the worth of a type system.

Type constructor polymorphism is another beautifully simple theory. In type constructor polymorphism, the bounds of your types may not only be concrete types, but also functions from types to types: C <: F<D> says that Cs must be subtypes of Fs, which are type-level functions that take a D as input. (Type constructor polymorphism also works naturally with F-bounded polymorphism.) It turns out that with this simple concept, we can statically typecheck GADTs, an advanced issue in typeful programming.

My take-away: so far studying type systems has been a lot of fun, though extremely challenging, and the concepts are simpler and more profound than I thought. As long as we keep type systems optional, and never let them get in the way, I think we should strive to understand and apply them in new languages.