Featherweight Musings

Monday, January 14, 2008

Existential types everywhere!

I am certainly biased in this respect, since most of my research work has been with existential types, but I think that existential types are vastly important to the world of OO programming languages, and probably the rest of PLT too. Existential types give us a way of expressing data hiding (i.e., abstraction) in the type system, and seeing as this is what most of software engineering is all about, it shouldn't be surprising that existential types start cropping up all over the place.

My own work has so far focused on Java wildcards, which are a (relatively) simple way of using existential types to deal with the mismatch between parametric (i.e., generics) and inclusion (i.e., subclassing) polymorphism. In the same way I have found existential types to be useful in the world of ownership types. I believe Werner Dietl is having a similar experience with universes.

Existential types are also a foundational model for objects themselves in OO languages. And, I suspect, are a better way of thinking of generic classes than the universal types that people often assume.

Furthermore, I've found some pretty elegant tricks that can be played using existential types mechanisms such as packing and unpacking types, in the realms of path dependent types and virtual classes. I'm pretty sure the same techniques can be used elsewhere.

More than a whiff of existential types can be had all over the place in current research, delayed types, ownership domains, and MOJO all come to mind, and I'm sure I've come across more that I can't remember.

And so what? Well I'm not sure, but I guess I'm glad I've managed to get pretty deep into existential types. I'm sure they'll keep coming in useful for some time to come.