{-# language PatternSynonyms #-}
{-# language Safe #-}
{-# language ViewPatterns #-}
-- |
-- Module       : Data.Group
-- Copyright    : (c) 2020 Emily Pillmore
-- License      : BSD-style
--
-- Maintainer   : Reed Mullanix <reedmullanix@gmail.com>,
--                Emily Pillmore <emilypi@cohomolo.gy>
--
-- Stability    : stable
-- Portability  : non-portable
--
-- This module provides definitions for 'Permutation's
-- along with useful combinators.
--
module Data.Group.Permutation
( -- * Permutation groups
  Permutation(..)
  -- ** Permutation group combinators
, permute
, pairwise
, (-$)
, ($-)
, embed
, retract
  -- ** Permutation patterns
, pattern Permute
) where


import Data.Group
import Data.Group.Additive
import Data.Group.Multiplicative

infixr 0 $-, -$

-- -------------------------------------------------------------------- --
-- Permutations

-- | 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!
--
data Permutation a = Permutation
  { Permutation a -> a -> a
to :: a -> a
    -- ^ The forward half of the bijection
  , Permutation a -> a -> a
from :: a -> a
    -- ^ The inverse half of the bijection
  }

-- instance Profunctor Permutation where
--   dimap = :'(

instance Semigroup a => Semigroup (Permutation a) where
  Permutation a
a <> :: Permutation a -> Permutation a -> Permutation a
<> Permutation a
b = (a -> a) -> (a -> a) -> Permutation a
forall a. (a -> a) -> (a -> a) -> Permutation a
Permutation (Permutation a -> a -> a
forall a. Permutation a -> a -> a
to Permutation a
a (a -> a) -> (a -> a) -> a -> a
forall a. Semigroup a => a -> a -> a
<> Permutation a -> a -> a
forall a. Permutation a -> a -> a
to Permutation a
b) (Permutation a -> a -> a
forall a. Permutation a -> a -> a
from Permutation a
a (a -> a) -> (a -> a) -> a -> a
forall a. Semigroup a => a -> a -> a
<> Permutation a -> a -> a
forall a. Permutation a -> a -> a
from Permutation a
b)

instance Monoid a => Monoid (Permutation a) where
  mempty :: Permutation a
mempty = (a -> a) -> (a -> a) -> Permutation a
forall a. (a -> a) -> (a -> a) -> Permutation a
Permutation a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id

instance Group a => Group (Permutation a) where
  invert :: Permutation a -> Permutation a
invert (Permutation a -> a
t a -> a
f) = (a -> a) -> (a -> a) -> Permutation a
forall a. (a -> a) -> (a -> a) -> Permutation a
Permutation (a -> a
f (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
t) (a -> a
t (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f)

instance AbelianGroup a => AbelianGroup (Permutation a)
instance AdditiveGroup a => AdditiveGroup (Permutation a)
instance AdditiveAbelianGroup a => AdditiveAbelianGroup (Permutation a)
instance MultiplicativeGroup a => MultiplicativeGroup (Permutation a)


-- -------------------------------------------------------------------- --
-- Permutation group combinators

-- | Build a 'Permutation' from a bijective pair.
--
permute :: (a -> a) -> (a -> a) -> Permutation a
permute :: (a -> a) -> (a -> a) -> Permutation a
permute = (a -> a) -> (a -> a) -> Permutation a
forall a. (a -> a) -> (a -> a) -> Permutation a
Permutation
{-# inline permute #-}

-- | Destroy a 'Permutation', producing the underlying pair of
-- bijections.
--
pairwise :: Permutation a -> (a -> a, a -> a)
pairwise :: Permutation a -> (a -> a, a -> a)
pairwise Permutation a
p = (Permutation a -> a -> a
forall a. Permutation a -> a -> a
to Permutation a
p, Permutation a -> a -> a
forall a. Permutation a -> a -> a
from Permutation a
p)
{-# inline pairwise #-}

-- | Infix alias for the 'to' half of 'Permutation' bijection
--
(-$) :: Permutation a -> a -> a
-$ :: Permutation a -> a -> a
(-$) = Permutation a -> a -> a
forall a. Permutation a -> a -> a
to
{-# inline (-$) #-}

-- | Infix alias for the 'from' half of 'Permutation' bijection
--
($-) :: Permutation a -> a -> a
$- :: Permutation a -> a -> a
($-) = Permutation a -> a -> a
forall a. Permutation a -> a -> a
from
{-# inline ($-) #-}

-- | Embed a 'Group' into the 'Permutation' group on it's underlying set.
--
embed :: (Group g) => g -> Permutation g
embed :: g -> Permutation g
embed g
g = Permutation :: forall a. (a -> a) -> (a -> a) -> Permutation a
Permutation { to :: g -> g
to = (g
g g -> g -> g
forall a. Semigroup a => a -> a -> a
<>), from :: g -> g
from = (g -> g
forall a. Group a => a -> a
invert g
g g -> g -> g
forall a. Semigroup a => a -> a -> a
<>) }

-- | Get a group element out of the permutation group.
-- This is a left inverse to 'embed', i.e.
--
-- @
--    retract . embed = id
-- @
--
retract :: (Group g) => Permutation g -> g
retract :: Permutation g -> g
retract Permutation g
p = Permutation g
p Permutation g -> g -> g
forall a. Permutation a -> a -> a
-$ g
forall a. Monoid a => a
mempty

-- | Bidirectional pattern synonym for embedding/retraction of groups
-- into their permutation groups.
--
pattern Permute :: Group g => Permutation g -> g
pattern $bPermute :: Permutation g -> g
$mPermute :: forall r g.
Group g =>
g -> (Permutation g -> r) -> (Void# -> r) -> r
Permute p <- (embed -> p)
  where Permute Permutation g
p = Permutation g -> g
forall g. Group g => Permutation g -> g
retract Permutation g
p