[Prev][Next][Index][Thread]
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
programs.
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