[darcs-devel] darcs patch: start gadt stuff (and 29 more)

David Roundy droundy at darcs.net
Sun Jun 17 07:24:41 PDT 2007


On Sat, Jun 16, 2007 at 02:40:46PM -0700, Jason Dagit wrote:
> On 6/16/07, David Roundy <droundy at darcs.net> 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


More information about the darcs-devel mailing list