Re: Subject Reduction in Java -- without joins

> > From: Benjamin Pierce,  Date: Fri, 19 Jun 1998 13:32:34 -0500 
> > ...  a "beta reduction" rule for Java should explicitly cast 
> > the arguments to the parameter types before substituting. 
> This casting is only necessary is order to help the type system,
> and one would not like a real implementation to be performing
> all these checks at run-time. 
> 2.2 How about introducing a special kind of casting that is just a type 
> annotation used for describing types, but is not executed? This 
> would - I suppose - correspond to the THIRD APPROACH as described in
> Benjamin Pierce's message.
> I feel this is better than the normal casts, but still do not like
> entering in the compiled language information that is only necessary
> to support the proof of subject reduction.

I'm away from my copy of the language spec, so please be gentle if I
misremember here.  Widening casts shouldn't actually generate code --
the bytecode verifier has to do the right thing here.  The lack of a
common supertype for multiple interfaces has been independently
rediscovered by lots of folks -- Sophia Drossopoulou was the first to
point it out to me; Ken Zadeck also (re)discovered the problem, and
noted that Sun's JVM does not follow the JVM spec here.  If memory
serves properly, the VM is _not_ required (by the spec) to handle this
case; i.e., the spec says such uses of interfaces are not valid

The widening cast to Object is a particularly interesting special
case, because it is certainly the intention of Java (modulo various
ClassLoader problems) that all objects will be instances of
(sub)classes of Object.  Thus, we _know_ the cast will succeed,
statically.  So it seems like the type-checker needs some information
to handle this, but we don't need dynamic checks.  The question is,
"How does this generalize?"

Drew Dean