[TYPES] how to typing for logic equality operator

[Klaus Ostermann]

2010/11/19 Philip Wadler <wadler at inf.ed.ac.uk>:
>  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]


One should note, though, that the Classic Java type system can be fixed without
using something like stupid casts. As far as I recall, in the
corrected 1999 tech report version
of the Classic Java paper, Flatt et al introduce a dedicated runtime
typing rule for
casts which looks something like this:

e : C
-------------
(D) e : D

Their system is still correct w.r.t the Java typing rules because the
type elaboration
rules are more restrictive than this runtime typing rule.

For more precise runtime typing, one could also annotate the type cast
with the original static type of the expression during type elaboration, i.e.
something like this:

e0 : C   D <: C
-------------------------------------
(D) e0 => (D) e0[C] : D

and then the following runtime typing rule

e0 : C'   C' <: C
---------------------
(D) e0[C] : D

I guess that once the discrepancies between static and runtime typing become
bigger and bigger, it pays off to formalize type elaboration rules
because it is not
clear to me whether this "stupid cast" technique can be generalized to other
techniques such as resolution of method overloading.

Klaus