[TYPES] a counterexample to Plotkin and Abadi's characterization of equivalence at existential type?

[Derek Dreyer]

Oh, of course!  I was reading "u = pack X x" and "v = pack Y y" in
Theorem 7 as syntactic equality, when they're really just PAL
equalities, which could themselves be established by simulation
arguments.  So Theorem 7 really allows for u and v, the equivalent
existential packages, to be related by a transitive composition of
simulation proofs, as my "counterexample" demonstrates is necessary.

Thanks for the clarification, Uday!

Having said that, however, now I'm wondering about something else.  It
seems to me that, at least when restricted to closed types (and
possibly more generally), all that the "only if" direction of Theorem
7 shows is that every term of existential type is equal to *some* term
of the form "pack X x".  In particular, it does *not* seem to imply
that equivalent packages are related by a transitive composition of
simulation arguments.

That is, suppose pack B1 b1 = pack B2 b2 : Exists X. A[X] (with A[X]
having only free variable X).  The "only if" direction of Theorem 7
doesn't actually tell us anything (new) about the relationship between
b1 and b2 because there's a trivial solution for the existentially
bound variables on the rhs.  I could have just chosen X and Y to
*both* be B1, x and y to *both* be b1, and S to be the identity
relation on B1.  It's certainly true that pack B1 b1 = pack B1 b1,
that pack B2 b2 = pack B1 b1, and that b1 is logically related to b1
at A[B1].  The first is trivial, the second follows from the
assumption, and the third follows from identity extension.

So, it seems that for existential types, knowing that two package
terms (pack B1 b1 and pack B2 b2 above) are logically related at
existential type does not reveal anything useful about the relation
between the terms inside the packages (b1 and b2 above).  Or does it?
Incidentally, this corresponds to my intuition about equivalence at
existential type, but I was under the impression that Theorem 7 was
stating something stronger.

Now perhaps what I said only applies to closed types A?  I'm not sure,
but it makes me wonder if the simulation condition (the last part of
the theorem that says x and y are related at A[S,eq_Zvec]) really adds
anything in the "only if" direction.

Thanks,
Derek

On Wed, Dec 5, 2012 at 4:05 PM, Uday S Reddy <u.s.reddy at cs.bham.ac.uk> wrote:
> Derek Dreyer writes:
>
>> In short, Theorem 7 in their paper says that two terms of existential
>> type are equal *if and only if* there exists a "simulation relation"
>> between their internal representations of the abstract type such that
>> the operations are logically related at the appropriate type
>> (interpreting the abstract type using the chosen simulation relation).
>
> The Theorem 7 doesn't quite say that.  u = (pack X x) means that <X, x> make
> up *some* representation of the abstract data type u.  X and x have no
> reason to be the same as what you regard as "the internal representation" of
> u.
>
> To put another way, the elements u of an existential type are *equivalence
> classes* of type representations.  The Theorem 7 says that a simulation
> relation exists between two cleverly chosen representatives of such
> equivalence classes.
>
> In my papers, I avoid the notation (pack X x), which is open to
> misinterpretation, and use two separate notations
>
>   <X, x>  -  for representations
>   <|X, x|> - for equivalence classes of representations.
>
> See for instance, "Objects and classes in Algol-like languages", Sec. 5.1.
> http://www.cs.bham.ac.uk/~udr/papers/objects-and-classes.pdf.
>
> Cheers,
> Uday