[PL-sem-jr] FJ subsubsion

[Richard Cobbe]

On Mon, Dec 04, 2006 at 12:51:26PM -0500, Carl Eastlund wrote:
> 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.

Not so much interfaces as a <: relation that's a DAG rather than a tree,
but sure.

<SNIP>

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

Putting the same thing a slightly different way:

As I said to Sam during discussion at the seminar on Friday, there is in
principle nothing wrong with having a nondeterministic type system.  So, in
FJ plus subsumption, interfaces, bool, and ?:, you could write the type
rule for ?: as follows:

    G |- e1 :: bool    G |- e2 :: t    G |- e3 :: t
    -----------------------------------------------
            G |- e1 ? e2 : e3 :: t

(I use :: to mean "has type" to avoid confusion with the : literal in the
language.)

Then, in Vasileios's example with interfaces, you could simply rely on the
type system to make the appropriate choice at each point and it will all
work out.  Of course, with additional language features it gets a little
messier: in the presence of Java-style method overloading, it's possible to
have one expression that can have any of several unrelated types depending
on which way the nondeterminism goes.

As Carl and Vasileios have pointed out elsewhere in the thread, and as I
also said on Friday, this nondeterminism in the type system makes it hard
to implement.

There are several options for recovering determinism.  Java 1.4 does this,
roughly:

    G |- e1 :: bool    G |- e2 :: t2    G |- e3 :: t3
                (t2 <: t3 or t3 <: t2)
    -------------------------------------------------
            G |- e1 ? e2 : e3 :: max(t2, t3)

(Other rules apply if either e2, e3 is the literal "null" or has numeric
type, but those aren't interesting here.  And <: is a slight
over-simplification, but again, not interesting.  See JLS 2, section 15.25
etc. for details.)  In Java 5, the situation is made more complex by the
presence of generics, and I'm too lazy to sort through all the formalisms
in JLS 3 to figure out exactly what the restrictions are.

Another strategy is simply to require, in the type rule, that t2 and t3
have a LUB and use that.

Richard