An element of KRen is either

1. Just an injective finite map from KAtom to KAtom (for this file, call this a renaming), or
2. A "nomap" value (Nothing).

A KRen represents a solution to the problem

does there exist a permutation that makes x equal to y?

A type in the KUnifyPerm typeclass is structurally guaranteed to give at most one solution to such a unification problem, up to renaming irrelevant atoms. So in a nutshell: names, lists, and tuples are good here, and functions (not an equality type) and sets (may have multiple solutions) are not good.

A Just value represents a solution to this unification problem; a Nothing value represents that no such solution can be found. unifyPerm calculates these solutions.

Renaming on a Tom instance

The identity renaming.

The Nothing renaming. If we think of KRen s as type of solutions to permutation unification problems, then nothingRen indicates no solution could be found.

Is it Just a renaming? (My unification problem can be solved, and here's the solution.)

Is it Nothing? (Nope; no solution exists.)

The parts of the map that are not identity

Extend a renaming m with a new pair a -> b, maintaining the property of being a partial injection. If adding a->b would destroy partial injectivity, then return Nothing.

Extract the graph of a KRen, Maybe.

Convert a graph to a KRen.

Given a block of atoms, remove them from the map provided that the atoms in that block only map to other atoms within it; if an atom gets mapped across the block boundary, return Nothing.

Needed for equality instance of Chunk.

Equal-up-to-permutation. The algorithm works very simply by traversing the element looking for atoms and when it finds them, trying to match them up. If it can do so injectively then it succeeds with Just a renaming; if it fails it returns Nothing.

Question: Granted that KUnifyPerm is a subset of KSupport, why are they not equal? Because for simplicity we only consider types for which at most one unifier can be found, by an efficient structural traversal. This avoids backtracking, and makes a kunifyPerm a function to KRen. So, a key difference is that KSupport can easily calculate the support of a set (unordered list without multiplicities) whereas KUnifyPerm does not even attempt to calculate unifiers of sets; not because this would be impossible, but because it would require a significant leap in complexity that we do not seem to need (so far).

Tom-instance of typeclass KUnifyPerm.

Unify on KAtoms, thus Tom-instance of kunifyPerm.

Does an s-unifier exist?

We write proxy instead of Proxy for the user's convenience, so the user can take advantage of any type that mentions s.

Does a Tom-unifier exist?

Unify a list with a prefix of the other

Unify a list with a prefix of the other (at Tom version).

One list unifies with a prefix of the other

One list unifies with a prefix of the other (at Tom version).