-- |
-- Module       : Data.Group.Free.Product
-- Copyright    : (c) 2020-2021 Reed Mullanix, 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 the 'FreeProduct' of two groups,
-- along with useful combinators.
--
module Data.Group.Free.Product
( FreeProduct(..)
, simplify
, coproduct
, injl
, injr
) where

import Data.Bifunctor
import Data.Group
import Data.Group.Order

import Data.Sequence (Seq(..))
import qualified Data.Sequence as Seq


-- -------------------------------------------------------------------- --
-- Free products

-- | The free product on two alphabets
--
-- __Note:__ This does not perform simplification upon multiplication or construction.
-- To do this, one should use 'simplify'.
--
newtype FreeProduct g h = FreeProduct { FreeProduct g h -> Seq (Either g h)
runFreeProduct :: Seq (Either g h) }
  deriving (Int -> FreeProduct g h -> ShowS
[FreeProduct g h] -> ShowS
FreeProduct g h -> String
(Int -> FreeProduct g h -> ShowS)
-> (FreeProduct g h -> String)
-> ([FreeProduct g h] -> ShowS)
-> Show (FreeProduct g h)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall g h. (Show g, Show h) => Int -> FreeProduct g h -> ShowS
forall g h. (Show g, Show h) => [FreeProduct g h] -> ShowS
forall g h. (Show g, Show h) => FreeProduct g h -> String
showList :: [FreeProduct g h] -> ShowS
$cshowList :: forall g h. (Show g, Show h) => [FreeProduct g h] -> ShowS
show :: FreeProduct g h -> String
$cshow :: forall g h. (Show g, Show h) => FreeProduct g h -> String
showsPrec :: Int -> FreeProduct g h -> ShowS
$cshowsPrec :: forall g h. (Show g, Show h) => Int -> FreeProduct g h -> ShowS
Show, FreeProduct g h -> FreeProduct g h -> Bool
(FreeProduct g h -> FreeProduct g h -> Bool)
-> (FreeProduct g h -> FreeProduct g h -> Bool)
-> Eq (FreeProduct g h)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall g h.
(Eq g, Eq h) =>
FreeProduct g h -> FreeProduct g h -> Bool
/= :: FreeProduct g h -> FreeProduct g h -> Bool
$c/= :: forall g h.
(Eq g, Eq h) =>
FreeProduct g h -> FreeProduct g h -> Bool
== :: FreeProduct g h -> FreeProduct g h -> Bool
$c== :: forall g h.
(Eq g, Eq h) =>
FreeProduct g h -> FreeProduct g h -> Bool
Eq, Eq (FreeProduct g h)
Eq (FreeProduct g h)
-> (FreeProduct g h -> FreeProduct g h -> Ordering)
-> (FreeProduct g h -> FreeProduct g h -> Bool)
-> (FreeProduct g h -> FreeProduct g h -> Bool)
-> (FreeProduct g h -> FreeProduct g h -> Bool)
-> (FreeProduct g h -> FreeProduct g h -> Bool)
-> (FreeProduct g h -> FreeProduct g h -> FreeProduct g h)
-> (FreeProduct g h -> FreeProduct g h -> FreeProduct g h)
-> Ord (FreeProduct g h)
FreeProduct g h -> FreeProduct g h -> Bool
FreeProduct g h -> FreeProduct g h -> Ordering
FreeProduct g h -> FreeProduct g h -> FreeProduct g h
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 g h. (Ord g, Ord h) => Eq (FreeProduct g h)
forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Bool
forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Ordering
forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> FreeProduct g h
min :: FreeProduct g h -> FreeProduct g h -> FreeProduct g h
$cmin :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> FreeProduct g h
max :: FreeProduct g h -> FreeProduct g h -> FreeProduct g h
$cmax :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> FreeProduct g h
>= :: FreeProduct g h -> FreeProduct g h -> Bool
$c>= :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Bool
> :: FreeProduct g h -> FreeProduct g h -> Bool
$c> :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Bool
<= :: FreeProduct g h -> FreeProduct g h -> Bool
$c<= :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Bool
< :: FreeProduct g h -> FreeProduct g h -> Bool
$c< :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Bool
compare :: FreeProduct g h -> FreeProduct g h -> Ordering
$ccompare :: forall g h.
(Ord g, Ord h) =>
FreeProduct g h -> FreeProduct g h -> Ordering
$cp1Ord :: forall g h. (Ord g, Ord h) => Eq (FreeProduct g h)
Ord)

instance Functor (FreeProduct g) where
  fmap :: (a -> b) -> FreeProduct g a -> FreeProduct g b
