[PL-sem-jr] FJ subsubsion

[Carl Eastlund]

On 12/4/06, Vasileios Koutavas <vkoutav at ccs.neu.edu> wrote:
> 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.

True, but if the typechecking algorithm had a constraint solving
system that carried around intersection types, it's possible it could
resolve the ambiguity as it needed to and still express a final
solution in regular old class-and-interface types.  Where multiple
options persist to the end it could choose one arbitrarily and where
none persist it would fail.  Of course that's more in the realm of
type inference than typechecking, and I have no idea if it makes the
type system intractable or undecideable.

-- 
Carl Eastlund

> 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