Talk:Understanding darcs/Patch theory

From Wikibooks, the open-content textbooks collection

Contents 1 Talk about the things in the book 1.1 An unasked for two cents 1.1.1 Vegas 04:58, 11 March 2007 (UTC) 1.2 Other stuff 2 Answering questions 3 Admin stuff 4 Category Theory Musings 4.1 What is a category? 4.2 An attempt at the complete reformulation 4.2.1 A category of repositories and patches 4.2.2 Required additional structure 4.2.3 Properties that follow 4.2.4 Examples encoded in the new formalism 4.3 Loose remarks documenting the process of reformulation

[edit] Talk about the things in the book

The file Darcs-complex-undo.png has a typo in it and needs to be changed. I'm not really up with my MediaWiki skills, that's why I didn't do it. Anyway the bottom says B-sub-1, A-sub-1, and A-inverse. It should say B-sub-1, A-sub-1, and A-sub-1-inverse. -- jared jennings 01:37, 27 September 2007 (UTC)

Thanks! Fixed. -- Kowey 03:51, 27 September 2007 (UTC)

[edit] An unasked for two cents

[edit] Vegas 04:58, 11 March 2007 (UTC)

Hey there. I just wanted to speak out a little bit in favor of your utilizing the same notation as the darcs documentation. I think that your exposition is a good bit clearer, and provides better examples of the various operations of the patch algebra. However, I think that your inversion of the composition operation ala FOSDEM 2006 is a little hinky, and complicates things for people who are going to be going back and forth between your stuff and the official documentation. Of course, as things stand, anyone who's going to even know that darcs exist probably has the cognitive firepower to switch back and forth betweeen the notations, but that may change.

Hi, thanks for your feedback! It's worth considering, especially since David seems to have abandoned the conflictors approach for something rather quite different anyway. I don't have time to look into it; maybe you'd be willing to put up an in progress banner of some kind and fix it? Perhaps discuss it with Arjan first. Best, -- Kowey 07:13, 11 March 2007 (UTC)

Oh, and you'd probably want to look into Ian's writeup which is much more down to business and probably clearer than what I've come up with :-) -- Kowey 07:15, 11 March 2007 (UTC)

[edit] Other stuff

This one:

One more important detail to note though! Context tells us why we can't simply flip AB into BA, but it does not mean that commutation itself depends on context. Whether or not AB commutes to some B1A1 is completely independent of the context that AB is in. Indeed, when we do the commutation, we get a composed patch which brings us from the same starting context to the same ending one. So, if we have {}^x{A^{z_1}}{B^y} (AB takes us from context x to y via z1), then commutation would give us {}^x{{B_1}^{z_2}}{{A_1}^y}. Either case, we go from the original context x to the final context y

seems hard to understand for me. Perhaps it's out of place at this early spot, anyway?

--Mikon

Thank-you very much for pointing this out! I have rewritten this paragraph. Is it clearer now? -- Kowey 17:10, 18 October 2006 (UTC)

Thank you for making me feel needed. :) This paragraph seems more concrete now, but I will not understand it fully until I reformulate all this stuff in term of category theory (a perversion of mine). Then I will comment some more in a mortal-understandable language. --Mikon

I find the definition of commutation imprecise. Could you please answer the questions in point 15 in the "Loose remarks" section below? I also find the first excercise unclear: am I to say what the result of applying B_1 to the file (which file?) should be or what the diff unfified format of B_1 should be, or what? A_1 is described in a way I don't quite know how to follow ("It adds "beer" to line 3 of the shopping list"). I guess sometimes a diff listing would be easier for me to understand that pictures with a natural language descriptions...

Hmm! I think this is worth a post on the darcs-conflicts mailing list.

For now the only use of my reformulation is that I understand much more of the theory and I know at which points I get lost in the descriptions and why (BTW, one of the reasons is surely that I'm yet to install darcs for the first time or see an actual darcs patch (are they just some diff outputs?) or read a darcs user manual of any kind). However, at some point the reformulation may (or may not) give something for free, like a category theory lemma applied to category Repo giving an interesting patches property for free, or an elegant proof of such, or some systematization or a natural class of extensions.

I'm unfortunately not a very mathy guy and not much of a computer scientist at that, but I have added the category theory reformulation to my reading list and will get back to you!

You are brave! :) But I really don't intend to force anybody to learn category theory to be able to undestand me, so let me translate point 15 back to your language and let's see if the answer is simple to provide then:

the commutation of patches X and Y seems to be described in the text as the existence of such X' and Y' that: for each starting context o, XY appplied in this context produce the same file contents as Y'X', X the same as X' and Y the same as Y'; is it correct? Or is the context o actually fixed in some of the equalities (then it's easier to find a commutation), e.g. we only need to find X' and Y' for one particular o?

I guess an example or two would answer my questions, but between me and the examples there is the paragraph I complained about at the top of this page. I guess a part of this paragraph may end up in the definition of commutation and a part is totally trivial once the definition is precise, so I'll stop here and wait to see what happens. :) (Writing mathematical texts is a nightmare and I know what I'm talking about.)

