[Prev][Next][Index][Thread]
Re: Subject reduction fails in Java
Here is an interesting historical tidbit related to Pierce's message on
Subject Reduction and Java.
I was amused when I first learned (from Wadler and/or Odersky, I believe) that
Java does not fully support subtyping (subsumption, actually) because of the
restrictions on the if-then-else expression (written b?x:y). We ran into this
problem many years ago when proving a subject-reduction theorem for TOOPLE, a
functional object-oriented programming language. The proof depended on showing
that each term had a minimum type. We were quite surprised to find that
the if-then-else expression presented a big problem in that regard because
we could write "if cond then exp1 else exp2" where the minimum types of exp1
and exp2 needed only to have a common supertype.
We resolved the problem by ensuring that every pair of types with an upper
bound has a least upper bound (and because of covariance problems, also a
similar statement with lower bounds). The moral is that seemingly
simple expressions can result in big problems when working with operational
semantics (never dismiss anything as trivial!).
The proof of minimum typing for TOOPLE was given in
Bruce et al, "Safe & decidable type-checking in an object-oriented language"
in OOPSLA '93 proceedings, pp. 29-46.
The actual proof of subject-reduction of TOOPLE can be found in
Bruce et al, "An operational semantics for TOOPLE: A statically typed
object-oriented programming language", MFPS '93 proceedings, LNCS 802,
pp. 603-626.
Kim Bruce