[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)
apfelmus at quantentunnel.de
Fri Oct 30 15:20:52 UTC 2009
Eric Kow wrote:
> Heinrich Apfelmus wrote:
>> In any case, I once again would like to stress that it is my
>> belief that
>> commutation is already too complicated to be a suitable foundation
>> understanding the semantics of merges.
>> In other words, thinking about the intricacies of commutation is a
>> of our precious brain cycles. :) They are better spent on a simpler
>> formalization where each line has its own GUID.
> So, one of things I thought was attractive about Darcs patch theory is
> that it seems to be completely independent of the patch types.
> You define patch types, inverse and commutation and the theory takes
> care of the rest (cherry picking, merging, conflicts).
Well, patch theory would take care of the rest if it were as mature
as we'd like to. :-) What I'm saying is that, in my opinion, GUIDs
make building a mature theory much easier because they eliminate
(My litmus test for maturity of a theory is that I can read it up
somewhere and implement my own toy darcs, just like I can implement
my own toy lambda calculus or my own toy type inference, for example.)
Being agnostic of patch types sounds great, but neither do I expect
GUIDs to be less agnostic, nor is Darcs patch theory as agnostic as
it may sound. The thing is that the commutation operation has to obey
a lot of rules ("patch laws"), some of which are collected in Judah's
paper and some of which are hitherto unknown, and if you introduce a
new patch type, it might just not be possible to make it obey the
> Right now the kinds of primitive patch Darcs knows about:
> - hunks (the most obvious)
> - add A, remove A, adddir D, rmdir D (book-keeping, perhaps)
> - move A B
The "Principled Approach to Version Control" shows that GUIDs can
> - replace tok1 tok2 (not everybody likes this)
Not sure about this one, but I think some weaker form can be done
with GUIDs as well, for example by lexing the whole file and giving
every token a unique GUID.
> Some things people have asked for:
> - char hunks
Every char gets its own GUID...
> - hunk movement
> - some kind of tree structure editing
What are these? But yes, there might be patch types that cannot be
formulated in terms of GUIDs. (Not sure whether this is a problem,
More information about the darcs-users