{-# LANGUAGE CPP          #-}
{-# LANGUAGE TypeFamilies #-}

{- |
   Free groups

     * https://en.wikipedia.org/wiki/Free_group
     * https://ncatlab.org/nlab/show/Nielsen-Schreier+theorem

 -}
module Data.Group.Free
    ( FreeGroup
    , fromDList
    , toDList
    , normalize

    , FreeGroupL
    , consL
    , fromList
    , toList
    , normalizeL
    ) where

import           Control.Monad (ap)
import           Data.Bifunctor (bimap)
import           Data.DList (DList)
import qualified Data.DList as DList
#if MIN_VERSION_dlist(1,0,0)
import           Data.DList.Unsafe (DList (..))
#endif
import           Data.Group (Group (..))
import           Data.List (foldl')

import           Data.Algebra.Free
                    ( AlgebraType
                    , AlgebraType0
                    , FreeAlgebra (..)
                    )

-- | Free group generated by a type @a@.  Internally it's represented by a list
-- @[Either a a]@ where inverse is given by:
--
-- @
--  inverse (FreeGroup [a]) = FreeGroup [either Right Left a]
-- @
--
-- It is a monad on a full subcategory of @Hask@ which constists of types which
-- satisfy the @'Eq'@ constraint.
--
-- @'FreeGroup' a@ is isomorphic with @'Free' Group a@ (but the latter does not
-- require @Eq@ constraint, hence is more general).
--
newtype FreeGroup a = FreeGroup {
        forall a. FreeGroup a -> DList (Either a a)
runFreeGroup :: DList (Either a a)
    }
    deriving (FreeGroup a -> FreeGroup a -> Bool
forall a. Eq a => FreeGroup a -> FreeGroup a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FreeGroup a -> FreeGroup a -> Bool
$c/= :: forall a. Eq a => FreeGroup a -> FreeGroup a -> Bool
== :: FreeGroup a -> FreeGroup a -> Bool
$c== :: forall a. Eq a => FreeGroup a -> FreeGroup a -> Bool
Eq, FreeGroup a -> FreeGroup a -> Bool
FreeGroup a -> FreeGroup a -> Ordering
FreeGroup a -> FreeGroup a -> FreeGroup a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (FreeGroup a)
forall a. Ord a => FreeGroup a -> FreeGroup a -> Bool
forall a. Ord a => FreeGroup a -> FreeGroup a -> Ordering
forall a. Ord a => FreeGroup a -> FreeGroup a -> FreeGroup a
min :: FreeGroup a -> FreeGroup a -> FreeGroup a
$cmin :: forall a. Ord a => FreeGroup a -> FreeGroup a -> FreeGroup a
max :: FreeGroup a -> FreeGroup a -> FreeGroup a
$cmax :: forall a. Ord a => FreeGroup a -> FreeGroup a -> FreeGroup a
>= :: FreeGroup a -> FreeGroup a -> Bool
$c>= :: forall a. Ord a => FreeGroup a -> FreeGroup a -> Bool
> :: FreeGroup a -> FreeGroup a -> Bool
$c> :: forall a. Ord a => FreeGroup a -> FreeGroup a -> Bool
<= :: FreeGroup a -> FreeGroup a -> Bool
$c<= :: forall a. Ord a => FreeGroup a -> FreeGroup a -> Bool
< :: FreeGroup a -> FreeGroup a -> Bool
$c< :: forall a. Ord a => FreeGroup a -> FreeGroup a -> Bool
compare :: FreeGroup a -> FreeGroup a -> Ordering
$ccompare :: forall a. Ord a => FreeGroup a -> FreeGroup a -> Ordering
Ord, Int -> FreeGroup a -> ShowS
forall a. Show a => Int -> FreeGroup a -> ShowS
forall a. Show a => [FreeGroup a] -> ShowS
forall a. Show a => FreeGroup a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FreeGroup a] -> ShowS
$cshowList :: forall a. Show a => [FreeGroup a] -> ShowS
show :: FreeGroup a -> String
$cshow :: forall a. Show a => FreeGroup a -> String
showsPrec :: Int -> FreeGroup a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FreeGroup a -> ShowS
Show)

instance Functor FreeGroup where
    fmap :: forall a b. (a -> b) -> FreeGroup a -> FreeGroup b
fmap a -> b
f (FreeGroup DList (Either a a)
as) = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f a -> b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DList (Either a a)
as

instance Applicative FreeGroup where
    pure :: forall a. a -> FreeGroup a
pure a
a = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall a b. (a -> b) -> a -> b
$ forall a. a -> DList a
DList.singleton (forall a b. b -> Either a b
Right a
a)
    <*> :: forall a b. FreeGroup (a -> b) -> FreeGroup a -> FreeGroup b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad FreeGroup where
    return :: forall a. a -> FreeGroup a
return  = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    FreeGroup DList (Either a a)
as >>= :: forall a b. FreeGroup a -> (a -> FreeGroup b) -> FreeGroup b
>>= a -> FreeGroup b
f = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall a b. (a -> b) -> a -> b
$ DList (Either a a)
as forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. FreeGroup a -> DList (Either a a)
runFreeGroup forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> FreeGroup b
f a -> FreeGroup b
f

-- | Normalize a @Dlist@, i.e. remove adjacent inverses from a word, i.e.
-- @ab⁻¹ba⁻¹c = c@.  Note that this function is implemented using
-- @'normalizeL'@, implemnting it directly on @DList@s would be @O(n^2)@
-- instead of @O(n)@.
--
-- /Complexity:/ @O(n)@
normalize
    :: Eq a
    => DList (Either a a)
    -> DList (Either a a)
normalize :: forall a. Eq a => DList (Either a a) -> DList (Either a a)
normalize = forall a. [a] -> DList a
DList.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [Either a a] -> [Either a a]
normalizeL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. DList a -> [a]
DList.toList

-- | Smart constructor which normalizes a dlist.
--
-- /Complexity:/ @O(n)@
--
fromDList :: Eq a => DList (Either a a) -> FreeGroup a
fromDList :: forall a. Eq a => DList (Either a a) -> FreeGroup a
fromDList = forall a. Eq a => [Either a a] -> FreeGroup a
freeGroupFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. DList a -> [a]
DList.toList

-- | Construct a FreeGroup from a list.
--
-- /Complextiy:/ @O(n)@
--
freeGroupFromList :: Eq a => [Either a a] -> FreeGroup a
freeGroupFromList :: forall a. Eq a => [Either a a] -> FreeGroup a
freeGroupFromList = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> DList a
DList.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [Either a a] -> [Either a a]
normalizeL

toDList :: FreeGroup a -> DList (Either a a)
toDList :: forall a. FreeGroup a -> DList (Either a a)
toDList = forall a. FreeGroup a -> DList (Either a a)
runFreeGroup

instance Eq a => Semigroup (FreeGroup a) where
    FreeGroup DList (Either a a)
as <> :: FreeGroup a -> FreeGroup a -> FreeGroup a
<> FreeGroup DList (Either a a)
bs = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall a b. (a -> b) -> a -> b
$ forall a. Eq a => DList (Either a a) -> DList (Either a a)
normalize (DList (Either a a)
as forall a. DList a -> DList a -> DList a
`DList.append` DList (Either a a)
bs)

instance Eq a => Monoid (FreeGroup a) where
    mempty :: FreeGroup a
mempty = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall a. DList a
DList.empty
#if __GLASGOW_HASKELL__ <= 802
    mappend = (<>)
#endif

instance Eq a => Group (FreeGroup a) where
    invert :: FreeGroup a -> FreeGroup a
invert (FreeGroup DList (Either a a)
as) = forall a. DList (Either a a) -> FreeGroup a
FreeGroup forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\DList (Either a a)
acu Either a a
a -> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left Either a a
a forall a. a -> DList a -> DList a
`DList.cons` DList (Either a a)
acu) forall a. DList a
DList.empty DList (Either a a)
as

type instance AlgebraType0 FreeGroup a = Eq a
type instance AlgebraType  FreeGroup g = (Eq g, Group g)
instance FreeAlgebra FreeGroup where
    returnFree :: forall a. a -> FreeGroup a
returnFree a
a = forall a. DList (Either a a) -> FreeGroup a
FreeGroup (forall a. a -> DList a
DList.singleton (forall a b. b -> Either a b
Right a
a))
    foldMapFree :: forall d a.
(AlgebraType FreeGroup d, AlgebraType0 FreeGroup a) =>
(a -> d) -> FreeGroup a -> d
foldMapFree a -> d
_ (FreeGroup DList (Either a a)
DList.Nil) = forall a. Monoid a => a
mempty
    foldMapFree a -> d
f (FreeGroup DList (Either a a)
as)        =
        let a' :: Either a a
a'  = forall a. DList a -> a
DList.head DList (Either a a)
as
#if MIN_VERSION_dlist(1,0,0)
            as' :: DList (Either a a)
as' = case DList (Either a a)
as of
              UnsafeDList [Either a a] -> [Either a a]
g -> forall a. ([a] -> [a]) -> DList a
UnsafeDList (forall a. Int -> [a] -> [a]
drop Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either a a] -> [Either a a]
g)
#else
            as' = DList.tail as
