In the discussion at patch2257 you wrote
> IMO the real issue is that the witnesses for `AddName` etc should really
> live in an orthogonal namespace to the witnesses for patch contents. The
> no-op commutes are actually a smell that they should happen for free.
It would be nice if we could have completely separate patch theories for
Names (with explicit dependencies) on the one hand and a for Content (with
implicit dependencies) on the other; and then combine them in a generic way
e.g. by saying that the product of Name and Content commutes iff both
components commute. But to make this actually useful we also need a way to
represent name changes and pure content changes explicitly, like in Rebase,
which means we actually need a mixture of product and sum similar to
'These', when we combine Name and Content.
It seems that what you are saying is that the witnesses for those theories
would "naturally" belong to different kinds, and that the witness kind for
the sum/product would be a product of those kinds. This might be so, but,
verbosity and technical difficulties aside, I don't think it is actually
necessary. The trivial commutes which you claim have a "smell" are just
another way to express the same idea without separate name spaces for
witnesses.
My patch is meant to show how this could be done. The idea is that when we
construct a Named patch from PatchInfo and content, we track the addition of
the name by also constructing and returning a suitable RebaseName patch that
removes that effect. For updatePatchHeader, this is a Rename. The patch is
incomplete because when we record a new patch we should also create a
DelName, when we unrecord an AddName, etc.
|
