{-# language BangPatterns #-}
{-# language PatternSynonyms #-}
{-# language Safe #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language ViewPatterns #-}
-- |
-- Module       : Data.Group
-- Copyright    : (c) 2020-2021 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
, equalPermutation
, comparePermutation
, orderOfPermutation
, permute
, pairwise
, (-$)
, ($-)
, embed
, retract
  -- ** Permutation patterns
, pattern Permute
) where


import Data.Group

import qualified Data.IntSet as ISet
import Data.Function (on)
import Numeric.Natural (Natural)

infixr 0 $-, -$

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

-- | Isomorphism of a type 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!
--
-- === __Examples:__
--
-- >>> p1 = permute succ pred :: Permutation Integer
-- >>> p2 = permute negate negate :: Permutation Integer
-- >>> to (p1 <> p2) 2
-- -1
-- >>> from (p1 <> p2) (-1)
-- 2
-- >>> to (p2 <> p1) 2
-- -3
--
-- Permutations on a finite set @a@ (, indicated by satisfying
-- @(Bounded a, Enum a)@ constraint,) can be tested their equality
-- and computed their 'order's.
--
-- >>> c1 = permute not not :: Permutation Bool
-- >>> equalPermutation (c1 <> c1) mempty
-- True
-- >>> orderOfPermutation c1
-- 2
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 (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 b c a. (b -> c) -> (a -> b) -> a -> c
. 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
b (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation a -> a -> a
forall a. Permutation a -> a -> a
from Permutation a
a)

instance 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 (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
t

-- | Equality test for permutations on a finite type 'a'
--
-- This module /intentionally omits/ the following instance, albeit
-- 'equalPermutation' is suitable implementation of
-- @(==)@ operator for many types.
--
-- > instance (Enum a, Bounded a) => Eq (Permutation a) where
-- >   (==) = equalPermutation
--
-- This is because some type satisfying @(Enum a, Bounded a)@ are
-- actually finite but too large to use @equalPermutation@ on.
-- For example, you can call @equalPermutation@ on @Permutation Int@,
-- but it takes too much computation to be considered usable.
equalPermutation
  :: (Enum a, Bounded a) => Permutation a -> Permutation a -> Bool
equalPermutation :: Permutation a -> Permutation a -> Bool
equalPermutation = [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Int] -> [Int] -> Bool)
-> (Permutation a -> [Int])
-> Permutation a
-> Permutation a
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ((a -> a) -> [Int]
forall a. (Enum a, Bounded a) => (a -> a) -> [Int]
functionRepr ((a -> a) -> [Int])
-> (Permutation a -> a -> a) -> Permutation a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation a -> a -> a
forall a. Permutation a -> a -> a
to)

-- | Comparison for permutations on a finite type 'a'
--
-- This module /intentionally omits/ the following instance, albeit
-- 'comparePermutation' is suitable implementation of
-- @compare@ method for many types.
--
-- > instance (Enum a, Bounded a) => Eq (Permutation a) where
-- >   compare = comparePermutation
--
-- This is because some type satisfying @(Enum a, Bounded a)@ are
-- actually finite but too large to use @comparePermutation@ on.
-- For example, you can call @comparePermutation@ on @Permutation Int@,
-- but it takes too much computation to be considered usable.
comparePermutation
  :: (Enum a, Bounded a) => Permutation a -> Permutation a -> Ordering
comparePermutation :: Permutation a -> Permutation a -> Ordering
comparePermutation = [Int] -> [Int] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Int] -> [Int] -> Ordering)
-> (Permutation a -> [Int])
-> Permutation a
-> Permutation a
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ((a -> a) -> [Int]
forall a. (Enum a, Bounded a) => (a -> a) -> [Int]
functionRepr ((a -> a) -> [Int])
-> (Permutation a -> a -> a) -> Permutation a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Permutation a -> a -> a
forall a. Permutation a -> a -> a
to)

functionRepr :: (Enum a, Bounded a) => (a -> a) -> [Int]
functionRepr :: (a -> a) -> [Int]
functionRepr a -> a
f = a -> Int
forall a. Enum a => a -> Int
fromEnum (a -> Int) -> (a -> a) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f (a -> Int) -> [a] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a
forall a. Bounded a => a
minBound .. a
forall a. Bounded a => a
maxBound]

-- | Order counting for a permutation on a finite type 'a'
--
-- This module /intentionally omits/ the following instance, albeit
-- 'orderOfPermutation' is suitable implementation of
-- @order@ method for many types.
--
-- > instance (Enum a, Bounded a) => GroupOrder (Permutation a) where
-- >   order a = Finite (orderOfPermutation a)
--
-- This is because some type satisfying @(Enum a, Bounded a)@ are
-- actually finite but too large to use @orderOfPermutation@ on.
-- For example, you can call @orderOfPermutation@ on @Permutation Int@,
-- but it takes too much computation to be considered usable.
orderOfPermutation
  :: forall a. (Enum a, Bounded a) => Permutation a -> Natural
orderOfPermutation :: Permutation a -> Natural
orderOfPermutation Permutation{to :: forall a. Permutation a -> a -> a
to = a -> a
f} = Natural -> IntSet -> Natural
go Natural
1 IntSet
fullSet
    where
      n :: Int
n = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ a -> Int
forall a. Enum a => a -> Int
fromEnum (Bounded a => a
forall a. Bounded a => a
maxBound @a)
      fullSet :: IntSet
fullSet = [Int] -> IntSet
ISet.fromDistinctAscList [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

      f' :: Int -> Int
      f' :: Int -> Int
f' = a -> Int
forall a. Enum a => a -> Int
fromEnum (a -> Int) -> (Int -> a) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f (a -> a) -> (Int -> a) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a
forall a. Enum a => Int -> a
toEnum

      go :: Natural -> ISet.IntSet -> Natural
      go :: Natural -> IntSet -> Natural
go !Natural
ord IntSet
elements = case IntSet -> Maybe (Int, IntSet)
ISet.minView IntSet
elements of
        Maybe (Int, IntSet)
Nothing             -> Natural
ord
        Just (Int
k, IntSet
elements') ->
          let (Natural
period, IntSet
elements'') = Int -> IntSet -> (Natural, IntSet)
takeCycle Int
k IntSet
elements'
          in Natural -> IntSet -> Natural
go (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
lcm Natural
period Natural
ord) IntSet
elements''

      takeCycle :: Int -> ISet.IntSet -> (Natural, ISet.IntSet)
      takeCycle :: Int -> IntSet -> (Natural, IntSet)
takeCycle Int
k = Natural -> Int -> IntSet -> (Natural, IntSet)
forall a. Enum a => a -> Int -> IntSet -> (a, IntSet)
loop Natural
1 (Int -> Int
f' Int
k)
        where
          loop :: a -> Int -> IntSet -> (a, IntSet)
loop !a
period Int
j IntSet
elements
            | Int
j Int -> IntSet -> Bool
`ISet.member` IntSet
elements      = a -> Int -> IntSet -> (a, IntSet)
loop (a -> a
forall a. Enum a => a -> a
succ a
period) (Int -> Int
f' Int
j) (Int -> IntSet -> IntSet
ISet.delete Int
j IntSet
elements)
            | {- j ∉ elements && -} Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k = (a
period, IntSet
elements)
            | Bool
otherwise                     = [Char] -> (a, IntSet)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (a, IntSet)) -> [Char] -> (a, IntSet)
forall a b. (a -> b) -> a -> b
$ [Char]
"Non-bijective: witness=toEnum " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
j

-- -------------------------------------------------------------------- --
-- 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 m. Group m => m -> m
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