{-# LANGUAGE FlexibleInstances            #-}
{-# LANGUAGE MultiParamTypeClasses        #-}
{-# LANGUAGE InstanceSigs                 #-}
{-# LANGUAGE ScopedTypeVariables          #-}

-----------------------------------------------------------------------------
-- |
-- Module      : Data.Semidirect.Lazy
-- Description : Lazy semidirect products
-- Copyright   : (c) Alice Rixte 2025
-- License     : BSD 3
-- Maintainer  : alice.rixte@u-bordeaux.fr
-- Stability   : unstable
-- Portability : non-portable (GHC extensions)
--
-- Semidirect products for left and right actions.
--
-- For a strict version, see @'Data.Semidirect.Strict'@.
--
-- [Usage :]
--
-- >>> import Data.Semigroup
-- >>> LSemidirect (Sum 1) (Product 2) <> LSemidirect (Sum (3 :: Int)) (Product (4 :: Int))
-- LSemidirect {lactee = Sum {getSum = 7}, lactor = Product {getProduct = 8}}
--
-- [Property checking :]
--
-- There is a @'Semigroup'@ instance for @'LSemidirect'@ (resp. @'RSemidirect'@)
-- only if there is a @'LActSgMorph'@ (resp. @'RActSgMorph'@) instance. For
-- example, @'Sum' Int@ acting on itself is not a semigroup action by morphism
-- and therefore the semidirect product is not associative :
--
-- >>> LSemidirect (Sum 1) (Sum 2) <> LSemidirect (Sum (3 :: Int)) (Sum (4 :: Int))
-- No instance for `LActDistrib (Sum Int) (Sum Int)'
--   arising from a use of `<>'
--
-----------------------------------------------------------------------------

module Data.Semidirect.Lazy
       ( LSemidirect (..)
       , lerase
       , lforget
       , lembedActee
       , lembedActor
       , lfromPair
        , RSemidirect (..)
        , rerase
        , rforget
        , rembedActee
        , rembedActor
        , rfromPair
       ) where

import Data.Bifunctor
import Data.Act

-- | A semi-direct product for a left action, where @s@ acts on @x@
--
data LSemidirect x s = LSemidirect
  { forall x s. LSemidirect x s -> x
lactee :: x -- ^ The value being acted on
  , forall x s. LSemidirect x s -> s
lactor :: s -- ^ The acting element
  }
  deriving (Int -> LSemidirect x s -> ShowS
[LSemidirect x s] -> ShowS
LSemidirect x s -> String
(Int -> LSemidirect x s -> ShowS)
-> (LSemidirect x s -> String)
-> ([LSemidirect x s] -> ShowS)
-> Show (LSemidirect x s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall x s. (Show x, Show s) => Int -> LSemidirect x s -> ShowS
forall x s. (Show x, Show s) => [LSemidirect x s] -> ShowS
forall x s. (Show x, Show s) => LSemidirect x s -> String
$cshowsPrec :: forall x s. (Show x, Show s) => Int -> LSemidirect x s -> ShowS
showsPrec :: Int -> LSemidirect x s -> ShowS
$cshow :: forall x s. (Show x, Show s) => LSemidirect x s -> String
show :: LSemidirect x s -> String
$cshowList :: forall x s. (Show x, Show s) => [LSemidirect x s] -> ShowS
showList :: [LSemidirect x s] -> ShowS
Show, ReadPrec [LSemidirect x s]
ReadPrec (LSemidirect x s)
Int -> ReadS (LSemidirect x s)
ReadS [LSemidirect x s]
(Int -> ReadS (LSemidirect x s))
-> ReadS [LSemidirect x s]
-> ReadPrec (LSemidirect x s)
-> ReadPrec [LSemidirect x s]
-> Read (LSemidirect x s)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall x s. (Read x, Read s) => ReadPrec [LSemidirect x s]
forall x s. (Read x, Read s) => ReadPrec (LSemidirect x s)
forall x s. (Read x, Read s) => Int -> ReadS (LSemidirect x s)
forall x s. (Read x, Read s) => ReadS [LSemidirect x s]
$creadsPrec :: forall x s. (Read x, Read s) => Int -> ReadS (LSemidirect x s)
readsPrec :: Int -> ReadS (LSemidirect x s)
$creadList :: forall x s. (Read x, Read s) => ReadS [LSemidirect x s]
readList :: ReadS [LSemidirect x s]
$creadPrec :: forall x s. (Read x, Read s) => ReadPrec (LSemidirect x s)
readPrec :: ReadPrec (LSemidirect x s)
$creadListPrec :: forall x s. (Read x, Read s) => ReadPrec [LSemidirect x s]
readListPrec :: ReadPrec [LSemidirect x s]
Read, LSemidirect x s -> LSemidirect x s -> Bool
(LSemidirect x s -> LSemidirect x s -> Bool)
-> (LSemidirect x s -> LSemidirect x s -> Bool)
-> Eq (LSemidirect x s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall x s.
(Eq x, Eq s) =>
LSemidirect x s -> LSemidirect x s -> Bool
$c== :: forall x s.
(Eq x, Eq s) =>
LSemidirect x s -> LSemidirect x s -> Bool
== :: LSemidirect x s -> LSemidirect x s -> Bool
$c/= :: forall x s.
(Eq x, Eq s) =>
LSemidirect x s -> LSemidirect x s -> Bool
/= :: LSemidirect x s -> LSemidirect x s -> Bool
Eq)

instance LActSgMorph x s
  => Semigroup (LSemidirect x s) where
  ~(LSemidirect x
x s
s) <> :: LSemidirect x s -> LSemidirect x s -> LSemidirect x s
<> ~(LSemidirect x
x' s
s') =
    x -> s -> LSemidirect x s
forall x s. x -> s -> LSemidirect x s
LSemidirect  (x
x x -> x -> x
forall a. Semigroup a => a -> a -> a
<> (s
s s -> x -> x
forall x s. LAct x s => s -> x -> x
<>$ x
x')) (s
s s -> s -> s
forall a. Semigroup a => a -> a -> a
<> s
s')

instance LActMnMorph x s => Monoid (LSemidirect x s) where
  mempty :: LSemidirect x s
mempty = x -> s -> LSemidirect x s
forall x s. x -> s -> LSemidirect x s
LSemidirect x
forall a. Monoid a => a
mempty s
forall a. Monoid a => a
mempty

instance Functor (LSemidirect x) where
  fmap :: forall a b. (a -> b) -> LSemidirect x a -> LSemidirect x b
fmap a -> b
f LSemidirect x a
a = LSemidirect x a
a {lactor = f (lactor a)}

instance Bifunctor LSemidirect where
  first :: forall a b c. (a -> b) -> LSemidirect a c -> LSemidirect b c
first a -> b
f LSemidirect a c
a = LSemidirect a c
a {lactee = f (lactee a)}
  second :: forall b c a. (b -> c) -> LSemidirect a b -> LSemidirect a c
second = (b -> c) -> LSemidirect a b -> LSemidirect a c
forall a b. (a -> b) -> LSemidirect a a -> LSemidirect a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

-- |  Erases the actee (i.e. replace it with @mempty@).
lerase :: Monoid x => LSemidirect x s -> LSemidirect x s
lerase :: forall x s. Monoid x => LSemidirect x s -> LSemidirect x s
lerase LSemidirect x s
a = LSemidirect x s
a {lactee = mempty}

-- |  Forget the actor (i.e. replace it with @mempty@).
lforget :: Monoid s => LSemidirect x s -> LSemidirect x s
lforget :: forall s x. Monoid s => LSemidirect x s -> LSemidirect x s
lforget LSemidirect x s
a =LSemidirect x s
a {lactor = mempty}

-- |  Make a semidirect pair whose actee is @mempty@.
lembedActor :: Monoid x => s -> LSemidirect x s
lembedActor :: forall x s. Monoid x => s -> LSemidirect x s
lembedActor s
s = x -> s -> LSemidirect x s
forall x s. x -> s -> LSemidirect x s
LSemidirect x
forall a. Monoid a => a
mempty s
s

-- |  Make a semidirect pair whose actor is @mempty@.
lembedActee :: Monoid s => x -> LSemidirect x s
lembedActee :: forall s x. Monoid s => x -> LSemidirect x s
lembedActee x
x = x -> s -> LSemidirect x s
forall x s. x -> s -> LSemidirect x s
LSemidirect x
x s
forall a. Monoid a => a
mempty

-- | Converts a pair into a semidirect product element.
lfromPair :: (x,s) -> LSemidirect x s
lfromPair :: forall x s. (x, s) -> LSemidirect x s
lfromPair (x
x,s
s) = x -> s -> LSemidirect x s
forall x s. x -> s -> LSemidirect x s
LSemidirect x
x s
s


------------------------------------------------------------------------------

-- |  A semidirect product for a right action, where @s@ acts on @x@
--
data RSemidirect x s = RSemidirect
  { forall x s. RSemidirect x s -> x
ractee :: x -- ^ The value being acted on
  , forall x s. RSemidirect x s -> s
ractor :: s -- ^ The acting element
  }
  deriving (Int -> RSemidirect x s -> ShowS
[RSemidirect x s] -> ShowS
RSemidirect x s -> String
(Int -> RSemidirect x s -> ShowS)
-> (RSemidirect x s -> String)
-> ([RSemidirect x s] -> ShowS)
-> Show (RSemidirect x s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall x s. (Show x, Show s) => Int -> RSemidirect x s -> ShowS
forall x s. (Show x, Show s) => [RSemidirect x s] -> ShowS
forall x s. (Show x, Show s) => RSemidirect x s -> String
$cshowsPrec :: forall x s. (Show x, Show s) => Int -> RSemidirect x s -> ShowS
showsPrec :: Int -> RSemidirect x s -> ShowS
$cshow :: forall x s. (Show x, Show s) => RSemidirect x s -> String
show :: RSemidirect x s -> String
$cshowList :: forall x s. (Show x, Show s) => [RSemidirect x s] -> ShowS
showList :: [RSemidirect x s] -> ShowS
Show, ReadPrec [RSemidirect x s]
ReadPrec (RSemidirect x s)
Int -> ReadS (RSemidirect x s)
ReadS [RSemidirect x s]
(Int -> ReadS (RSemidirect x s))
-> ReadS [RSemidirect x s]
-> ReadPrec (RSemidirect x s)
-> ReadPrec [RSemidirect x s]
-> Read (RSemidirect x s)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall x s. (Read x, Read s) => ReadPrec [RSemidirect x s]
forall x s. (Read x, Read s) => ReadPrec (RSemidirect x s)
forall x s. (Read x, Read s) => Int -> ReadS (RSemidirect x s)
forall x s. (Read x, Read s) => ReadS [RSemidirect x s]
$creadsPrec :: forall x s. (Read x, Read s) => Int -> ReadS (RSemidirect x s)
readsPrec :: Int -> ReadS (RSemidirect x s)
$creadList :: forall x s. (Read x, Read s) => ReadS [RSemidirect x s]
readList :: ReadS [RSemidirect x s]
$creadPrec :: forall x s. (Read x, Read s) => ReadPrec (RSemidirect x s)
readPrec :: ReadPrec (RSemidirect x s)
$creadListPrec :: forall x s. (Read x, Read s) => ReadPrec [RSemidirect x s]
readListPrec :: ReadPrec [RSemidirect x s]
Read, RSemidirect x s -> RSemidirect x s -> Bool
(RSemidirect x s -> RSemidirect x s -> Bool)
-> (RSemidirect x s -> RSemidirect x s -> Bool)
-> Eq (RSemidirect x s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall x s.
(Eq x, Eq s) =>
RSemidirect x s -> RSemidirect x s -> Bool
$c== :: forall x s.
(Eq x, Eq s) =>
RSemidirect x s -> RSemidirect x s -> Bool
== :: RSemidirect x s -> RSemidirect x s -> Bool
$c/= :: forall x s.
(Eq x, Eq s) =>
RSemidirect x s -> RSemidirect x s -> Bool
/= :: RSemidirect x s -> RSemidirect x s -> Bool
Eq)

instance RActSgMorph x s
  => Semigroup (RSemidirect x s) where
  ~(RSemidirect x
x s
s) <> :: RSemidirect x s -> RSemidirect x s -> RSemidirect x s
<> ~(RSemidirect x
x' s
s') =
    x -> s -> RSemidirect x s
forall x s. x -> s -> RSemidirect x s
RSemidirect  (x
x x -> x -> x
forall a. Semigroup a => a -> a -> a
<> (x
x' x -> s -> x
forall x s. RAct x s => x -> s -> x
$<> s
s)) (s
s s -> s -> s
forall a. Semigroup a => a -> a -> a
<> s
s')

instance RActMnMorph x s => Monoid (RSemidirect x s) where
  mempty :: RSemidirect x s
mempty = x -> s -> RSemidirect x s
forall x s. x -> s -> RSemidirect x s
RSemidirect x
forall a. Monoid a => a
mempty s
forall a. Monoid a => a
mempty

instance Functor (RSemidirect x) where
  fmap :: forall a b. (a -> b) -> RSemidirect x a -> RSemidirect x b
fmap a -> b
f RSemidirect x a
a = RSemidirect x a
a {ractor = f (ractor a)}

instance Bifunctor RSemidirect where
  first :: forall a b c. (a -> b) -> RSemidirect a c -> RSemidirect b c
first a -> b
f RSemidirect a c
a = RSemidirect a c
a {ractee = f (ractee a)}
  second :: forall b c a. (b -> c) -> RSemidirect a b -> RSemidirect a c
second = (b -> c) -> RSemidirect a b -> RSemidirect a c
forall a b. (a -> b) -> RSemidirect a a -> RSemidirect a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

-- |  Erase the actee (i.e. replace it with @mempty@).
rerase :: Monoid x => RSemidirect x s -> RSemidirect x s
rerase :: forall x s. Monoid x => RSemidirect x s -> RSemidirect x s
rerase RSemidirect x s
a = RSemidirect x s
a {ractee = mempty}

-- |  Forget the actor (i.e. replace it with @mempty@).
rforget :: Monoid s => RSemidirect x s -> RSemidirect x s
rforget :: forall s x. Monoid s => RSemidirect x s -> RSemidirect x s
rforget RSemidirect x s
a = RSemidirect x s
a {ractor = mempty}

-- |  Make a semidirect pair whose actee is @mempty@.
rembedActor :: Monoid x => s -> RSemidirect x s
rembedActor :: forall x s. Monoid x => s -> RSemidirect x s
rembedActor s
s = x -> s -> RSemidirect x s
forall x s. x -> s -> RSemidirect x s
RSemidirect x
forall a. Monoid a => a
mempty s
s

-- |  Make a semidirect pair whose actor element is @mempty@ .
rembedActee :: Monoid s => x -> RSemidirect x s
rembedActee :: forall s x. Monoid s => x -> RSemidirect x s
rembedActee x
x = x -> s -> RSemidirect x s
forall x s. x -> s -> RSemidirect x s
RSemidirect x
x s
forall a. Monoid a => a
mempty

-- | Convert a pair into a semidirect product element
rfromPair :: (x,s) -> RSemidirect x s
rfromPair :: forall x s. (x, s) -> RSemidirect x s
rfromPair (x
x,s
s) = x -> s -> RSemidirect x s
forall x s. x -> s -> RSemidirect x s
RSemidirect x
x s
s