[Prev][Next][Index][Thread]
Re: Subject Reduction in Java -- without joins
I feel that we all agreed so far, that conditional expressions
as defined in Java now
1) do not satisfy subject reduction for small step semantics
2) do not create any possibility for breaking the
type system, so are not a serious threat to soundness of the type
system
Therefore, as well as thinking about improving the language
definition, it is interesting to try to formalize the situation as is
and prove soundness.
I see the following alternatives:
1) Use large step semantics -- I believe that the Nipkov/vonOheimB
proof could be extended to describe conditional expressions without
any problems.
2) Some variation of the idea that the language executed is an
"enrichment" of the original language (e.g. enriched by signatures in
the case of method calls). More about this later on.
I feel that an interesting lesson is, that oo languages may
be sound even if they do not satisfy the "OO polymorphism property"
or "substitution property".
> If an expression e is soundly typed under the assumption that
> variables X1,...,Xn have type T1,...,Tn respectively, then it
> is soundly typed under the assumption that X1,..., Xn have
> types T1', ..., Tn' respectively, where each Ti' is subtype of Ti.
Now, in more detail, about alternative 2:
2.1
> 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.
2.3 Another suggestion would be to allow expressions of the run-time
language to have many types, and to reformulate the "OO polymorphism"
and subject reduction properties accordingly.
2.4 The last idea is to restrict syntactically the language under
consideration and allow conditionals to appear only after assignments
-- thus the type of the left hand side plays the role of the type
annotation in suggestions 1 and 2.
More details on 2.3
-------------------
1) For the original language type rule for conditionals
remains as is
2) For the run-time language the type rule for conditionals is
b : bool e1:E1 e2:E2
E1 < T E2 < T
-----------------------------------------
(b?e1:e2) T
that is, the conditional may have many types.
3) The "OO polymorphism property" is modified to say that:
If \Gamma, X1:T1, .. Xn:Tn |- e : T
then, for T1', ..., Tn', where each Ti' is subtype of Ti,
there exists a type T'', such that
* \Gamma, X1:T1, .. Xn:Tn |- e : T''
* \Gamma, X1:T1', .. Xn:Tn' |- e : T'
* T' is subtype of T''
In other words, substitution preserves _one of the types_ of
the expression e.
3) The subject reduction theorem also has to be modified to say
If \Gamma |- e : T, and e non-ground, then
then, there exists a T', T'', e' such that
1. Case * e rewrtites to e'
* \Gamma |- e : T''
* \Gamma, |- e' : T'
* T' is subtype of T''
2. Case an exception was raised
4) The soundness theorem then says that
If |- e : T in the original language, then execution
of the term will produce value of a subtype of T
(remember that types in the original language are
unique)
I 'll think about 2.3 over the week end.
Now,
More on details on 2.4
-----------------------
This seems more straightforward.
1. require conditional expressions to appear only after
assignments, something like a conditional assignment
operator, which may only appear as
as statement = ? : ,
e.g. x = ( b ? e1 : e2 )
where x is any variable, and b, e1, e2 any expressions
2. In Java_SE require for
x = ( b ? e1 ? e2 )
that b is boolean; e1, e2 have such types that one can
be widened to the other; the types of e1 and e2 can be
widened to that of x
3. In Java_R we only require for
x = ( b ? e1 ? e2 )
that b is boolean; the types of e1 and e2 can be
widened to that of x
4. We can then prove the subject reduction theorem
The syntactic restriction does not really restrict the expresive
power of Java, since it only requires the introduction of
local variuables to transform any Java program inbto one that
satisfies the restriction
===============================================================================
Have a nice week-end,
Sophia