[TYPES] how to typing for logic equality operator

[Klaus Ostermann]

Hello all,

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

I believe that the original poster's problem of formalizing Java's
equality operator and
also the examples Tillmann gave (and many more examples, such as the resolution
of method overloading or Java's "? : " operator) call for a more
sophisticated style of formalization, namely one
with type elaboration rules which transform the program during type
checking into
a form suitable for runtime type checking. Type elaboration rules
allow one to have
a kind of two-stage type system where one can still cleanly formalize
subject reduction.

A good example for such a semantics that fits to the intention of the
original poster would be
Felleisen et al's "ClassicJava" formalization in their POPL'98 paper
on "Classes and Mixins".

For instance, for the "==" operator, the type elaboration rules could
type-check and annotate the equality operation as follows:

e1:T1  e2:T2    T1 <: T2
----------------------------------------------------
e1 == e2  => e1 ==[T2] e2 : Bool


e1:T1  e2:T2    T2 <: T1
----------------------------------------------------
e1 == e2  => e1 ==[T1] e2 : Bool

and then the "runtime" typing rule would be


e1:T1   e2:T2    T1 <: T    T2 <: T
----------------------------------------------------
e1 == [T] e2 : Bool

Klaus