[Prev][Next][Index][Thread]
Re: Subject reduction fails in Java
Dear Benjamin,
The subject reduction problem with Java discussed in your message in the
types-mailing list is very interesting. I believe that it is closely
related to the notion of typed reduction we have been studying in our work
on Coercive Subtyping (see, for example, my papers [1][2] for the
description of the framework.)
Java-conversions (the widening conversions) can be regarded as what we
have called "coercions". In the framework of coercive subtyping, if
f:K->K', a:K0, and K0 <_c K (ie, K is a subtype via coercion c), then
f(a) is computationally equal to (reduces to) f(c(a))
In particular, ([x:K]b)(a) does not reduce to [a/x]b, but it reduces to
([x:K]b)(c(a)) (coercion insertion as reduction)
which beta-reduces to [c(a)/x]b. In other words, reductions such as beta
cannot be done directly when the argument's type is a proper subtype of
the required type; instead, a coercion (or type-casting operation, or
conversion in Java's term) has to be inserted (as a step of reduction)
before the reduction (beta in the above example) can be done. I think
this corresponds to the suggestion you have made in your DISCUSSION
section of your message.
I am very interested in this and hope to get your further opinions. Do
you know of other related work that uses the similar ideas to deal with
these situations? (Please let me know if so.)
Best regards,
Zhaohui.
P.S. It is OK for this message to be sent to the types-list if you
think it is appropriate.
[1] Z. Luo. Coercive subtyping in type theory. Proc. of CSL'96, the 1996
Annual Conference of the European Association for Computer Science Logic,
Utrecht. LNCS 1258, 1997.
[Available from URL: http://www.dur.ac.uk/~dcs0zl/SUBTYPING96.ps.gz]
[2] Z. Luo. Coercive subtyping. Submitted to Journal of Logic and
Computation. 1997. To appear.
[Draft available from URL: http://www.dur.ac.uk/~dcs0zl/JLC98.ps.gz]
On Thu, 18 Jun 1998, Benjamin Pierce wrote:
> [------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
>
> 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.
>
>