#endif
        in forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall m. Group m => m -> m
invert forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> d
f) a -> d
f Either a a
a' forall a. Monoid a => a -> a -> a
`mappend` forall (m :: * -> *) d a.
(FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) =>
(a -> d) -> m a -> d
foldMapFree a -> d
f (forall a. DList (Either a a) -> FreeGroup a
FreeGroup DList (Either a a)
as')

-- | Free group in the class of groups which multiplication is strict on the
-- left, i.e.
--
-- prop> undefined <> a = undefined
--
newtype FreeGroupL a = FreeGroupL { forall a. FreeGroupL a -> [Either a a]
runFreeGroupL :: [Either a a] }
    deriving (Int -> FreeGroupL a -> ShowS
forall a. Show a => Int -> FreeGroupL a -> ShowS
forall a. Show a => [FreeGroupL a] -> ShowS
forall a. Show a => FreeGroupL a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FreeGroupL a] -> ShowS
$cshowList :: forall a. Show a => [FreeGroupL a] -> ShowS
show :: FreeGroupL a -> String
$cshow :: forall a. Show a => FreeGroupL a -> String
showsPrec :: Int -> FreeGroupL a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FreeGroupL a -> ShowS
Show, FreeGroupL a -> FreeGroupL a -> Bool
forall a. Eq a => FreeGroupL a -> FreeGroupL a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FreeGroupL a -> FreeGroupL a -> Bool
$c/= :: forall a. Eq a => FreeGroupL a -> FreeGroupL a -> Bool
== :: FreeGroupL a -> FreeGroupL a -> Bool
$c== :: forall a. Eq a => FreeGroupL a -> FreeGroupL a -> Bool
Eq, FreeGroupL a -> FreeGroupL a -> Bool
FreeGroupL a -> FreeGroupL a -> Ordering
FreeGroupL a -> FreeGroupL a -> FreeGroupL a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (FreeGroupL a)
forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Bool
forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Ordering
forall a. Ord a => FreeGroupL a -> FreeGroupL a -> FreeGroupL a
min :: FreeGroupL a -> FreeGroupL a -> FreeGroupL a
$cmin :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> FreeGroupL a
max :: FreeGroupL a -> FreeGroupL a -> FreeGroupL a
$cmax :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> FreeGroupL a
>= :: FreeGroupL a -> FreeGroupL a -> Bool
$c>= :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Bool
> :: FreeGroupL a -> FreeGroupL a -> Bool
$c> :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Bool
<= :: FreeGroupL a -> FreeGroupL a -> Bool
$c<= :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Bool
< :: FreeGroupL a -> FreeGroupL a -> Bool
$c< :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Bool
compare :: FreeGroupL a -> FreeGroupL a -> Ordering
$ccompare :: forall a. Ord a => FreeGroupL a -> FreeGroupL a -> Ordering
Ord)

