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

[Uday S Reddy]

Derek Dreyer writes:

> Thanks for the clarification, Uday!

My pleasure.  I think syntactic reasoning can be mysterious, and it is only
clarified when we consider semantics.  Consider that a plug for semantics!

> 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.

Once again, syntactic reasoning locks in mysteries here.  The remark
following Theorem 7 provides the only way in PAL to show that two terms of a
an existential type are equal.  So, if you managed to prove that two such
terms are equal in PAL, you would have constructed a trasitive composition
of simulation arguments.  So, the property you want follows as a metatheorem
about PAL.

(If we were givinng a semantics, we would be forced to write that down
explicitly.  But, in a formal system, it is implicit.)

> 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.

That is indeed right.  For closed types, the "only if" direction is trivial.
However, for open types, it is not.  You would notice in Theorem 7 the
additional condition that x and y have to be related by A[S,rho].  That
plays a significant role.

Cheers,
Uday