A typeclass for elements for which a supporting set of atoms can be computed in an efficient, structural, type-directed manner.

So: lists, sets, and name-abstractions yes, and function-types no. See instances for full details.

Note: This gives KSupport a strictly more specific and structure-directed meaning than the motivating mathematical notion of support, which does work e.g. on function-types.

A Tom instance of KSupport.

A Tom instance of ksupp.

a and b are kapart when they are supported by disjoint sets of s-atoms.

We use proxy instead of Proxy below, so the user can supply any type that mentions s.

a and b are apart when they are supported by disjoint sets of atoms.

Bring the first element of a list-like structure that an atom points to (by being mentioned in the support), and put it at the head of the nonempty list. Raises error if no such element exists.

atomPoint, for names. A name is just a labelled atom, and namePoint just discards the label and calls atomPoint.

Class for types that support a remove these atoms from my support, please operation. Should satisfy e.g.:

restrict atms $ restrict atms x == restrict atms x

atms `apart` x ==> restrict atms x == x

The canonical instance of KRestrict is Nom. The Swappable constraint is not necessary for the code to run, but in practice wherever we use KRestrict we expect the type to have a swapping action.

Note for experts: We may want KRestrict without KSupport, for example to work with Nom (Atom -> Atom).

Note for experts: Restriction is familiar in general terms (e.g. pi-calculus restriction). In a nominal context, the original paper is nominal rewriting with name-generation (author's pdf), and this has a for-us highly pertinent emphasis on unification and rewriting.

Instance of KRestrict on a Tom.

Form of restriction that takes names instead of atoms. Just discards name labels and calls restrict.