[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.