[PL-sem-jr] FJ subsubsion

[Vasileios Koutavas]

Following my question in last week's PL-Jr about whether one can add a 
subsumption rule in FJ, and after consulting with a friend studying in 
UPenn, here is the answer: A subsumption rule would work fine in FJ, but 
not when you extend it with interfaces together with a conditional 
statement.

The reason is that with interfaces two expressions e1, e2 may have 
multiple "common types". e.g.:

interface I...
class D...
class C1 extends D implements I...
class C2 extends D implements I...

Now the type-checking rule for conditionals (assuming we have a 
subsumption rule) would be:

CT |- if test then e2 else e3 : t
iff
CT |- test: bool,
CT |- e2: t,
CT |- e3: t

Imagine that because of subsumption there is no LUB for t, and we have 
many choices for choosing t (just like in the example above). Then the 
type-checking algorithm wouldn't know which t to choose. If it chose 
randomly then the rest of the type checking would depend on that choice. 
To elaborate say that:

interface I { void m1(); }
class D { void m2(){ return unit; } }
class C1 extends D implements I { void m1(){return unit;} }
class C2 extends D implements I { void m1(){return unit;} }

and now try to type-check the expressions:

(if true then new C1() else new C2()).m1();
(if true then new C1() else new C2()).m2();

(If you don't like that conditional is an expression, I'm sure you can 
find a similar example)
both of these expressions should type-check, but the algorithm can't 
choose differently the type of the conditional in each case.

Supposingly there is an exercise in TaPL that deals exactly with this 
situation, but I've missed it and I don't have the book with me.

--Vassilis