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

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:

> 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 
I 'll think about 2.3 over the week end.


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,