|Maintainer||Stephanie Weirich <email@example.com>|
A slow, but hopefully correct implementation of permutations.
- data Perm a
- single :: Ord a => a -> a -> Perm a
- compose :: Ord a => Perm a -> Perm a -> Perm a
- apply :: Ord a => Perm a -> a -> a
- support :: Ord a => Perm a -> [a]
- isid :: Ord a => Perm a -> Bool
- join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)
- empty :: Perm a
- restrict :: Ord a => Perm a -> [a] -> Perm a
- mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)
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.
Compose two permutations. The right-hand permutation will be applied first.
The support of a permutation is the set of elements which are not fixed.
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.