-- | Like @'normalize'@ but for lists.
--
-- /Complexity:/ @O(n)@
--
normalizeL
    :: Eq a
    => [Either a a]
    -> [Either a a]
normalizeL :: forall a. Eq a => [Either a a] -> [Either a a]
normalizeL = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Eq a => Either a a -> [Either a a] -> [Either a a]
consL_ []

-- | Cons a generator (@'Right' x@) or its inverse (@'Left' x@) to the left
-- hand side of a 'FreeGroupL'.
--
-- /Complexity:/ @O(1)@
--
consL :: Eq a => Either a a -> FreeGroupL a -> FreeGroupL a
consL :: forall a. Eq a => Either a a -> FreeGroupL a -> FreeGroupL a
consL Either a a
a (FreeGroupL [Either a a]
as) = forall a. [Either a a] -> FreeGroupL a
FreeGroupL (forall a. Eq a => Either a a -> [Either a a] -> [Either a a]
consL_ Either a a
a [Either a a]
as)

consL_ :: Eq a => Either a a -> [Either a a] -> [Either a a]
consL_ :: forall a. Eq a => Either a a -> [Either a a] -> [Either a a]
consL_ Either a a
a [] = [Either a a
a]
consL_ Either a a
a as :: [Either a a]
as@(Either a a
b:[Either a a]
bs) = case (Either a a
a, Either a a
b) of
    (Left a
x,  Right a
y) | a
x forall a. Eq a => a -> a -> Bool
== a
y -> [Either a a]
bs
    (Right a
x, Left a
y)  | a
x forall a. Eq a => a -> a -> Bool
== a
y -> [Either a a]
bs
    (Either a a, Either a a)
