Safe Haskell | Safe-Inferred |
---|

- data Permutation = Perm {}
- permute :: Permutation -> [a] -> [a]
- idP :: Int -> Permutation
- takeP :: Int -> Permutation -> Permutation
- liftP :: Int -> Permutation -> Permutation
- composeP :: Permutation -> Permutation -> Permutation
- invertP :: Permutation -> Permutation
- compactP :: Permutation -> Permutation
- reverseP :: Permutation -> Permutation
- expandP :: Int -> Int -> Permutation -> Permutation
- topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

# Documentation

data Permutation Source

permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]

Agda typing would be:
`Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation`

`m`

is the `size`

of the permutation.

permute :: Permutation -> [a] -> [a]Source

`permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]`

More precisely, `permute indices list = sublist`

, generates `sublist`

from `list`

by picking the elements of list as indicated by `indices`

.
`permute [1,3,0] [x0,x1,x2,x3] = [x1,x3,x0]`

Agda typing:
`permute (Perm {m} n is) : Vec A m -> Vec A n`

idP :: Int -> PermutationSource

takeP :: Int -> Permutation -> PermutationSource

liftP :: Int -> Permutation -> PermutationSource

`liftP k`

takes a `Perm {m} n`

to a `Perm {m+k} (n+k)`

.
Analogous to `liftS`

,
but Permutations operate on de Bruijn LEVELS, not indices.

composeP :: Permutation -> Permutation -> PermutationSource

permute (compose p1 p2) == permute p1 . permute p2

compactP :: Permutation -> PermutationSource

Turn a possible non-surjective permutation into a surjective permutation.

reverseP :: Permutation -> PermutationSource

permute (reverseP p) xs == reverse $ permute p $ reverse xs

Example:
```
permute (reverseP (Perm 4 [1,3,0])) [x0,x1,x2,x3]
== permute (Perm 4 $ map (3-) [0,3,1]) [x0,x1,x2,x3]
== permute (Perm 4 [3,0,2]) [x0,x1,x2,x3]
== [x3,x0,x2]
== reverse [x2,x0,x3]
== reverse $ permute (Perm 4 [1,3,0]) [x3,x2,x1,x0]
== reverse $ permute (Perm 4 [1,3,0]) $ reverse [x0,x1,x2,x3]
```

expandP :: Int -> Int -> Permutation -> PermutationSource

`expandP i n π`

in the domain of `π`

replace the *i*th element by *n* elements.

topoSort :: (a -> a -> Bool) -> [a] -> Maybe PermutationSource

Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.