Copyright | (c) 2020 Emily Pillmore |
---|---|

License | BSD-style |

Maintainer | Reed Mullanix <reedmullanix@gmail.com>, Emily Pillmore <emilypi@cohomolo.gy> |

Stability | stable |

Portability | non-portable |

Safe Haskell | Safe |

Language | Haskell2010 |

This module provides definitions for `Permutation`

s
along with useful combinators.

## Synopsis

- data Permutation a = Permutation {}
- permute :: (a -> a) -> (a -> a) -> Permutation a
- pairwise :: Permutation a -> (a -> a, a -> a)
- (-$) :: Permutation a -> a -> a
- ($-) :: Permutation a -> a -> a
- embed :: Group g => g -> Permutation g
- retract :: Group g => Permutation g -> g
- pattern Permute :: Group g => Permutation g -> g

# Permutation groups

data Permutation a Source #

Isomorphism of a finite set onto itself. Each entry consists of one half of the isomorphism.

*Note*: It is the responsibility of the user to provide inverse proofs
for `to`

and `from`

. Be responsible!

#### Instances

## Permutation group combinators

permute :: (a -> a) -> (a -> a) -> Permutation a Source #

Build a `Permutation`

from a bijective pair.

pairwise :: Permutation a -> (a -> a, a -> a) Source #

Destroy a `Permutation`

, producing the underlying pair of
bijections.

(-$) :: Permutation a -> a -> a infixr 0 Source #

Infix alias for the `to`

half of `Permutation`

bijection

($-) :: Permutation a -> a -> a infixr 0 Source #

Infix alias for the `from`

half of `Permutation`

bijection

embed :: Group g => g -> Permutation g Source #

Embed a `Group`

into the `Permutation`

group on it's underlying set.

retract :: Group g => Permutation g -> g Source #

Get a group element out of the permutation group.
This is a left inverse to `embed`

, i.e.

retract . embed = id

## Permutation patterns

pattern Permute :: Group g => Permutation g -> g Source #

Bidirectional pattern synonym for embedding/retraction of groups into their permutation groups.