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

[Eric Kow]

Hi,

Jean-Phillipe: I thought you might be interested in this discussion
and the paper that sparked it

The paper is /A formalization of Darcs patch theory using inverse
semigroups/ by Judah Jacobson

  http://www.math.ucla.edu/~jjacobson/patch-theory/

As for the underlying discussion, I'm adding you because I vaguely
remember GUIDs being thrown around in the Henderson's cafe (Edinburgh
Haskell Hackathon)

If it's too hard to follow the below, please have a look at
  http://lists.osuosl.org/pipermail/darcs-users/2009-October/021970.html

Now...

Eric worried:
>> 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).

On Fri, Oct 30, 2009 at 16:20:52 +0100, Heinrich Apfelmus replied:
> 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.)

Darcs-users: Speaking of toy implementations, here's a tarball for
FoCAL, which I think you have seen but which I'm reposting because it
seemed relevant

  http://www.cse.chalmers.se/~bernardy/focal_Code_Anders_Petter.tar.gz

Jean-Phillipe : perhaps it would be useful to put up a Darcs repository
for that, for example, on patch-tag.com

> 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.

Now that you put it that way, consider me reassured!  Not that I should
have anything to say about what goes into a patch theory.

>> 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/ 
> PrincipledVersionControl.pdf

>>  - 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,  
> though.)

Hunk move patches are just the idea of displacing a block of text within
a file or maybe even to some other file.  But it sounds like this could
be done in such a scheme, and perhaps made simpler? Ganesh was
commenting that it's got tons of cases to consider.

Tree structure editing: I don't know, but there have been people asking
about using Darcs to edit XML files.  So I imagine that operations like
"add a child node here; move this node there; delete this node" could be
interesting.

I'm still hoping that someday in the future we'll see some interesting
specialised Darcs-like tools for doing some notion of
versioning/merging/etc on wacky data, which was why I asked about
patch agnosticism.

Now that you've tackled agnosticism, I have one more question for you,
oh monorail salesman: what about dependencies?  I understand how Darcs
figures out if one patch depends on another (they don't commute).  Would
it be straightforward to have such tracking in a commute-free patch
theory?  I imagine that along with conflict marking this would become a
mere user interface issue more than anything else.  Maybe this would
even make it easy to implement the "breakable dependencies" that some
people keep asking for.  (then again, in a commutation-based scheme,
I guess breaking dependencies would just be creating a conflict and no
more difficult).

Finally: are there any reasons to be GUID-skeptical?  If they really
could give us a better way to think about patches, why do we continue
the line of inquiry into commutation-based merging?  I imagine that one
reason is that (a) because it's known to work (for the most part),
whereas the new scheme would open up whole new cans of worms and that
(b) Ian really has pretty much worked it all out already and it's really
just a matter of hammering out the proofs in Coq.  Is that a close
approximation of the truth?  Is there a deeper story behind this?

Thanks!

Eric

PS.  As you can see, I don't even understand half of the discussion
     here, but I hope I'm at least plugging the right people together...

-- 
Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow>
PGP Key ID: 08AC04F9
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: Digital signature
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20091030/7ad5b7b0/attachment.pgp>