Incidentally, one of my more mathy friends was really excited for a couple of days, trying to formulate patch theory in a sequent calculus (uhh... I think that's what he said), but then he got bored and wandered away.

Interesting. An operational semantics (big steps) for the patch transformations? Or some logical calculus for reasoning about patch relations? Both are a bit too unstructured and untyped for my taste...

For the exercise, I was expecting a natural language description, like patch B_1 adds beer to line... X of the file. Perhaps I should just reformulate it "to what line of file shplst does patch B_1 add beer?". Another problem is that I don't really define "add to line X". Perhaps "insert before line X" would be better. -- Kowey 05:40, 19 October 2006 (UTC)

Really great ideas (X is a number, I presume?). Let me see if I now understand the excercise... Yes, now I get it and I can even solve it. :) (BTW, I find myself knotting my tongue on "shplst" whenever I encounter it, perhaps "shop.lst" or better just "shop_list" would be acceptable for you?) --Mikon

(Resetting indents). Thanks for the idea. I'll use something like "s_list" so that it will fit.

Also, context is irrelvant for commutation. You should be able to commute (or not) any two patches based only on the information within the patches themselves.

OK. That clarifies things a lot. I'll try to understand the definition and the subsequent remark again, now.

As for X and X' being the same,

I meant: "X appplied in any context produces the same file contents as X' applied in the same context" --- quantification by contexts again. And a similar question for Y and Y'. (I see that in the example just after the definition of commutation, X' is exactly equal to X, while Y' produces different file contents than Y, for most arguments. But if we change the format of patches in that example from "put pasta after line 5" to "put pasta after cookies" then Y' is equal to Y. Hmmm. What would be the case is real darcs?)

it depends on your perspective. I assume you mean modulo the effects of commutation (line number, file name shifts, etc), in which case, yes.

I meant the weakest of the common equalities of function-like objects, the so called extensional equality. I ask if the two operations (patches) give the same effects for the same arguments (file contents). I do not ask about equality of textual representations of the operations (e.g. diff outputs). I'm well aware the representations are likely to be changed all the time. Anyway, I want to know what "are intended to perform the same change" precisely means. --Mikon

Finally, regarding my math-friend's work, I do not have any idea whatsover. I saw inference rules and big gammas, but don't remember what he was getting at. Perhaps now that I understand patch theory better, I can see better what he was aiming for, but for now I can only shrug my shoulders. (That being said, I would tend to lean to the latter more than the former) -- Kowey 17:07, 22 October 2006 (UTC)

The section "The complex undo revisited" suggests the commutation is really about finding such Y' that XY is extensionally equal to Y'X and that's all (gives the same results in all contexts). This is a totally different mathematical operation, but it's precisely defined and it's possible to perform more often. I probably miss something, because I cannot deduce anything else about commutation from all three chapters about patch theory. --Mikon

I think calling the result context "ab" in section "Parallel patches" is misleading --- it looks like two context composed; "c" may be a better idea. Point 4. of section Performing the merge is hard to understand for me (in particular, "these patches" is hard to dereference). In point 5. it may be worthwile to expain that "ditching" is doable just as a sequential composition with B_1 --- it is not yet another patch manipulation operation (in general, "ditching" (or factorization) is nontrivial in algebras, categories, optimizing compilers, optimizing source code management systems, etc.). --Mikon

The claim that merging is symmetric does not follow either from the original construction, which uses the imprecisely defined "commutation" notion, nor from my (currently abandoned) construction, which uses a weaker (probably) notion. Or perhaps the symmetry of merging is not a property of the construction but an assumption on the form of patches, just as the existence of reverse patches? --Mikon

As far as I can tell from section "Forced commutation" the forced commutation of X and Y is just X and Y. What am I missing? If I'm right, why not just say that? --Mikon

Sorry, I keep meaning to answer your questions (and then wandering off and forgetting about them). Perhaps you should start interacting with the guys on the darcs-conflicts list? That might be a more comfortabel venue for this :-) I'll re-read your questions later and get back in the meantime. -- Kowey 17:25, 28 October 2006 (UTC)

No problem. Thank you again for the wikibook. When I have something ready I will start advertising. :)

For a more formal description of the things in this section of the book see also: [[1]]. And there's an alternative definition of patch theory using multisets of immutable patches here: [[2]]. I don't know enough of category theory to make any comments but above links might be helpful material to compare with. -- arjan

