...also involved some playing around with patch theory (again). I noticed that RepoPatchV1 heavily uses unsafeCoerceP and friends and saw a comment that explains it, historically. It suggested that a better representation might lead to less of these type castings. Another comment made look at very early versions of darcs1 that still contained David's explanations in the code (Patch.lhs). This early code does has no witnesses (so it isn't swamped with coertions) and does not yet use the optimization of pre-calculating the effect and the unwinding and putting them into the patch type. I wondered why merge and commute need to be so complicated since even with David's explanations this isn't completely clear, so I started playing around with it, which of course didn't work. The explanation I found is that while the semantics of a first level Merger is simple (Merger a b applies after a, represents b, and has effect a^-1), this simple semantics works only if a and b are prim patches and not when one of them is themself a Merger. Darcs1 has Mergers nested within Mergers and, as I learned, their semantics is necessarily very complicated.
That led me to try again to understand the camp theory. The last version I had read (which was quite some time ago) had many parts missing and did not yet contain any (Coq) formalizations and few explanations, so I did not understand it back then. With the latest version I understood the ideas (which to a large extent is due to my being more familiar with darcs' patch theory). It explains the algorithms pretty well and my understanding is that the camp theory is actually simpler than that of darcs-2. Furthermore, appendix B explains why both darcs theories cannot have the properties we would like, in particular why concistency of failure (in the presence of duplicate patches) is actually not attainable there. So I thought about how to incorporate camp theory as some sort of RepoPatchV3 into darcs. I think the greatest hurdle here is that camp relies on primitive patches to be "named", that is, we must generate and store some unique ID with every primitive patch. The appendix B explains pretty well why this is needed. I think this could be done by adding (yet) another class (interface) for prim patches, one which is used only to implement RepoPatchV3, so could perhaps be hidden inside the representation. Cheers Ben _______________________________________________ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
