unbound-0.2.1: Generic support for programming with names and binders

MaintainerStephanie Weirich <sweirich@cis.upenn.edu>



A slow, but hopefully correct implementation of permutations.



data Perm a Source

A permutation is a bijective function from names to names which is the identity on all but a finite set of names. They form the basis for nominal approaches to binding, but can also be useful in general.


Ord a => Eq (Perm a) 
Show a => Show (Perm a) 
Ord a => Monoid (Perm a)

Permutations form a monoid under composition.

single :: Ord a => a -> a -> Perm aSource

Create a permutation which swaps two elements.

compose :: Ord a => Perm a -> Perm a -> Perm aSource

Compose two permutations. The right-hand permutation will be applied first.

apply :: Ord a => Perm a -> a -> aSource

Apply a permutation to an element of the domain.

support :: Ord a => Perm a -> [a]Source

The support of a permutation is the set of elements which are not fixed.

isid :: Ord a => Perm a -> BoolSource

Is this the identity permutation?

join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)Source

Join two permutations by taking the union of their relation graphs. Fail if they are inconsistent, i.e. map the same element to two different elements.

empty :: Perm aSource

The empty (identity) permutation.

restrict :: Ord a => Perm a -> [a] -> Perm aSource

Restrict a permutation to a certain domain.

mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)Source

mkPerm l1 l2 creates a permutation that sends l1 to l2. Fail if there is no such permutation, either because the lists have different lengths or because they are inconsistent (which can only happen if l1 or l2 have repeated elements).