[TYPES] how to typing for logic equality operator

[Philip Wadler]

I should note I included that line from the paper not to cast
aspersions on Matthias and co., but to point out that even excellent
researchers can fall foul of these subtleties.  Yours,  -- P

On Fri, Nov 19, 2010 at 5:57 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> 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
>
>
>



-- 
.\ 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.