Class of patches that have an identity/name.

Patches with an identity give rise to the notion of nominal equality, expressed by the operators =\^/= and =/^\=.

Laws:

ident-commute

Patch identity must be invariant under commutation:

'commute' (p :> _) == 'Just' (_ :> p') => 'ident' p == 'ident' p'

and thus (via symmetry of commute):

'commute' (_ :> q) == 'Just' (q' :> _) => 'ident' q == 'ident' q'

Conversely, patches with the same identity result from a series of commutes:

'ident' p == 'ident' p' => exists qs, qs' :: FL p. 'commuteFL' (p :> qs) == 'Just' (qs' :> p')

ident-compare

In general, comparing patches via their identity is weaker than (semantic) equality:

'unsafeCompare' p q => 'ident' p == 'ident' q

However, if the patches have a common context, then semantic and nominal equality should coincide, up to internal re-ordering:

p '=\~/=' q  <=> p '=\^/=' q

p '=/~\=' q  <=> p '=/^\=' q

(Technical note: equality up to internal re-ordering is currently only defined for FLs, but it should be obvious how to generalize it.)

Taken together, these laws express the assumption that recording a patch gives it a universally unique identity.

Note that violations of this universal property are currently not detected in a reliable way. Fixing this is possible but far from easy.

Constraint for patches that have an identity that is signed, i.e. can be positive (uninverted) or negative (inverted).

Provided that an instance Invert exists, inverting a patch inverts its identity:

'ident' ('invert' p) = 'invertId' ('ident' p)

The reason this is not associated to class Ident is that for technical reasons we want to be able to define type instances for patches that don't have an identity and therefore cannot be lawful members of class Ident.

Nominal equality for patches with an identity in the same context. Usually quite a bit faster than structural equality.

Signed identities.

Like for class Invert, we require that invertId is self-inverse:

'invertId' . 'invertId' = 'id'

We also require that inverting changes the sign:

'positiveId' . 'invertId' = 'not' . 'positiveId'

Side remark: in mathematical terms, these properties can be expressed by stating that invertId is an involution and that positiveId is a "homomorphism of sets with an involution" (there is no official term for this) from a to the simplest non-trivial set with involution, namely Bool with the involution not.

Storable identities.

The methods here can be used to help implement ReadPatch and ShowPatch for a patch type containing the identity.

As with all Read/Show pairs, We expect that the output of showId ForStorage x can be parsed by readId to produce x:

'parse' 'readId' . 'renderPS' . 'showId' 'ForStorage' == 'id'

Remove a patch from an FL of patches with an identity. The result is Just whenever the patch has been found and removed and Nothing otherwise. If the patch is not found at the head of the sequence we must first commute it to the head before we can remove it.

We assume that this commute always succeeds. This is justified because patches are created with a (universally) unique identity, implying that if two patches have the same identity, then they have originally been the same patch; thus being at a different position must be due to commutation, meaning we can commute it back.

For patch types that define semantic equality via nominal equality, this is only faster than removeFL if the patch does not occur in the sequence, otherwise we have to perform the same number of commutations.

Same as fastRemoveFL only for RL.

Find the common and uncommon parts of two lists that start in a common context, using patch identity for comparison. Of the common patches, only one is retained, the other is discarded.

Try to commute all patches matching any of the PatchIds in the set to the head of an FL, i.e. backwards in history.