[TYPES] how to typing for logic equality operator

[Derek Dreyer]

Interesting.

I believe the original poster's rule

>> e1 : T1  e2 : T2  T1 <: T2 || T2 <: T1
>> --------------------------------
>> e1 == e2 : Bool

corresponds precisely to 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.

The rule Daniel suggests:

> e1 : T1  e2 : T2  T1 <: T  T2 <: T
> ----------------------------------
> e1 == e2 : Bool

would allow pretty much any equality test to typecheck by choosing T
to be Object.  So that doesn't correspond to Java typechecking.

However, the original poster had a point about substitution.  As far
as I can tell, the substitution theorem A.14 on page 532 of Pierce's
TAPL book ceases to hold in the presence of the first equality rule
above.  The theorem states roughly that:

If G, x:B |- t : D and G |- s : A, where A <: B, then G |- [x->s]t : C
for some C <: D.

The issue is that [x->s]t has type C for some C <: D, but does not
have type D itself, due to the lack of an implicit subsumption rule in
FJ.  Thus, if we try to prove this theorem for the first equality rule
above, we get stuck because:

[x->s]e1 : T1' <: T1
[x->s]e2 : T2' <: T2
T1 <: T2 || T2 <: T1

but we have no reason to believe that T1' <: T2' || T2' <: T1', which
is what we need to show.  (Incidentally, substitution works fine for
Daniel's rule.)

So it seems to me the original poster was asking a good question.  One
can easily turn the failed proof above into a counterexample to
subject reduction.

Derek


On Fri, Nov 19, 2010 at 2:18 AM,  <wagnerdm at seas.upenn.edu> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Well, this rule looks a bit strange:
>
> Quoting ??? <is99zcp at hotmail.com>:
>
>
> I would expect something along these lines instead:
>
>
> Does this rule have better substitution properties? If not, can you briefly
> describe examples of a well-typed term (using either rule) and a
> substitution that breaks the typed-ness? (I'm not even sure I understand why
> the rule you proposed doesn't work.)
>
> ~d
>