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

[Uday S Reddy]

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