[Prev][Next][Index][Thread]
Re: forwarded message from Benjamin Pierce
[This TYPES posting will be followed by several more: I've just
returned from a trip and am catching up. Sorry for the burden on your
inboxes. --BCP]
-----------------------
Date: Fri, 19 Jun 1998 09:48:36 -0400
From: Robert Cartwright - Sun Microsystems <cork@East>
Subject: forwarded message from Benjamin Pierce
Ben Pierce has discovered that subject reduction (the usual
formulation of type soundness) fails for a technical reason in Java.
The culprit is the type checking rule for conditional expressions;
t ? a : b
is type correct for reference types only when the type of b is a
subtype of the type a or vice-versa. I was not aware of this rule! I
assumed that the result type of t ? a : b would be the least upper
bound of the types of a and b. I am interested in why the more
restrictive rule was chosen. The more liberal typing rule eliminates
Ben's counterexample.
As I recall, the principal difficulty is that lub's are not unique
when interface types are involved. Rather than try to define a more
complicated rule to deal with interfaces, Bill and I decided to have
the more restrictive rule, which, in effect, punts the problem to
the programmer. The "workaround" is for the programmer to provide
an explicit cast in one of both branches of the conditional. Such casts
are always widening and therefore do not result in any runtime cost;
moreover, they serve as excellent documentation in the source code
as to exactly what is intended.
As for subject reduction, it is incorrect in the form that Ben stated it
in his original message, even if conditional expressions are not used,
because of method overloading. Consider this program fragment (derived
from Ben's example):
Integer i = new Integer();
int n = m (i);
Now, suppose that the method m above is defined as follows:
int m (Object a1) {
return foo(a1);
}
where the method foo is overloaded:
int foo (Object a1) {
return 1;
}
int foo (Integer a1) {
return 2;
}
This code is well typed. But if we "beta-reduce" the call to m, we obtain
Integer i = new Integer();
int n = foo (i);
and now n will get the value 2 instead of the correct result 1.
I believe that the *correct* reduction rule is: Given a definition
R m (T1 x1, ..., Tn xn) {
return r;
}
of a method m with parameters x1...xn of types T1...Tn and result type
R, we expect to be able to rewrite a call to m of the form
m(a1...an)
by "inlining" the body r, replacing formal parameters by corresponding
arguments THAT ARE CAST TO THE CORRESPONDING DECLARED PARAMETER TYPES:
m(a1...an) --> r[(T1)(a1)/x1...(Tn)(an)/xn]
This version of the rule appears to take care of at least the method
overloading problem and the conditional expression problem.
--Guy