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