On Sat, Jun 16, 2007 at 02:40:46PM -0700, Jason Dagit wrote: > On 6/16/07, David Roundy <[EMAIL PROTECTED]> wrote: > > >I hope that's clear. I know it's pretty brief. My implementation actually > >uses unsafeCoerce# internally when parsing Conflicted patches. We could > >have avoided this by storing the inverse of the conflicted patch and its > >context, but it didn't seem worth the change. The code would have been > >more elegant, but I think the patches would have been more confusing. > > Your explanation helps a lot. I think I see the need for Sealed now. > I also see that MyEq could return Sealed EqCheck and avoid the > unsafeCoerce# but it would be overkill.
No, if MyEq returned a Sealed EqCheck then it wouldn't serve its function, which is to prove that two *already-known* types are the same. > I need to think more about the hypothetical change to Conflicted > patches. I'm not sure I understand how that also solves the problem. It would solve the problem because when we read a patch or patch sequence the *initial* state can be whatever we like, it's only the final state that is existential. This was somewhat arbitrarily chosen, but matches with how repositories are stored: we always know the previous state before reading a patch, and only then discover the post-patch state. Note that even this arbitrary initial state still weakens the safety provided by the type witnesses, as someone could read patches out of order, and thus generate an invalid patch sequence. Which is to say that all code that reads patches must be carefully audited. That's already true, and there's nothing that we can do to change that, since only the repository structure (or patch contents) tells us the proper context for a patch, and the type system can't tell us that! -- David Roundy http://www.darcs.net _______________________________________________ darcs-devel mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-devel
