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