[TYPES] how to typing for logic equality operator

[Matthias Felleisen]

concerning: Flatt, Krishnamurthi, & Felleisen, Classic Java, POPL'98: 

Phil is correct. We messed up both the statement of the type soundness theorem (typo level omission of the divergence clause) and its proof (not treating these 'casts' properly) in POPL'98. 

Klaus is correct, too. We fixed the system in a TR and some follow-up paper. 

-- Matthias




On Nov 19, 2010, at 12:04 PM, Klaus Ostermann wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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