[PL-sem-jr] FJ subsumption

[Vasileios Koutavas]

On Mon, 4 Dec 2006, Carl Eastlund wrote:

> 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.

I think that what you are proposing would work, but it would mean to
change the type judgments to have the form:

CT |- e : {t1, t2, t3...}

where t1,... are all the possible types that e can have, and then take
the intersection of these sets at conditionals.

But I wouldn't like this type system for plain-old FJ, just for the
purpose of being extensible to interfaces *and* keeping the subsumption
rule. If they can get away by just removing subsumption, I think it's
cool.

--vassilis