[Prev][Next][Index][Thread]
Subject reduction fails in Java - Part 2
SUMMARY
-------
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
Wadler.
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.
DISCUSSION
----------
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
joins.
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.
A THIRD APPROACH
----------------
One other approach to the original difficulty is also worth
mentioning.
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
another.
[A similar division of labor between surface and internal language is
being explored by the ML2000 project.]
Regards,
Haruo Hosoya
Benjamin Pierce
David Turner