[Prev][Next][Index][Thread]
Subject reduction fails in Java
We were recently surprised to discover that Java fails to possess a
straightforward analogue of the familiar SUBJECT REDUCTION property of
typed lambda-calculi. This note sketches a counterexample and briefly
discusses its significance.
Regards,
Haruo Hosoya
Benjamin Pierce
David Turner
"SUBJECT REDUCTION" IN JAVA
---------------------------
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 might 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:
m(a1...an) --> r[a1/x1...an/xn]
Unfortunately, this inlining operation does not, in general, preserve
typing. That is, it may be that both the definition and the use of m
are well typed, but that the "contractum" r[a1/x1...an/xn] is not.
COUNTEREXAMPLE
--------------
The culprit here is the innocent-looking conditional expression
b ? e1 : e2
which yields e1 if the boolean expression b is true and e2 if b is
false. The typing rule for such expressions given in the Java
Specification (page 367-368) says:
1) the guard b must have type boolean
2) if the bodies e1 and e2 have reference types E1 and E2, then
either
2a) E1 and E2 must be identical, or
2b) one of E1 and E2 must be a subtype of the other.
3) similar conditions when E1 and E2 are numeric types or the
special null type.
Now, suppose that the method m above is defined as follows:
Object m (Object a1, Object a2) {
return (b ? a1 : a2);
}
That is, it takes parameters a1 and a2 of type Object and returns
(b ? a1 : a2), where b is some boolean expression. The body (b ? a1 : a2)
is well typed, using rules 1 and 2a above.
Next, consider the following program fragment:
Integer i = new Integer();
HashTable h = new HashTable();
Object o = m (i, h);
Again, this code is well typed. But if we "beta-reduce" the call to
m, we obtain
Integer i = new Integer();
HashTable h = new HashTable();
Object o = (b ? i : h);
which is *not* well typed: the branches of the conditional now have
the *different* reference types Integer and Hashtable, neither of
which is a subtype of the other.
DISCUSSION
----------
One may wonder how this failure of subject reduction squares with
recent proofs of type soundness for fragments of Java by Drossopolou
and Eisenbach [2] and Nipkow and XXXXXXXXXXXXXX [3]. On the one hand,
since these fragments omit the conditional expression form, this
failure does not affect the validity of their results, per se. On the
other hand, both of these papers use a reduction-based operational
semantics, and therefore, it seems, their proof methods cannot easily
be extended to deal with the full Java language including conditional
expressions.
Of course, it remains intuitively clear that the typing rule for
conditional expressions *is* sound, in the sense that it cannot lead
to unchecked failures at run time. One possible way of formalizing
this intuition is to alter the beta-reduction rule so that, in the
example above, the expression
Integer i = new Integer();
HashTable h = new HashTable();
Object o = m (i, h);
is rewritten as
Integer i = new Integer();
HashTable h = new HashTable();
Object o = (b ? (Object)i : (Object)h);
carrying the parameter types along explicitly during the substitution
operation and thus maintaining the well-typedness of the conditional
expression.
CITATIONS
---------
[1] Gosling, Joy, and Steele, The Java Language Specification, Addison
Wesley, 1996.
[2] Drossopolou and Eisenbach, "Java is type safe -- probably," ECOOP
'97.
[3] Nipkow and von Oheimb, "Java_light is type-safe -- definitely,"
POPL '98.