Subject reduction fails in Java - Part 2


Our posting yesterday seems to have generated an unusual amount of
activity on the TYPES list!  The responses so far (both postings and
some private emails) have basically been of two forms:

  1) Some people reiterated our suggestion that a "beta reduction" rule
     for Java should explicitly cast the arguments to the parameter
     types before substituting.

     This solution has the advantage of dealing with the (related)
     difficulty with subject reduction and overloading, observed by 

  2) Others proposed a different solution: change the original typing
     rule for conditionals from

                     b : bool    e1:E1     e2:E2
                         T=E1>E2  or  T=E2>E1
                            (b?e1:e2) : T

     to (some variation of):

                     b : bool    e1:E1     e2:E2
                           E1 < T   E2 < T
                     ---------------------------       (*)
                            (b?e1:e2) : T

     That is, take the type of the conditional to be any common
     supertype of the types of the branches.


The second proposal is one that we also considered [and should have
discussed in the original posting].  The problem with it is that a
typechecking algorithm typically needs to calculate a single _minimal_
type for each term.  But, the suggested rule (*) only admits minimal
types if the subtype relation possesses a join for every pair of
types.  Java's subtyping relation, unfortunately, does not have all

For example, suppose we have Java interfaces A, B, C, and D, with the
following subtyping relations declared among them:

        A     B
        |\   /|
        | \ / |
        |  .  |
        | / \ |
        |/   \|
        C     D

Now suppose that we have declared variables x of type C and y of type
D.  Then, according to the rule (*), the expression

    (b ? x : y)

could validly be either type A or type B, since these are both common
supertypes of C and D.  But C and D have no minimal common supertype
(there is nothing in the position marked . in the diagram), so there
is no "best result type" for the typechecking algorithm to return.

The lack of joins seems to be a basic property of Java's approach to
typing.  We do not see any way to "add in joins" without substantial
and fundamental changes to the type system.


One other approach to the original difficulty is also worth

  3) We might choose to regard the typing of the conditional as a
     _type inference_ problem.  In this view, we would distinguish
     (a) the surface language in which the programmer writes from (b) 
     a "fully typed" internal language, where some annotations have been
     added by the compiler.  In the internal language, the conditional
     expression would be given an explicit type annotation

       (b ? x : y) in T

     that would determine its result type exactly:

                     b : bool    e1:E1     e2:E2
                           E1 < T   E2 < T
                        ((b?e1:e2) in T)  :  T

     The transformation from surface to internal language would
     involve filling in the "in T" annotations on conditionals using
     some simple rule such as the one currently used by Java.
     (Overloading resolution might also take place at this point.)

     Subject reduction would then be a question of preservation of
     typing by reductions of one internal language expression to

     [A similar division of labor between surface and internal language is
     being explored by the ML2000 project.]


        Haruo Hosoya
        Benjamin Pierce
        David Turner