[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
