[darcs-users] Re: current status of darcs

[apfelmus at quantentunnel.de]

David Roundy wrote:
> On Fri, Mar 09, 2007 at 07:27:09PM +0100, Juliusz Chroboczek wrote:
>>>  1. The conflict bug.
>> This is the big one.  Nobody knows how to fix it (or they're not saying).
> 
> I believe we do know how to solve it, it's just that it'll be a lot of
> work.  Jason is planning on starting work on that in the spring--but of
> course he'll start out by working on a simulated version.  We talked about
> this after the Haskell workshop in the fall, and I'm quite confident that
> we know what the solution looks like, it's just a question of coding it up
> and figuring how to design a repository format that'll work with it.
> 
> [...] There will be lots of book keeping, but the math
> needed to determine the state of a repository is actually very simple, so
> the main issues should be technical ones (doing so efficiently, how to
> store it on disk, how to determine dependencies interactively when
> prompting for changes, etc).

Disclaimer: I'm an uninformed bystander. But I'm in awe of the miracle
that darcs exists without a really rigorous Theory Of Patches. Alas, the
miracle dissolves rather quickly when noting that The Conflict Bug
haunts darcs for some year(s) now. This gives rise to the following
prophecy: darcs will be haunted until it is crystal clear what the
semantics of patches are.

Crystal clear. Why must the prophecy be true? Well, here's the _proof_:
once the issue is solved, the darcs source code is a fully worked out
Theory Of Patches. QED :)

Please, do not underestimate this, developing a crystal clear Theory Of
Patches is hard. It is far form being a "technical issue" that only
needs "coding it up". For instance, efficiency is an integral part: it's
quite imaginable that the Theory is too general and turns out to be
NP-hard. What if it's interactivity that makes it NP-hard?

I guess E.W. Dijsktra and R. Bird would give the same advice: understand
the problem, find the proofs. Equational reasoning will generate your
implementation for free.

Regards,
apfelmus


PS: Personally, I always wondered whether one could use a bit category
theory for a Theory Of Patches. Patches f : A -> B are arrows between
repositories A and B. Actually, to be able to move them around, they
should be a family of arrows (= a functor) like F : forall a . A a -> B
a, I don't know. The product AxB of two repositories is the last common
repo they developed from. The coproduct A+B is a canonical merge of A
and B. Maybe it's not a merge but it's the disjoint sum with all
conflicts yet unresolved. Then, a conflict resolving patch would have a
family member f : A+B -> C. Can such single arrows be extended to
functors by some universal property? I mean, that's the key point: given
a change f : A -> B between very concrete repos, find a more general one.