_                           -> Either a a
a forall a. a -> [a] -> [a]
: [Either a a]
as

-- | Smart constructor which normalizes a list.
--
-- /Complexity:/ @O(n)@
fromList :: Eq a => [Either a a] -> FreeGroupL a
fromList :: forall a. Eq a => [Either a a] -> FreeGroupL a
fromList = forall a. [Either a a] -> FreeGroupL a
FreeGroupL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [Either a a] -> [Either a a]
normalizeL

toList :: FreeGroupL a -> [Either a a]
toList :: forall a. FreeGroupL a -> [Either a a]
toList = forall a. FreeGroupL a -> [Either a a]
runFreeGroupL

instance Eq a => Semigroup (FreeGroupL a) where
    FreeGroupL [Either a a]
as <> :: FreeGroupL a -> FreeGroupL a -> FreeGroupL a
<> FreeGroupL [Either a a]
bs = forall a. [Either a a] -> FreeGroupL a
FreeGroupL forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Eq a => Either a a -> [Either a a] -> [Either a a]
consL_ [Either a a]
bs [Either a a]
as

instance Eq a => Monoid (FreeGroupL a) where
    mempty :: FreeGroupL a
mempty = forall a. [Either a a] -> FreeGroupL a
FreeGroupL []
#if __GLASGOW_HASKELL__ <= 802
    mappend = (<>)
#endif

instance Eq a => Group (FreeGroupL a) where
    invert :: FreeGroupL a -> FreeGroupL a
invert (FreeGroupL [Either a a]
as) = forall a. [Either a a] -> FreeGroupL a
FreeGroupL forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\[Either a a]
acu Either a a
a -> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left Either a a
a forall a. a -> [a] -> [a]
: [Either a a]
acu) [] [Either a a]
as

type instance AlgebraType0 FreeGroupL a = Eq a
type instance AlgebraType  FreeGroupL g = (Eq g, Group g)
instance FreeAlgebra FreeGroupL where
    returnFree :: forall a. a -> FreeGroupL a
returnFree a
a = forall a. [Either a a] -> FreeGroupL a
FreeGroupL [forall a b. b -> Either a b
Right a
a]
    foldMapFree :: forall d a.
(AlgebraType FreeGroupL d, AlgebraType0 FreeGroupL a) =>
(a -> d) -> FreeGroupL a -> d
foldMapFree a -> d
_ (FreeGroupL []) = forall a. Monoid a => a
mempty
    foldMapFree a -> d
f (FreeGroupL (Either a a
a : [Either a a]
as)) =
        forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall m. Group m => m -> m
invert forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> d
f) a -> d
f Either a a
a forall a. Monoid a => a -> a -> a
`mappend` forall (m :: * -> *) d a.
(FreeAlgebra m, AlgebraType m d, AlgebraType0 m a) =>
(a -> d) -> m a -> d
foldMapFree a -> d
f (forall a. [Either a a] -> FreeGroupL a
FreeGroupL [Either a a]
as)