I need a name...

Virtual types/classes are very cool. I firmly believe that they are a "good thing" in the world of programming language design. Especially when combined with dependent types and you get the likes of vObj/VC/Tribe. Tres bien!

However, the trouble is, there are so many flavours: virtual types, virtual classes, nested types, nested classes, nested inheritance, family polymorphism, higher order hierarchies, virtual patterns... I want a name to describe the whole bunch of various flavours where a class or type may occur inside another class or object and there is some kind of inheritance, binding or subtyping between the 'inside' classes or types. Trouble is, all the good names (and permutations of names) have been taken...

Alex Buckley, King of the (Java) world!

Friend, former colleague and Imperial alumnus Alex Buckley is now King of the World, or at least, the Java spec. This is very impressive, well done to Alex and I'm sure he'll do well. We'll miss Gilad though...

So, Flexible Dynamic Linking in Java 7.0 then?

Expressible and Denotable types

Wildcards were added to Java in version 5 to make generics more useable (that is, more powerful and flexible). Whereas most people understand generics pretty quickly ("so its a List of Strings, not just a List"), wildcards seem much more widely misunderstood and confusing. One reason is that they are undoubtedly more complex (compare WildFJ to FGJ). But, I believe another reason they are hard to use (and understand) is that the programmer can create types that can not be defined in the syntax. To quote Erik Meijer (on a different mechanism), Java has types that are "expressible but not denotable". This basically means that the type system can say what they are, but the syntax can't. Here's an example:

<Z> Pair<Z,Z> makePair(List<X> l) {...}
<Z> void usePair(Pair<Z,Z> p) {...}
void m(List<?> x, Pair<?, ?> y)
{
    usePair(y);            //type error
    usePair(makePair(x));  //OK
}

Weird, huh? The type checker knows that makePair(x) has type Pair<?, ?>, but the ? represent the same types, whereas in the type of y they represent different types. Unfortunately this can't be denoted in the syntax (thus the soundbyte: types can be expressed by the programmer but not denoted).

So, Java has expressible but not denotable types, so what? Well you can probably see the kind of ugly situation that occurs from the little example above. Type correctness becomes confusing and surprising (for the programmer, never good). Also, I believe, since there is no syntax for the types, they become harder to reason about by a programmer (they are certainly harder to reason about formally, but more on that another day...).

It seems then, that having 'expressible but not denotable' types is bad language design. Certainly, if I were to design a language (after playing with Wildcards for a year), I'd avoid expressible but not denotable types like the Black Plague. However, is there an alternative? The way to reason about these types formally is to use existential types. So we could replace wildcards with existential types, but to be honest this would probably make it more confusing. The above example becomes:

void m(∃Y.List<Y> x, ∃X,Y.Pair<X,Y> y)
{
    usePair(y);            //type error
    ∃Y.Pair<Y,Y> z = makePair(x);
    usePair(z);            //OK
}

The extra assignment isn't necessary, but shows you the type can be denoted. Not so nice huh? And don't even ask how you'd type '∃' in an ASCII editor. So, can anyone think of an alternative?

Hello World

I will blog and no one will read (probably). (This is my mission statement.) But if anyone does, then they can expect musings and observations on the world of programming language design and theory (exiciting stuff, eh?). These will be un-backed up, un-supported, un-important and, mostly, un-reasonable. If they were anything else I would write them somewhere sensible....