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

[Derek Dreyer]

> As to what you can "do" with the "only if" direction, I don't know.  I was
> assuming that you had some application in mind since you raised this.  The
> "only if" directions are essentially stating completeness of the respective
> proof rules.  So, they could presumably be used to *disprove* that two terms
> are related by showing that all possible ways proving them related are
> exhausted.

What I find surprising and unintuitive somehow is that we have a
theorem which could presumably be used for such "disproving" purposes
only in the case that the types are open, and not in the specific case
when they are closed.  (Off the top of my head, I can't think of other
examples of this phenomenon, but it's early in the morning for me. ;-)

Incidentally, as I wrote before, I don't think the "only if" direction
of Theorem 7 is trivial even in the closed types case: it *does* give
you the "canonical forms" property that every term of existential type
is equal to some "pack X x".  It just doesn't seem to give you
anything else in that case.

Derek

>
> Cheers,
> Uday
>