Thank you! Wow, you are, presumably, the guy who adds beer to shopping lists! :) The server of the first link is currently down, but the authors of the second link seem like they would know what they are doing. This theory is more difficult than I thought. Every two-line categorical definition I throw at it ends up short of capturing the behaviour of Darcs (as I guess it works). If I had some more time this might actually get quite interesting. Anyway, time to try three-line definitions... --Mikon

OK, the server in the first link now works --- nice paper, too... --Mikon

[edit] Answering questions

Hi, here are mostly non-answers to your questions in case you're interested. You've probably got what you need from the paper, but here's my take, just in case. Note that I probably will not be able to answer any more, judging from my inability to keep up with my previous promises! Perhaps Ian would be willing to help.

1. What does "intended to perform the same change" precisely mean?
   • The idea of XY and Y'X' being extensionally equivalent (where ) sounds right. Informally, if you unrecorded Y and X and then re-recorded it into one big patch Z, this patch would be exactly the same as if you had unrecorded X' and Y' and re-recorded that.
2. The claim that merging is symmetric does not follow either from the original construction, which uses the imprecisely defined "commutation" notion, nor from my old constructions, which use a weaker (probably) notion. Or perhaps the symmetry of merging is not a property of the construction but an assumption on the form of patches, just as the existence of reverse patches?
   • Sorry, sort of a non-answer here. For merging, all we say is that AB' performs the same change (see above) as BA', where and . Surely we can work something out from the notion of commutation. Perhaps there is some missing link re: how inverse patches are supposed to behave wrt to commutation? Some relationship between A' ^{− 1} and A ^{− 1}'
3. As far as I can tell from section "Forced commutation" the forced commutation of X and Y is just X and Y. What am I missing? If I'm right, why not just say that?
   • Hmm... that does sound right. I guess the reason is just to keep in mind that Y' is still "supposed" to be Y and X' is supposed to be X even if their effects are quite the opposite. Can't help you here. I need to learn this stuff better, myself.

Sorry, I'm going to have to throw my hands up here and leave the discussion to the more mathematically minded. Am going to read Ian's paper. Best wishes.

-- Kowey 16:38, 14 November 2006 (UTC)

Thank you very much for the answers. I've only skimmed the two papers, searching in vain for category theory inside. I may some day compare their results to mine (when I have any), but for now I think I've grasped enough understanding from the examples in your book to be able to formalize this myself.

I think my questions show what a mathematically-minded person may have trouble with when reading about patch theory. If the troubles are in the theory, in its language or just in your book is still unclear to me. During the time I've spent on reformulation I've learned that the patch interactions are by far not trivial, despite my first impression, so indeed often the only thing one can say is "any operation with the following properties is called commutation/inverse/merge/etc." and not "we define commutation (inverse/merge/etc.) of patches A and B to be the following...". Not only I failed to provide constructions for many notions, but I even failed to uniquely determine them by axioms. And quite possibly this is just how it has to be.

I guess the mixup between "axioms" and "definitions" may be the main problem with this book and some earlier descriptions of patch theory. Mathematically-minded persons are inclined to read "definition" and "uniquely determined" even between the lines, so they really need a clear statement at the beginning that you only describe important properties of a particular construction (code), in the hope the properties will hold also for others. Also, any use of the word "definition", unless it's really a definition (a description that uniquely determines a mathematical object), should be avoided.

After all, I think the pictures you have in your presentation are a good idea, perhaps with a change in their descriptions from "add to line X" to "insert before line X". Also, a single example of a Darcs patch file head to head with a picture would be helpful (though probably earlier in your book you already have one). Thank you again. Frankly, if I were you, I'd stop writing these chapters, until there is something stable to write about. :)

--Mikon 15:13, 15 November 2006 (UTC)

[edit] Admin stuff

Oh by the way, i have updated the diagrams/text to incorporate your advice re: shplst and ab context; also, i think i am going to postpone learning about your work below until you're somewhat satisfied with it. Speaking of which, you might consider creating a wikibooks account just so that your contributions are attributed -- Kowey 16:38, 14 November 2006 (UTC)

[edit] Category Theory Musings

(Category theory nerds only, the occasional mathematics foundations or computer science foundations specialist will be tolerated.)

If you do not mind I will reserve this part of the discussion page for a reformulation of the patches theory in terms of category theory, which seems necessary for me to understand this. Let's hope it will prove any better than a pure set theory approach... Please comment using indents inside the text or using item numbers at the end of this page. --Mikon

Unfortunately, I won't have time to work on this in the foreseeable future, so a few parting thoughts: 1. Unfortunately the categorical reformulation does not work so far (see the TODOs, and much more is needed). 2. The reformulation would be much easier for a system like A Principled Approach to Version Control, which is strict and 'constructive' instead of axiomatic. 3. The elegance of category theory aside, my main goal was to systematically construct the semantics of the patches theory, as opposed to the original ad-hoc axiomatic approach. So A Principled Approach to Version Control beats me to it, though for a significantly different theory. 4. Perhaps, since we don't describe the quantum mechanics or any other given physical system that holds us hostage, it would be wiser to change the Darcs code to fit an elegant, strict, carefully constructed theory, instead of trying to formalize and prove properties of such a complex and changing system as the current Darcs? 5. See Darcs Patch Theory (more or less) for what I mean by 'complex system'. I suspect only a quarter of this complexity is inevitable, which is still impressive. 6. So Long, and Thanks for All the Fun. --Mikon (talk) 18:23, 1 January 2009 (UTC)

