[darcs-users] Theory of Patches

Jason Dagit dagit at codersbase.com
Thu Apr 9 22:42:39 UTC 2009


On Thu, Apr 9, 2009 at 3:26 PM, Daniel Carrera
<daniel.carrera at theingots.org> wrote:
> Hello,
>
> I posted to darcs-devel but apparently the two lists have merged. So let's
> see... I have two questions:

Welcome!

> 1. Where can I learn more about the theory of patches? I already read
> the manual page (http://darcs.net/manual/node9.html). I have a math
> background, so a research paper is fine.

My recent M.S. thesis covered darcs witness types.  It focuses on our
witness types, but chapter 3 provides an alternative overview of patch
theory, sorry no proofs though.  You can find a copy of my thesis
here:
http://files.codersbase.com/thesis.pdf
and some slides:
http://files.codersbase.com/thesistalk.pdf

You might also find it interesting to read about camp, which also uses patches:
http://projects.haskell.org/camp/
and
darcs get http://code.haskell.org/camp/devel/paper/

Just take a good look at the camp website as there is some work in Coq
and other interesting things.

> 2. Do patches have an internal representation that is context independent?

Short answer: Yes and no.

Detailed answer:
Yes:  There are no values in darcs that correspond to context.
Specifically, context is tracked implicitly.  Our witness types do
carry context information, but they are implemented as phantom types.
A phantom type is just a type variable with no value associated with
it.  So, in this sense the "representation" of a patch is independent
of the context.

No:  When you commute two patches sometimes the representation of the
patches changes (see Chapter 3 of my thesis for an example).  One
could argue that the reason it changed is because the context is part
of that representation.  Additionally, we could track patch context
dynamically as we manipulate patch sequences.  This could potentially
have a huge negative impact on performance.

I hope that answers your questions,
Jason


More information about the darcs-users mailing list