[TYPES] how to typing for logic equality operator

[Philip Wadler]

We dealt with exactly the issue Tillmann Rendel describes in our
design of Featherweight Java.  See quote below. -- P


Featherweight Java: A Minimal Core
Calculus for Java and GJ
ATSUSHI IGARASHI
University of Tokyo
BENJAMIN C. PIERCE
University of Pennsylvania
and
PHILIP WADLER
Avaya
ACM Transactions on Programming Languages and Systems, Vol. 23, No. 3,
May 2001, Pages 396–450.

One technical innovation in FJ is the introduction of “stupid” casts.
There are three rules for type casts: in an upcast the subject is a
subclass of the target; in a downcast the target is a subclass of the
subject; and in a stupid cast the target is unrelated to the subject.
The Java compiler rejects as ill typed an expression containing a
stupid cast, but we must allow stupid casts in FJ if we are to
formulate type soundness as a subject reduction theorem for a
small-step semantics. This is because an expression without stupid
casts may reduce to one containing a stupid cast. ... We indicate the
special nature of stupid casts by including the hypothesis stupid
warning in the type rule for stupid casts (T-SCAST); an FJ typing
corresponds to a legal Java typing only if it does not contain this
rule. (Stupid casts were omitted from Classic Java [Flatt et al.
1998a], causing its published proof of type soundness to be incorrect;
this error was discovered independently by ourselves and the Classic
Java authors).  [p. 405]



On Fri, Nov 19, 2010 at 2:24 PM, Tillmann Rendel
<rendel at informatik.uni-marburg.de> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
>
>



-- 
.\ Philip Wadler, Professor of Theoretical Computer Science
./\ School of Informatics, University of Edinburgh
/  \ http://homepages.inf.ed.ac.uk/wadler/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.