fmap a -> b
f = Seq (Either g b) -> FreeProduct g b
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either g b) -> FreeProduct g b)
-> (FreeProduct g a -> Seq (Either g b))
-> FreeProduct g a
-> FreeProduct g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either g a -> Either g b) -> Seq (Either g a) -> Seq (Either g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> Either g a -> Either g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (Seq (Either g a) -> Seq (Either g b))
-> (FreeProduct g a -> Seq (Either g a))
-> FreeProduct g a
-> Seq (Either g b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeProduct g a -> Seq (Either g a)
forall g h. FreeProduct g h -> Seq (Either g h)
runFreeProduct

instance Bifunctor FreeProduct where
  bimap :: (a -> b) -> (c -> d) -> FreeProduct a c -> FreeProduct b d
bimap a -> b
f c -> d
g = Seq (Either b d) -> FreeProduct b d
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either b d) -> FreeProduct b d)
-> (FreeProduct a c -> Seq (Either b d))
-> FreeProduct a c
-> FreeProduct b d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either a c -> Either b d) -> Seq (Either a c) -> Seq (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
f c -> d
g) (Seq (Either a c) -> Seq (Either b d))
-> (FreeProduct a c -> Seq (Either a c))
-> FreeProduct a c
-> Seq (Either b d)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeProduct a c -> Seq (Either a c)
forall g h. FreeProduct g h -> Seq (Either g h)
runFreeProduct

-- | /O(n)/ Simplifies a word in a 'FreeProduct'.
-- This means that we get rid of any identity elements, and perform multiplication of neighboring @g@s and @h@s.
--
simplify :: (Eq g, Eq h, Monoid g, Monoid h) => FreeProduct g h -> FreeProduct g h
simplify :: FreeProduct g h -> FreeProduct g h
simplify (FreeProduct Seq (Either g h)
fp) = Seq (Either g h) -> FreeProduct g h
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either g h) -> FreeProduct g h)
-> Seq (Either g h) -> FreeProduct g h
forall a b. (a -> b) -> a -> b
$ Seq (Either g h) -> Seq (Either g h)
forall a b.
(Eq a, Eq b, Monoid a, Monoid b) =>
Seq (Either a b) -> Seq (Either a b)
go Seq (Either g h)
fp
  where
    go :: Seq (Either a b) -> Seq (Either a b)
go (Left a
IdentityElem :<| Seq (Either a b)
ghs) = Seq (Either a b) -> Seq (Either a b)
go Seq (Either a b)
ghs
    go (Right b
IdentityElem :<| Seq (Either a b)
ghs) = Seq (Either a b) -> Seq (Either a b)
go Seq (Either a b)
ghs
    go (Left a
g :<| Left a
g' :<| Seq (Either a b)
ghs) = Seq (Either a b) -> Seq (Either a b)
go (Seq (Either a b) -> Seq (Either a b))
-> Seq (Either a b) -> Seq (Either a b)
forall a b. (a -> b) -> a -> b
$ a -> Either a b
forall a b. a -> Either a b
Left (a
g a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
g') Either a b -> Seq (Either a b) -> Seq (Either a b)
forall a. a -> Seq a -> Seq a
:<| Seq (Either a b)
ghs
    go (Right b
h :<| Right b
h' :<| Seq (Either a b)
ghs) = Seq (Either a b) -> Seq (Either a b)
go (Seq (Either a b) -> Seq (Either a b))
-> Seq (Either a b) -> Seq (Either a b)
forall a b. (a -> b) -> a -> b
$ b -> Either a b
forall a b. b -> Either a b
Right (b
h b -> b -> b
forall a. Semigroup a => a -> a -> a
<> b
h') Either a b -> Seq (Either a b) -> Seq (Either a b)
forall a. a -> Seq a -> Seq a
:<| Seq (Either a b)
ghs
    go (Either a b
gh :<| Seq (Either a b)
ghs) = Either a b
gh Either a b -> Seq (Either a b) -> Seq (Either a b)
forall a. a -> Seq a -> Seq a
:<| Seq (Either a b) -> Seq (Either a b)
go Seq (Either a b)
ghs
    go Seq (Either a b)
Empty = Seq (Either a b)
forall a. Seq a
Empty

instance Semigroup (FreeProduct g h) where
  FreeProduct Seq (Either g h)
ghs <> :: FreeProduct g h -> FreeProduct g h -> FreeProduct g h
<> FreeProduct Seq (Either g h)
ghs' = Seq (Either g h) -> FreeProduct g h
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either g h) -> FreeProduct g h)
-> Seq (Either g h) -> FreeProduct g h
forall a b. (a -> b) -> a -> b
$ Seq (Either g h)
ghs Seq (Either g h) -> Seq (Either g h) -> Seq (Either g h)
forall a. Semigroup a => a -> a -> a
<> Seq (Either g h)
ghs'

