[Prev][Next][Index][Thread]
Re: Subject reduction fails in Java
Dear All:
Before you jump on Java or the typing rules, you may wish to consider the
*full* context of the discussion.
Java is *not* a functional language. It is an imperative language and, if
we wish to prove all of Java type sound, we should include assignment in
the reduction semantics. Felleisen-Friedman-Hieb (popl 87, tcs 87, 89) have
shown that this strategy is possible. Felleisen-Wright (rice 91/info-comp
94) have shown how to prove type-soundness for core ML. At POPL'98,
Flatt-Krishnamurthi-Felleisen show how to scale this approach to
Java. Proving type soundness of Java + if-expressions using small-step
subject-reduction is then straightforward.
Here is the approximate reduction according to FSF98:
Object m (Object a1, Object a2) {
return (b ? a1 : a2);
}
Integer i = new Integer();
HashTable h = new HashTable();
Object o = m (i, h);
-->
Object m (Object a1, Object a2) {
return (b ? a1 : a2);
}
Integer i = new Integer();
HashTable h = new HashTable();
Object a1 = <Integer,...>;
Object a2 = <HashTable,...>;
Object o = (b ? a1 : a2);
More generally, the FSF approach requires a (minor) elaboration from
surface syntax into core syntax and the rewriting happens on core
syntax. Every intermediate stage can trivially be converted into a running
Java program (we carry along a quasi-store, i.e., we use the Felleisen-Hieb
trick, and it must be converted into definitions). -- The rewriting model
is close to an implementation in that sense, even though it can be read at
the surface syntax model. I do not consider this a plus or a minus of a
model, I simply wish to point out an attribute. Personally I believe a
model should be useful for reasoning in context.
If the question concerns types, please ignore the above remarks and excuse
their length.
Regards -- Matthias Felleisen
P.S. I conjecture that Phil Wadler's example also disappears.