[TYPES] how to typing for logic equality operator

[Tillmann Rendel]

Derek Dreyer wrote:
> the typing rule for reference equality described in the Java language spec:
>
> http://java.sun.com/docs/books/jls/third_edition/html/expressions.html#15.21.3
>
> There, it explicitly states: "A compile-time error occurs if it is
> impossible to convert the type of either operand to the type of the
> other by a casting conversion (§5.5). The run-time values of the two
> operands would necessarily be unequal."  From what I can tell, a
> casting conversion basically means either an upcast or a downcast.

This rule breaks subject reduction not only technically, but also in 
spirit. The rationale for this rule is to disallow expressions with 
statically known values. But the idea of reduction semantics is to 
incrementally transform an expression into a value, and clearly, the 
value of a value is always statically known. The rationale of this rule 
therefore clashes with the idea of reduction semantics to encode the 
evaluation of a program in a sequence of programs which are more and 
more statically known.


This is similar to other parts of the Java language specification which 
deal with "obviously boring code". For example, javac accepts the 
following sequence of statements:

   if (true) return 27;
   return 42;

But rejects the following:

   return 27;
   return 42;

I would expect a reduction semantics for Java statements to reduce the 
former sequence of statements into the latter, so this example seems to 
break subject reduction, too. And again, javac's behavior is mandated by 
the Java language spec, Sec. 14.21:
> It is a compile-time error if a statement cannot be executed because
> it is unreachable. Every Java compiler must carry out the conservative
> flow analysis specified here to make sure all statements are reachable.


I think these two problems, and all similar ones, are best dealt with by 
considering such static checks not as type checks, but as separate 
static analyses to be performed after type checking. They do not need to 
be modeled in a formal type system, then, and do not contribute nor 
disturb subject reduction. If type safety can be established for this 
smaller type system, it can not later be broken by ruling out some 
so-far well-typed programs by additional static analyses.

So my advice to the original poster would be: Choose a weaker typing 
rule for ==. As long as you can prove subject reduction for that weaker 
rule, your proof also works for the stronger rule actually used in Java 
compilers, if you show that the stronger rule implies the weaker rule.


But from the point of view of language design, I wonder what the point 
of specifying such details in a language specification might be?

   Tillmann