Typeful Dynamic Programming, or, Java/C# Generics and what does F-bounded polymorphism have to do with it?

On LtU, Anton van Straaten repeatedly and vehemently made the point that users of dynamically type-checked languages don't program without types. Instead, in my interpretation, they do they type checking and inference in their heads.

Now, Java can in fact be used as a dynamically type-checked language: just declare all your variables, parameters, and return values as Object, and use instanceof to dispatch on types or reflection to invoke methods. Runtime type information (RTTI) saves the day. But, Java with generics also offers a quite potent type system. (Even if it's hampered by type erasure for backwards compatibility. C# keeps RTTI about polymorphic type variables around (the actual class of T in List<T>).)

And Java's generics are in turn based on F-bounded polymorphism for object-orientation, a nice and rather simple way for type checking parameterized classes. F-bounded polymorphism can do cool stuff like solve the expression problem (if heavy-handedly), and type families of mutually recursive types.

* * *
I recently had the case of a Listener, that's parameterized over its Broadcaster, that again is parameterized over the listener. But I didn't know Java generics well by then, and just gave up on typing it. With F-bounded polymorphism, the two types could be defined like this:


It's weird, but I'm developing a bit of intuition about it. And I have to say, the expressivity is nice, even if the syntax is bad. But my hope is that macros can help factor out some common use cases of F-bounded polymorphism.

* * *
One of the goals of typesystems like O'Caml's is to never have to store runtime type information (RTTI). But in a Lisp or other dynamic languages, users are already prepared to pay for RTTI anyway, so type systems can be layered on top of the completely dynamically type-checked language. What does this say to us as people looking for the ultimate dynamic language?

For one, there's a vista that an advanced type system like F-bounded polymorphism and a at its core dynamically type-checked language can work well together. (Cecil does exactly this.) O'Caml and Haskell programmers routinely write down the exact types of variables and functions. And anyone who has ever experienced these languages knows about the value of their type systems (no pun intended). Let's try out advanced types in dynamic languages!

Second, in a completely dynamically type-checked language augmented with an advanced type-system, compiler type errors become warnings about potential runtime type errors. Why? Because it's guaranteed that you'll get a runtime error for type violations from the dynamically type-checking core language anyhow. This means, the error listing from the compiler changes to a dynamic console of current warnings about expressions that may yield a runtime type error, if executed. But the compiler lets you start your program anyway. Until you hit the first actual error.