[darcs-devel] Semantics of witnesses

[Ben Franksen]

Hi Ganesh

thanks for bringing more structure to this discussion.

> If we view a state as a set of patches, then the following kinds of
> states are relevant to the discussion.
> 
> (1) The initial state of a patch representation

How do we define this initial state? It is defined implicitly as the
state we get when we apply all "previous patches" to the empty repo. But
the same patch (representation) can exist in different repos or
different reorderings of the same repo. So this initial state is only
unique relative to one repository at one point in time. It is not an
"invariant" property of a patch.

> (2) The set of states you can reach by commuting where the patch keeps
> the same representation

This is what I regard as the domain of the patch and what I think the
witness(es) of a patch symbolically denote. It /is/ an invariant
property of the patch in the sense that it does not depend on any
external context.

> (3) The set of states the unchanged patch representation would apply to
> cleanly
> (4) The set of states you can reach by commuting where the patch may not
> keep the same representation
> (5) The set of all states
> 
> (3) and (4) are supersets of (2) but neither is a superset of each other.

Agreed.

> Darcs has made a fundamental design choice - in the UI/patch semantics -
> to use commuting to determine what states a patch can be applied to,
> i.e. a patch representation is only valid in state (1) and a patch is
> valid in state (4) subject to a possible change in representation which
> is defined by the commute function.

I think this is closely related to patch equality which we discussed a
length elsewhere. The set (4) is /not/ what we track with witnesses. On
the UI layer we may identify patches with the same PatchId, but there
are no witnesses or domains and ranges at the UI layer. Internally, we
must be sure to identify two patches with the same name only /provided/
that either domain or range coincides i.e. the have the same start or
ending witness. This means that the set (4) is irrelevant in the context
of our current discussion.

> It's certainly plausible to design a VCS/patch theory to use (3) in some
> way but I think that would be quite different to the current Darcs. 

I fully agree with that, except that I do /not/ think it is possible to
arrive at a consistent theory based on (3), where with "consistent" I
mean a theory where we can expect reasonable laws to hold. The problem
with (3) is that it does not take the history of changes into account. A
sequences of patches can have intermediate states that overlap with
those of another sequence, even though the overall start and end states
are completely disjoint. This is why in Darcs merging is associative,
but not in Git or Mercurial.

> We
> could perhaps identify the set of states (2) to optimise our existing
> implementation.

Yes. I may have previously failed to make this clear, but I never
thought to take (3) as the domain of a patch, only (2).

Cheers
Ben