instance Monoid (FreeProduct g h) where
  mempty :: FreeProduct g h
mempty = Seq (Either g h) -> FreeProduct g h
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct Seq (Either g h)
forall a. Seq a
Seq.empty

instance (Group g, Group h) => Group (FreeProduct g h) where
  invert :: FreeProduct g h -> FreeProduct g h
invert (FreeProduct Seq (Either g h)
ghs) = Seq (Either g h) -> FreeProduct g h
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either g h) -> FreeProduct g h)
-> Seq (Either g h) -> FreeProduct g h
forall a b. (a -> b) -> a -> b
$ (g -> g) -> (h -> h) -> Either g h -> Either g h
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap g -> g
forall m. Group m => m -> m
invert h -> h
forall m. Group m => m -> m
invert (Either g h -> Either g h) -> Seq (Either g h) -> Seq (Either g h)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (Either g h) -> Seq (Either g h)
forall a. Seq a -> Seq a
Seq.reverse Seq (Either g h)
ghs

instance (GroupOrder g, GroupOrder h) => GroupOrder (FreeProduct g h) where
  -- TODO: It performs simplify each time @order@ is called.
  --   Once "auto-simplify" is implemented, this
  --   call of simplify should be removed.
  order :: FreeProduct g h -> Order
order = Seq (Either g h) -> Order
forall a a.
(GroupOrder a, GroupOrder a) =>
Seq (Either a a) -> Order
go (Seq (Either g h) -> Order)
-> (FreeProduct g h -> Seq (Either g h))
-> FreeProduct g h
-> Order
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeProduct g h -> Seq (Either g h)
forall g h. FreeProduct g h -> Seq (Either g h)
runFreeProduct (FreeProduct g h -> Seq (Either g h))
-> (FreeProduct g h -> FreeProduct g h)
-> FreeProduct g h
-> Seq (Either g h)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeProduct g h -> FreeProduct g h
forall g h.
(Eq g, Eq h, Monoid g, Monoid h) =>
FreeProduct g h -> FreeProduct g h
simplify
    where
      go :: Seq (Either a a) -> Order
go Seq (Either a a)
Seq.Empty         = Natural -> Order
Finite Natural
1
      go (Either a a
x :<| Seq (Either a a)
Seq.Empty) = (a -> Order) -> (a -> Order) -> Either a a -> Order
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Order
forall g. GroupOrder g => g -> Order
order a -> Order
forall g. GroupOrder g => g -> Order
order Either a a
x
      go (Left a
g :<| (Seq (Either a a)
ghs :|> Left a
g'))
        | a
g a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
g' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Monoid a => a
mempty = Seq (Either a a) -> Order
go Seq (Either a a)
ghs
      go (Right a
h :<| (Seq (Either a a)
ghs :|> Right a
h'))
        | a
h a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
h' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Monoid a => a
mempty = Seq (Either a a) -> Order
go Seq (Either a a)
ghs
      go Seq (Either a a)
_ = Order
Infinite

-- | Left injection of an alphabet @a@ into a free product.
--
injl :: a -> FreeProduct a b
injl :: a -> FreeProduct a b
injl a
a = Seq (Either a b) -> FreeProduct a b
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either a b) -> FreeProduct a b)
-> Seq (Either a b) -> FreeProduct a b
forall a b. (a -> b) -> a -> b
$ Either a b -> Seq (Either a b)
forall a. a -> Seq a
Seq.singleton (a -> Either a b
forall a b. a -> Either a b
Left a
a)

-- | Right injection of an alphabet @b@ into a free product.
--
injr :: b -> FreeProduct a b
injr :: b -> FreeProduct a b
injr b
b = Seq (Either a b) -> FreeProduct a b
forall g h. Seq (Either g h) -> FreeProduct g h
FreeProduct (Seq (Either a b) -> FreeProduct a b)
-> Seq (Either a b) -> FreeProduct a b
forall a b. (a -> b) -> a -> b
$ Either a b -> Seq (Either a b)
forall a. a -> Seq a
Seq.singleton (b -> Either a b
forall a b. b -> Either a b
Right b
b)

-- | The 'FreeProduct' of two 'Monoid's is a coproduct in the category of monoids (and by extension, the category of groups).
--
coproduct :: Monoid m => (a -> m) -> (b -> m) -> FreeProduct a b -> m
coproduct :: (a -> m) -> (b -> m) -> FreeProduct a b -> m
coproduct a -> m
gi b -> m
hi (FreeProduct Seq (Either a b)
ghs) = (Either a b -> m) -> Seq (Either a b) -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> (b -> m) -> Either a b -> m
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> m
gi b -> m
hi) Seq (Either a b)
ghs