[edit] What is a category?

Before I describe the category of patches, here is the definition of a category (somewhat edited part of the Wikipedia article at http://en.wikipedia.org/wiki/Category_%28mathematics%29#Definition).

1. A category C consists of
   • a class ob(C) of objects:
   • a class hom(C) of morphisms. Each morphism f has a unique source object a and target object b where a and b are in ob(C). We write f: a -> b, and we say "f is a morphism from a to b".
   • for every object x, a morphism id_x : x -> x called the identity morphism for x.
   • for every three objects a, b and c, a binary operation hom(a, b) x hom(b, c) -> hom(a, c) called composition of morphisms; the composition of f : a -> b and g : b -> c is written as f;g (some authors use other notation).
2. such that the following axioms hold:
   • (associativity) if f : a -> b, g : b -> c and h : c -> d then f ; (g ; h) = (f ; g) ; h, and
   • (identity) for every morphism f : a -> b, we have id_a ; f = f = f ; id_b.
3. Examples of categories (from the same Wikipedia article):
   • The category Set of all sets together with functions between sets, where composition is the usual function composition and identity is the identity function.
   • The category consisting of all groups with group homomorphisms (this is a subcategory of Set, in particular composition and identity is the same as in Set).
   • Any monoid (algebra with a composition and identity operations, e.g., the monoid of character strings with string concatenation and empty string) forms a category with a single object x (e.g., the set of all strings). The morphisms from x to x are precisely the elements of the monoid, and the categorical composition of morphisms is given by the monoid operation.

[edit] An attempt at the complete reformulation

[edit] A category of repositories and patches

1. Repo is a category representing repositories and patches. It is a subcategory of Set (at least until we need to add some additional artificial morphisms) and has some additional structure and properties we will formally present below. We will call the objects of Repo repos (from "repositories") and we will call the morphisms of Repo patches (they are abstractions of context-less patches of Darcs).
2. a repo that belongs to ob(Repo) is the set of all possible states of a repository (the states are determined by contents and permissions of files and directories which exist in the given repository, etc.); for simplicity we identify single-file repositories with files, etc.; we often abbreviate "set of all possible states of file N" to "N", etc.
3. patches that belong to hom(Repo) are functions between sets of states. Not every such function needs to belong to hom(Repo) (that is, the category needs not be a full subcategory of Set), e.g. we may want a Repo modelling only repositories with hunk patches. The domain of a patch is the domain of the function (e.g. the set of states of a file it "reads" the contents to be changed from); the codomain of a patch is the codomain of the function (e.g. the file it "writes" the modified contents to).
4. As in all subcategories of Cat, identity in Repo is the identity function and the composition f ; g of two patches f and g is the composition of functions (applying patch f first and then patch g).
5. Just by Repo being a category we have the following properties:
   • patch composition is a function (the result of applying a patch depends only on the starting repository state)
   • patch composition is associative (compacting consecutive patches into a single patch does not change the outcome repository state)

---

Comments:

It seems to me that with definition 2, Repo contains only a single element since given any set of files, permissions etc. there is a morphism that maps it to any other set of files, permissions etc. Nullstring (talk) 18:32, 9 January 2008 (UTC)

Bad wording on my part. Thanks, fixed.

For example, there is a patch that maps version 2.6.1 of the Linux kernel source code to version 2.0.1 of the Firefox source code.

Yes, it is a function between the set of all states of files and directories as in kernel 2.6.1 and the set of all states of files and directories as in Firefox 2.0.1. The function can be applied also to some other versions of the Linux kernel, but only the very close ones, where no files and directories are added or removed.

If I'm correct here, then either the set of morphisms is trivial, or ob(Repo) should really contain repository states rather than sets of repository states.

Nope, that would be too limiting. My idea was half-way between that and one huge object containing everything: for each directory and file structure you have one object that contains every possible state of files and directories (and whatever else is a part of the repository).

Another way to go (which I haven't thought through) might be to have ob(Repo) consist of pairs (product, repo) so that repository states are tied to the products they represent. This maps well to the way we use repositories, but I don't know how well it maps out mathematically. Nullstring (talk) 18:32, 9 January 2008 (UTC)

Unfortunately I don't know (or remember) what 'product' is (and I use the term for a different, standard concept below). Anyway, I don't think such small objects would be useful and one of my aims was to abstract the context of patches so that they are applicable when reasonable, instead of always (as a standard diff output is, though you may get an error) or only for a particular single snapshot of a repository, as Darcs patches are (sometimes) defined. My choice of the "reasonable" circumstances was when the structure of the repository agrees (the directory and file structure, etc.). --Mikon (talk) 19:35, 1 January 2009 (UTC)

[edit] Required additional structure

1. Repo has finite products (patches can read from many files, directories and produce the state of many aggregated repos). In particular, Repo has a product of the empty family of repos, which is called a terminal object 1. The terminal object can be imagined as a file that is guaranteed to be always empty (say, /dev/null; in fact any permanently unmodifiable file or directory would do, since it has a one-element set of possible states). For any repo b there is exactly one patch !_b : b -> 1 --- the patch that reads the contents from repo b and writes nothing to 1 (but does not change b). A particular state of a given repository a can be represented as a patch o : 1 -> a that reads from /dev/null and produces at once a fully determined state (contents, etc.) of a.
2. A concrete inverse of patch f : a -> b in context o : 1 -> a is a patch g : b -> a, such that o ; f ; g = o. Concrete inverses always exist; for example, the morphism !_b ; o (the constant function always giving the element represented by o) is a concrete inverse for any f in context o. A right inverse of f : a -> b is a patch f^r : b -> a such that f;f^r = id_a. If a right inverse of f exists, it is also a concrete inverse of f in any context. The concrete inverses have no role in our subsequent definitions, but they are quite important for source control.
3. A merge of a pair of patches f : a -> b and g : a -> b is a pair of patches f': b -> b, g': a -> a such that f ; g' = g ; f'. The patch f ; g' is then ambigously called the merge morphism, or just the merge. For example, any manually chosen repo state s : 1 -> b gives rise to a merge f ; !_b ; s = g ; !_b ; s.
4. (TODO: Verify for hunk patches.) We call a merge of f : a -> b and g : a -> b the most general merge and denote it's components m1(f, g): b -> b, m2(f, g): b -> b and the corresponding merge morphism m(f, g) : a -> b, iff for every merge f', g' of f and g:
   • (*) there exist h1, h2 : b -> b such that f' = m1(f, g) ; h1 and g' = m2(f, g) ; h2
   • (**) and for any h1, h2 : b -> c, if m1(f, g) ; h1 = m1(f, g) ; h2 then f' ; h1 = f' ; h2 and if m2(f, g) ; h1 = m2(f, g) ; h2 then g' ; h1 = g' ; h2.
5. If the most general merge of f and g does not exist, we say that there is a conflict between f and g or that f and g are conflicting patches.

[edit] Properties that follow

1. If g is a concrete inverse of f in context o then f is a concrete inverse of g in context o ; f ("an inverse of an inverse is the original"). Proof: we have to show that (o ; f) ; g ; f = o ; f. This trivially follows from g being the inverse: o ; f ; g = o.
2. TODO: The most general merge is unique. Proof: let f1, g1 and f2, g2 be the most general merges of f and g. From (*) we know that there are h1, h2 such that f1 = f2 ; h2, f2 = f1 ; h1. So f1 = f2 ; h2 = f1 ; h1 ; h2, so by (**) f2 = f2 ; h1 ; h2, so f1 = f1 ; h1 ; h1 ; h2 ; h2. Hmmm, too weak? Oops, I don't use the fact they are merges... I need some more examples.
3. The most general merge of a pair of identical morphisms is a pair of identities. Proof: let the merged morhism be called f. Obviously the pair of identities is a merge of f, f. Let f', g' be a merge of f, f. For (*) put h1 = f' and h2 = g'. For (**) notice that id_b ; h1 = id_b ; h2 implies that h1 = h2 and so f' ; h1 = f' ; h2 and similarly for g'.
4. The most general merge operation is not symmetric, but if f', g' is a merge of f, g then g', f' is a merge of g, f and analogously for the most general merges. Proof: the corresponding definitions are invariant under the exchange of f for g and f' for g' and m1(f, g) for m2(f, g).
5. The relation of not having a conflict is reflexive and symmetric, but not transitive. Proof: two of the above facts and an easy example.
6. TODO: the most general merge operation is associative
7. TODO: a merge of a composition is ...

[edit] Examples encoded in the new formalism

In our examples let us fix a one-file repository and focus on hunk patches, that is patches adding or removing lines (given by line number and content) and acting as identities if that cannot be done.

1. Two different patches (repository imports, rather) f, g : 1 -> b need not be in conflict. For example, if there are only two morphisms from b to b in the Repo at hand: identity and h = 1_b ; f : b -> b then h, h is the only merge and so the most general merge.
2. Let patch f insert line "beer" before line 3 of the file and act as identity if the contents of the file has less than 2 lines. Then f^r that removes line 3 with "beer" in it or acts as identity if such line does not exist, is a right inverse of f. f^r is a concrete inverse of f in all contexts. In Repo with all functions as patches (as opposed to only hunk patches) another concrete inverse of f in context o is the function g, such that g(f(o)) = o and g(x) = x for x <> o. A concrete inverse of f^r in context o ; f, for any context o, is f; a concrete inverse of f^r in any other contexts is the identity.
3. Let g insert line "pasta" before line 5 of the file and act as identity if the contents of the file has less than 4 lines. Let the right inverse of g which is also a concrete inverse of g among hunk patches be called g^r. Note that right inverses of f^r and g^r do not exist. Also, left inverses of g and f do not exist and so inverses of f and g do not exist (the functions are not surjective).
4. The following definition may or may not be useless for our formalism, but we use it in the old examples below:
   • A left conjugation of patch f : b -> b by patch g : a -> b is such a patch l(f, g) : a -> a that g ; f = l(f, g) ; g. A right conjugation of patch f : a -> a by patch g : a -> b is such a patch r(f, g) : b -> b that f ; g = g ; r(f, g). The conjugations needn't be unique, so we assume a choice of them for our notation. Note that if a left inverse g^l of g exists then l(f, g), as well as r(f, g^l) exist (e.g., g ; f ; g^l) and if g^r exists then r(f, g), as well as l(f, g^r) exist (e.g., g^r ; f ; g). However, if the inverses do not exist, the conjugations may exist nevertheless.
5. l(g, f) and r(g, f^r) exist and insert line "pasta" before line 4, l(f, g) and r(f, g^r) do not exist (adding "pasta" would be done at a wrong line), r(f, g) and l(f, g^r) exist and are probably unique: g^r ; f ; g, r(g, f) and l(g, f^r) may be set to be equal to f^r ; g ; f, but can also be chosen to just insert "pasta" before line 6 --- both choices are good for the merge. The result of m(f, g) has "beer" as line 3 and "pasta" as line 6. So, then m(f, g) = f ; r(g, f) = g ; f (but g ; r(f, g) is wrong!).
6. We now try to merge f^r and g^r. The composition f^r ; g^r results in lines 3 and 6 of the original file removed (if both contained "beer") and g^r ; f^r results in lines 5 and 3 removed. Intuitively the latter is m(f^r, g^r). Since the left inverse of g^r is g, we can set l(f^r, g^r) = g^r ; f^r ; g and l(g^r, f^r) = f^r ; g^r ; f, but neither seems helpful for the merge. r(f^r, g^r) does not seem to exist ("pasta" is possibly removed from wrong line and cannot be just readded because it might have been absent from the original file), r(g^r, f^r) removes "pasta" from line 6 (and seems to be unique). So m(f^r, g^r) = f^r ; r(g^r, f^r) = g^r ; f^r.
7. Let f' insert line "beer" before line 10 of the file and act as identity if the contents of the file has less than 9 lines. Let h = f ; f' so that its result has "beer" as lines 3 and 10 (inserted before lines 3 and 9 of the original file). Note that h is no longer a hunk patch. The result of h^r has lines 3 and 10 with "beer" in them removed, if such lines exist.
8. Let us try to merge h and g. Note that in this case neither h ; g nor g ; h is m(h, g); this implies that also g ; r(h, g) and h ; r(g, h) are not the merge morphism. Neither l(g, h) nor l(h, g) exist. The result of m(h, g) has "beer" as line 3 and 11 and "pasta" as line 6. m(h, g) = g ; f' ; f = h ; r(g, f). TODO: try to express m(h, g) in terms of m(f, g), m(f', g), etc.
9. Let h' = f' ; f. The result of m(h', g) has "beer" as line 3 and 12 and "pasta" as line 6. m(h', g) = f' ; g ; f.
10. m(h^r, g^r) = f'^r ; g^r ; f^r, m(h^r, g) = f'^r ; g ; f^r, m(h'^r, g) cannot be expressed as a composition of the three (so it's not always the case that merges of compositions of hunks are compositions of the very hunks), m(h'^r, g^r) is almost equal to g^r ; f'^r ; f^r, but if the original file has no "pasta" at line 5, "beer" will be removed from line 10 of the original file, instead of line 11.
11. Let k = f^r; f'. Notice that k has no right nor left inverses. TODO: try to merge k with everything.

[edit] Loose remarks documenting the process of reformulation

Most of the following uses a naming style, I've abandoned (file names instead of repos, etc.).

1. let's start with a simple case of repositories with no directories, no file permissions, only a fixed collection of named files, which furthermore cannot be deleted nor renamed
2. let's identify the set of all possible file contents with the set of all sequences of characters; let's say the set of all patches is a subset of the set of functions on character sequences (or, instead of functions, we may talk of representations of functions, e.g. in various diff formats); let's identify the files governed by the repository (or the file descriptors in the filesystem) with their filenames
3. we seem to operate in a category P, where filenames are objects of P and patches are morphisms of P
4. the domain of patch A is the filename N (the location on the hard disk, or the file descriptor in the filesystem) from which the patch "reads" the contents to be changed; the codomain of A is the filename M to which A "writes" the modified contents; we write this A : N -> M; usually N and M will be the same filename
5. identity on filename N in P (called id_N, or id in short), is the identity (empty) patch that operates on N by not changing it
6. composition of patches A and B in P, is the "sequence" AB (I like this diagrammatical notation) of patches A and B; for now let's gloss over any other cases than A and B both operating on the same file N
7. P is (roughly) a subcategory of the category of sets and functions (called Set) and it seems easy to make it a full subcategory, close it under products and coproducts and perhaps recover even more of the Set properties, but let's forget it until we need the other properties
8. we need to close P under finite products:
   • for filenames N_1, N_2, ..., N_k let N_1 x N_2 x ... x N_k be an object of our category (it can be identified with a huge reserved space on hard disk under the name "N_1xN_2x...xN_k" able to hold the contents of k files)
   • let pi_n : N_1 x N_2 x ... x N_k -> N_n be a projection patch, that is, a patch that given a contents of k files produces the contents of the n-th file;
   • for patches A_1, A_2, ..., A_k, such that A_n : M -> N_n, there exists exactly one patch <A_1, A_2, ..., A_k> : N -> N_1 x N_2 x ... x N_k such that <A_1, A_2, ..., A_k> pi_n (composition) is equal to A_n; the <A_1, A_2, ..., A_k> patch can be identified with the function that given contents of file M produces, e.g., the concatenation of results of patches N_1, N_2, ..., N_k on that content
9. now that P is closed under products, P, in particular, it has a product of the empty family of file names, which is called a terminal object 1
10. the terminal object can be imagined as a file that is guaranteed to be always empty (say, /dev/null); for any filename N there is exactly one patch !_N : N -> 1 --- the patch that reads the contents from file N and writes nothing to 1 (but does not change N)
11. now we are ready for the first important discovery: contexts are patches with domain 1
12. under this formulation, ^oA^aB^bC^c reads c = oABC, or more precisely: o : 1 -> N, A : N -> N_1, a = oA : 1 -> N_1, B : N_1 -> N_2, b = oAB : 1 -> N_2, C : N_2 -> N_3, c = oABC : 1 -> N_3
13. the categorical inverse of a morphism A, that is, the only morphism B such that AB = id and BA = id, is just the patch inverse A ^{- 1}; the condition about contexts trivially holds, when translated to the categorical notation
14. I see from the patch theory text that the set of morphisms of P must be such that every morphism A : N -> N has the inverse; so every endomorphism in P is an isomorphism; obviously other morphisms needn't be isomorphisms, e.g. if all the morphisms between 1 and other file names are isomorphisms, then all files in the repository are empty (or at least not modifiable at all)! set-theoretically, the isomorphism condition means that every patch A : N -> N (function on character sequences) has to be a bijection
15. the commutation of patches X and Y seems to be described in the text as the existence of such X' and Y' that: for each o : 1 -> N, oXY = oY'X', oX = oX' and oY = oY'; is it correct? Or is the context o actually fixed in some of the equalities (then it's easier to find a commutation)? (see the translation of this paragraph to the human language at the beginning of the talk page)
16. examples suggest commutation is something different than proposed above (and it seems fortunate, because otherwise commutation would be very hard to obtain for some global context sensitive formats of patches); I now have to wait for some more input to choose an appropriate definition
17. Hmmm. I'll assume the following definition of commutation and try to work from this onward, looking out for problems: the commutation of patches X and Y is such a patch Y' that for each o : 1 -> N, oXY = oY'X. (Yes, there are problems --- I also need the other, symmetric definition of commutation...)
18. it seems from the description in section "Parallel patches" that a pair of parallel patches is a triple o : 1 -> a, A : a -> b, B : a -> c. What is a merge of such parallel patches? We have B ^{− 1} : c -> a, so B ^{− 1} ; A : c -> b. I see a and b should be equal repos (file names) for the commutation below to make sense. Let A_1 : c -> c be the commutation of B ^{− 1} and A, so the following are extensionally equal: B ^{− 1} ; A and A_1 ; B ^{− 1}. The patch B ; A_1 : a -> c is the merge of the parallel patches.
19. Hmm, I see I've not used the morphism o for anything, so perhaps merge is independent of the context. I'll have to verify this vs. section "Performing the merge" and later sections. Unless a is equal to c, the typing is not symmetric, so merging A with B may be doable, while merging B with A may be not... The merge M of A and B has the property that M ; B ^{− 1} = A, but I can't find anything else to say about M and I bet this is not enough for the user (e.g., probably M ; A ^{- 1} = B would be needed, but perhaps some ugly kinds of patches are really not symmetric wrt merging?).
20. I've verified my definition of merge against the example in section "Merging is symmetric" and it's OK and, by accident, symmetric in this case. However, there is a subtle point here: if file rename is not a shallow operation on a directory (certain inode gets another name, but patch A still writes to the same inode) but if it's an operation that wipes the contents of one file and then writes it to another file, then the merge is no longer symmetric. The result then depends on whether adding the "beer" line happens before the wiping out or after --- I guess this is called a conflict...
21. the "commutation with inverse property" is quite trivial. To obtain one equality from the other just multiply both sides by one of the 8 patches from the left and by another from the right.
22. that would be it --- I've read and understood the entire 3 chapters about patch theory --- so the categorical reformulation works for me :). Now it's time to look up some other articles to try and find answers to my questions and verify my guesses I've incorporated into the reformulation. Thanks a lot for the wikibook!
23. Oops. While trying to compute some simple examples with my formalism I've noticed the patches are usually not surjective, so they do not have left inverses (when their domains and codomains are equal). I'll have to limit their codomains to make them surjective, but then I start depending on Set a lot. :( Other approach would be to work with partial functions, but then true inverses are even more scarce.
24. a better way will be to drop the requirement that patches have inverses. Right or left inverses should suffice for most things, anyway. And if true inverses are needed they can always be postulated for some patches. So I drop the two paragraphs:
    • Every patch f : a -> a must have an inverse. So every endomorphism of Repo is an isomorphism. Obviously other morphisms needn't be isomorphisms or, in the presence of terminal objects, the category would become trivial (all repos unmodifiable)
    • If the categorical inverse f ^{- 1} of a patch f : a -> b exists, it is unique (categorical inverse is a morphism that is both a right inverse and a left inverse: f;f ^{− 1} = id_a and f ^{− 1};f = id_b); ).
25. I'm a bit stuck right now. The overall setup is now stable and much simpler than any existing approaches, but the definition of merge should be probably much more complex. I don't like complex things so I guess I will take a break. So much for a page of category theory that ends world hunger. :)
26. The following definition of the Darcs "inverse" is wrong (unless we restrict Repo in strange ways):
    • A concrete inverse of patch f : a -> b in context o : 1 -> a is a patch cinv(o, f) : b -> a such that o ; f ; cinv(o, f) = o and f = cinv(o ; f, cinv(o, f)).
    • Let repo a be the set {1, 2}, repo b be {1, 2, ..., 10} and all functions between a and b belong to hom(Repo). Then there are no cinv operation with the states properties. (Let's assume such cinv exists. There are 2 ^ 10 = 1024 functions from a to b and only 10 * (10 ^ 2) = 1000 pairs of elements of b and functions from b to a. Let o : 1 -> a and let F(f : a -> b) = (o ; f, cinv(o, f)). Then there exist two different functions f1, f2 : a -> b such that we have F(f1) = (o ; f1, cinv(o, f1)) = (o ; f2, cinv(o, f2)) = F(f2). It would follow that f1 = cinv(o ; f1, cinv(o, f1)) = cinv(o ; f2, cinv(o, f2)) = f2, which is a contradiction). Another example of strange results of this definition appears if we consider concrete inverses of the hunk patch that removes line 3 with "beer", in contexts with no such line. It seems natural that we would like to take cinv in this case to be the identity, but then the inverse of identity cannot be the identity, which is outright bizarre. OTOH, if we weaken the second equality to o ; f = o ; cinv(o ; f, cinv(o, f)) it follows from the first equality for the two inverses and so it's not needed.
27. Perhaps it would make sense to generalize concrete inverse to:
    • A right inverse of f : a -> b relative to h : c -> a is such rinv(h, f) : b -> a that h ; f ; rinv(h, f) = h.
    • This may find some use in (some special?) merging. It also makes it possible to compute concrete inverses taking into account only parts of the patch collection: if there is h such that rinv(h, f) exists then cinv(o ; h, f) is equal to it, but we ignored the, possibly complex, patch o.
28. I see no way of determining a unique concrete inverse for a given patch. The following definition is wrong (not unique, e.g. the inverse of identity is only known to be an isomorphism):
    • We require that there exists the most general concrete inverse cinv(o, f) : b -> a for any f : a -> b and o : 1 -> a. That is, for every concrete inverse g of f and o, there is exactly one morphism h such that g = cinv(o, f) ; h. Note that the most general concrete inverse depends not only on f and o but also on hom(Repo), as demonstrated in the examples below.
    • o ; cinv(o ; f, cinv(o, f)) = o ; f for any context o (simple equational reasoning not using the property that cinv is most general). However, the following equation does not hold, e.g., for hunk patches: cinv(o ; f, cinv(o, f)) = f. So it is not true that "the most general inverse of the most general inverse is the original".