[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)

Heinrich 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  
>> for
>> understanding the semantics of merges.
>> In other words, thinking about the intricacies of commutation is a  
>> waste
>> 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  
commutation altogether.

(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  
patch laws.

> 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"[1] shows that GUIDs can  
do these.

   [1]: http://www.cse.chalmers.se/~wouter/Publications/ 

>  - 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 mailing list