[PL-sem-jr] (correction) FJ subsumption

[Vasileios Koutavas]

I obviously meant subsumption... :-)

On Mon, 4 Dec 2006, Vasileios Koutavas 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.
> 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
>
> _______________________________________________
> Pl-sem-jr mailing list
> Pl-sem-jr at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-sem-jr
>