{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DerivingStrategies         #-}

--------------------------------------------------------------------------------
-- |
--
-- Module      :  Data.Act.Cyclic
-- Description :  Cyclic actions and actions generated by a subset of generators.
-- Copyright   :  (c) Alice Rixte 2024
-- License     :  BSD 3
-- Maintainer  :  alice.rixte@u-bordeaux.fr
-- Stability   :  unstable
-- Portability :  non-portable (GHC extensions)
--
-- = Presentation
--
-- === Cyclic actions
--
-- A cyclic action (see @'LActCyclic'@ or @'RActCyclic'@) is an action such that
-- every element of the actee set can be obtained by acting on some generator,
-- which we call here the /origin/ of the actee set.
--
-- For example, @'Sum' Integer@ acts cyclically on @'Integer'@ because for every
-- @n :: Integer@, we have @Sum n <>$ O == n@. In this example, @0@ is a
-- generator of the action @'LAct' Int (Sum Int)@ and in this library, we will
-- call it @'lorigin'@.
--
-- This gives us a way to lift any actee element into an action element. In this
-- library,  we call that lifting @'lshift'@  (resp. @'rshift'@). In the
-- previous example we get @'lshift' = Sum@.
--
-- === Actions generated by a subset of generators
--
-- In a more general setting, this library also provides @'LActGen'@ and
-- @'RActGen'@. In theory, they should be superclasses of @'LActCyclic'@ and
-- @'RActCyclic'@. In practice it is annoying to need @'Eq'@ instances for
-- defining @'lgenerators'@ and @'rgenerators'@. Please open an issue if you
-- actually need this.
--
--
-- = Usage
--
-- >>> {-# LANGUAGE TypeApplications #-}
-- >>> import Data.Act.Cyclic
-- >>> import Data.Semigroup
-- >>> lorigin @(Sum Int) :: Int
-- 0
-- >>> lshift (4 :: Int) :: Sum Int
-- Sum {getSum = 4}
--
-- = Formal algebraic definitions
--
-- In algebraic terms, a subset @u@ of the set @x@ is a /generating set/ of the
-- action @LAct x s@ if for every @x :: x@, there exists a pair @(u,s) :: (u,s)@
-- such that @s <>$ u = x@. When the set @u@ is finite, the action @LAct x s@ is
-- said to be finitely generated. When the set @u@ is a singleton, the action is
-- said to be /cyclic/.
--
-- When the previous decomposition is unique, the action is said to be /free/.
-- If it is both free and cyclic, it is /1-free/.
--
-- (See /Monoids, Acts and Categories/ by Mati
-- Kilp, Ulrich Knauer, Alexander V. Mikhalev, definition 1.5.1, p.63.)
--
-- Remark : Freeness could be represented with classes @LActFree@ and
-- @LActOneFree@ that have no methods. Feel free to open an issue if you need
-- them.
--------------------------------------------------------------------------------


module Data.Act.Cyclic
  ( -- * Cyclic actions
    LActCyclic (..)
  , lorigin
  , RActCyclic (..)
  , rorigin
   -- * Action generated by a subset of generators
  , LActGen (..)
  , lgenerators
  , lgeneratorsList
  , lorigins
  , RActGen (..)
  , rgenerators
  , rgeneratorsList
  , rorigins
  )
  where

import Data.Bifunctor
import Data.Functor.Identity
import Data.Coerce
import Data.Semigroup as Sg
import Data.Monoid as Mn

import Data.Default



import Data.Act.Act


-- | A left action generated by a single generator.
--
-- Instances must satisfy the following law :
--
-- * 'lshift' x @ <>$ 'lorigin' == x@
--
-- In other words, 'lorigin' is a generator of the action @LAct x s@.
--
class LAct x s => LActCyclic x s where
  -- | The only generator of the action @LAct x s@.
  --
  -- >>> lorigin' @Int @(Sum Int)
  -- 0
  --
  -- To avoid having to use the redundant first type aplication, use
  -- @'lorigin'@.
  --
  lorigin' :: x

  --- | Shifts an element of @x@ into an action @lshift x@ such that
  -- @lshift x <>$ lorigin == x@.
  --
  lshift :: x -> s

-- | A version of @'lorigin''@ such that the first type application is @s@.
--
-- >>> lorigin @(Sum Int) :: Int
-- 0
--
lorigin :: forall s x. LActCyclic x s => x
lorigin :: forall s x. LActCyclic x s => x
lorigin = forall x s. LActCyclic x s => x
lorigin' @x @s
{-# INLINE lorigin #-}


-- | A right action generated by a single generator.
--
-- Instances must satisfy the following law :
--
-- * 'rorigin' @ $<> 'rshift' x == x@
--
-- In other words, 'rorigin' is a generator of the action @RAct x s@.
--
class RAct x s => RActCyclic x s where
  -- | The only generator of the action @RAct x s@.
  --
  -- >>> rorigin' @Int @(Sum Int) :: Int
  -- 0
  --
  -- To avoid having to use the redundant first type aplication, use
  -- @'rorigin'@.
  rorigin' :: x

  -- | Shifts an element of @x@ into an action @rshift x@ such that
  -- @rshift x $<> rorigin == x@.
  rshift :: x -> s

-- | A version of @'rorigin''@ such that the first type application is @s@.
--
-- >>> rorigin @(Sum Int) :: Int
-- 0
--
rorigin :: forall s x. RActCyclic x s => x
rorigin :: forall s x. RActCyclic x s => x
rorigin = forall x s. RActCyclic x s => x
rorigin' @x @s
{-# INLINE rorigin #-}




-- | A left action generated by a subset of generators @'lgenerators'@.
--
-- Intuitively, by acting repeteadly on generators with actions
-- of @s@, we can reach any element of @x@.
--
-- Since the generating subset of @x@ maybe infinite, we give two alternative
-- ways to define it : one using a characteristic function @'lgenerators'@ and
-- the other using a list @'lgeneratorsList'@.
--
-- All the above is summarized by the following law that all instances must
-- satisfy :
--
-- 1. 'snd' @('lshiftFromGen' x) <>$ 'fst' ('lshiftFromGen' x) == x@
-- 2. 'lgenerators'@  ('fst' $ 'lshiftFromGen' x) == True@
-- 3. 'lgenerators' @ x == x `'elem'` 'lgeneratorsList' proxy@
--
class LAct x s => LActGen x s where
  -- | The set of origins of the action @'LAct' x s@.
  --
  -- This is a subset of @x@, represented as its characteristic function,
  -- meaning the function that returns @True@ for all elements of @x@ that are
  -- origins of the action and @False@ otherwise.
  --
  -- To use @'lgenerators'@, you need TypeApplications:
  --
  -- >>> lgenerators' @Int @(Sum Int) 4
  -- False
  --
  -- >>> lgenerators' @Int @(Sum Int) 0
  -- True
  --
  -- To avoid having to use the redundant first type aplication, use
  -- @'lgenerators'@.
  lgenerators' :: x -> Bool
  default lgenerators' :: Eq x => x -> Bool
  lgenerators' x
x = x
x x -> [x] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall x s. LActGen x s => [x]
lgeneratorsList' @x @s

  -- | The set of origins of the action @LAct x s@ seen as a list.
  --
  -- You can let this function undefined if the set of origins cannot be
  -- represented as a list.
  --
  -- >>> lgeneratorsList' @Int @(Sum Int)
  -- [0]
  --
  -- To avoid having to use the redundant first type aplication, use
  -- @'lgeneratorsList'@.
  --
  lgeneratorsList' :: [x]
  default lgeneratorsList' :: LActCyclic x s => [x]
  lgeneratorsList' = [forall s x. LActCyclic x s => x
lorigin @s]

  -- | Returns a point's associated genrator @u@ along with an action @s@ such
  -- that @s <>$ u == x@.
  lshiftFromGen:: x -> (x,s)
  default lshiftFromGen :: LActCyclic x s => x -> (x,s)
  lshiftFromGen x
x = (forall s x. LActCyclic x s => x
lorigin @s, x -> s
forall x s. LActCyclic x s => x -> s
lshift x
x)

-- | A version of @'lgenerators''@ such that the first type application is @s@.
--
-- >>> lgenerators @(Sum Int) (4 :: Int)
-- False
--
-- >>> lgenerators @(Sum Int) (0 :: Int)
-- True
--
lgenerators :: forall s x. LActGen x s => x -> Bool
lgenerators :: forall s x. LActGen x s => x -> Bool
lgenerators = forall x s. LActGen x s => x -> Bool
lgenerators' @x @s
{-# INLINE lgenerators #-}

-- | A version of @'lgeneratorsList''@ such that the first type application is
-- @s@.
--
-- >>> lgeneratorsList @(Sum Int) :: [Int]
-- [0]
--
lgeneratorsList :: forall s x. LActGen x s => [x]
lgeneratorsList :: forall s x. LActGen x s => [x]
lgeneratorsList = forall x s. LActGen x s => [x]
lgeneratorsList' @x @s
{-# INLINE lgeneratorsList #-}

-- | An alias for @'lgeneratorsList'@.
lorigins :: forall s x. LActGen x s => [x]
lorigins :: forall s x. LActGen x s => [x]
lorigins = forall s x. LActGen x s => [x]
lgeneratorsList @s
{-# INLINE lorigins #-}



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

-- | A right action generated by a subset of generators @'lgenerators'@.
--
-- Intuitively, by acting repeteadly on generators with actions
-- of @s@, we can reach any element of @x@.
--
--
-- Since the generating subset of @x@ maybe infinite, we give two alternative
-- ways to define it : one using a characteristic function @'rgenerators'@ and
-- the other using a list @'rgeneratorsList'@.
--
-- All the above is summarized by the following law that all instances must
-- satisfy :
--
-- 1. 'rgenerators'@  ('fst' $ 'rshiftFromGen' x) == True@
-- 2. 'fst' ('rshiftFromGen' x) $<> 'snd' @('rshiftFromGen' x) == x@
-- 3. 'rgenerators' @x == x `'elem'` 'rgeneratorsList' x@
--
class RAct x s => RActGen x s where
  -- | The set of origins of the action @'RAct' x s@.
  --
  -- This is a subset of @x@, represented as its characteristic function,
  -- meaning the function that returns @True@ for all elements of @x@ that are
  -- origins of the action and @False@ otherwise.
  --
  -- To use @'rgenerators'@, you need TypeApplications:
  --
  -- >>> rgenerators' @(Sum Int) (4 :: Int)
  -- False
  --
  -- >>> rgenerators' @(Sum Int) (0 :: Int)
  -- True
  --
  -- To avoid having to use the redundant first type aplication, use
  -- @'rgenerators'@.
  rgenerators' :: x -> Bool
  default rgenerators' :: Eq x => x -> Bool
  rgenerators' x
x = x
x x -> [x] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall x s. RActGen x s => [x]
rgeneratorsList' @x @s
  {-# INLINE rgenerators' #-}

  -- | The set of origins of the action @RAct x s@ seen as a list.
  --
  -- You can let this function undefined if the set of origins cannot be
  -- represented as a list.
  --
  -- >>> rgeneratorsList' @(Sum Int) :: [Int]
  -- [0]
  --
  rgeneratorsList' :: [x]
  default rgeneratorsList' :: RActCyclic x s => [x]
  rgeneratorsList' = [forall s x. RActCyclic x s => x
rorigin @s]
  {-# INLINE rgeneratorsList' #-}

  -- | Returns a point's associated generator @u@ along with an action @s@ such
  -- that @u $<> s == x@.
  rshiftFromGen :: x -> (x,s)
  default rshiftFromGen :: RActCyclic x s => x -> (x,s)
  rshiftFromGen x
x = (forall s x. RActCyclic x s => x
rorigin @s, x -> s
forall x s. RActCyclic x s => x -> s
rshift x
x)
  {-# INLINE rshiftFromGen #-}

-- | A version of @'rgenerators''@ such that the first type application is @s@.
--
-- >>> rgenerators @(Sum Int) (4 :: Int)
-- False
--
-- >>> rgenerators @(Sum Int) (0 :: Int)
-- True
--
rgenerators :: forall s x. RActGen x s => x -> Bool
rgenerators :: forall s x. RActGen x s => x -> Bool
rgenerators = forall x s. RActGen x s => x -> Bool
rgenerators' @x @s
{-# INLINE rgenerators #-}

-- | A version of @'rgeneratorsList''@ such that the first type application is
-- @s@.
--
-- >>> rgeneratorsList @(Sum Int) :: [Int]
-- [0]
--
rgeneratorsList :: forall s x. RActGen x s => [x]
rgeneratorsList :: forall s x. RActGen x s => [x]
rgeneratorsList = forall x s. RActGen x s => [x]
rgeneratorsList' @x @s
{-# INLINE rgeneratorsList #-}

-- | An alias for @'rgeneratorsList'@.
--
rorigins :: forall s x. RActGen x s => [x]
rorigins :: forall s x. RActGen x s => [x]
rorigins = forall s x. RActGen x s => [x]
rgeneratorsList @s
{-# INLINE rorigins #-}



---------------------------------- Instances -----------------------------------

-- Identity --

instance LActGen x s => LActGen (Identity x) (Identity s) where
  lgenerators' :: Identity x -> Bool
lgenerators' (Identity x
x) = forall s x. LActGen x s => x -> Bool
lgenerators @s x
x
  {-# INLINE lgenerators' #-}
  lgeneratorsList' :: [Identity x]
lgeneratorsList' = x -> Identity x
forall a. a -> Identity a
Identity (x -> Identity x) -> [x] -> [Identity x]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s x. LActGen x s => [x]
lgeneratorsList @s
  {-# INLINE lgeneratorsList' #-}
  lshiftFromGen :: Identity x -> (Identity x, Identity s)
lshiftFromGen (Identity x
x) = (x -> Identity x)
-> (s -> Identity s) -> (x, s) -> (Identity x, Identity s)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap x -> Identity x
forall a. a -> Identity a
Identity s -> Identity s
forall a. a -> Identity a
Identity ((x, s) -> (Identity x, Identity s))
-> (x, s) -> (Identity x, Identity s)
forall a b. (a -> b) -> a -> b
$ x -> (x, s)
forall x s. LActGen x s => x -> (x, s)
lshiftFromGen x
x
  {-# INLINE lshiftFromGen #-}

instance LActCyclic x s => LActCyclic (Identity x) (Identity s) where
  lorigin' :: Identity x
lorigin' = x -> Identity x
forall a. a -> Identity a
Identity (forall s x. LActCyclic x s => x
lorigin @s)
  {-# INLINE lorigin' #-}
  lshift :: Identity x -> Identity s
lshift (Identity x
x) = s -> Identity s
forall a. a -> Identity a
Identity (x -> s
forall x s. LActCyclic x s => x -> s
lshift x
x)
  {-# INLINE lshift #-}

instance RActGen x s => RActGen (Identity x) (Identity s) where
  rgenerators' :: Identity x -> Bool
rgenerators' (Identity x
x) = forall s x. RActGen x s => x -> Bool
rgenerators @s x
x
  {-# INLINE rgenerators' #-}
  rgeneratorsList' :: [Identity x]
rgeneratorsList' = x -> Identity x
forall a. a -> Identity a
Identity (x -> Identity x) -> [x] -> [Identity x]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s x. RActGen x s => [x]
rgeneratorsList @s
  {-# INLINE rgeneratorsList' #-}
  rshiftFromGen :: Identity x -> (Identity x, Identity s)
rshiftFromGen (Identity x
x) = (x -> Identity x)
-> (s -> Identity s) -> (x, s) -> (Identity x, Identity s)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap x -> Identity x
forall a. a -> Identity a
Identity s -> Identity s
forall a. a -> Identity a
Identity ((x, s) -> (Identity x, Identity s))
-> (x, s) -> (Identity x, Identity s)
forall a b. (a -> b) -> a -> b
$ x -> (x, s)
forall x s. RActGen x s => x -> (x, s)
rshiftFromGen x
x
  {-# INLINE rshiftFromGen #-}

instance RActCyclic x s => RActCyclic (Identity x) (Identity s) where
  rorigin' :: Identity x
rorigin' = x -> Identity x
forall a. a -> Identity a
Identity (forall s x. RActCyclic x s => x
rorigin @s)
  {-# INLINE rorigin' #-}
  rshift :: Identity x -> Identity s
rshift (Identity x
x) = s -> Identity s
forall a. a -> Identity a
Identity (x -> s
forall x s. RActCyclic x s => x -> s
rshift x
x)
  {-# INLINE rshift #-}

-- ActSelf --

instance (Eq s, Monoid s) => LActGen s (ActSelf s)

instance Monoid s => LActCyclic s (ActSelf s) where
  lorigin' :: s
lorigin' = s
forall s. Monoid s => s
mempty
  {-# INLINE lorigin' #-}
  lshift :: s -> ActSelf s
lshift = s -> ActSelf s
forall s. s -> ActSelf s
ActSelf
  {-# INLINE lshift #-}

instance (Eq s, Monoid s) => RActGen s (ActSelf s)

instance Monoid s => RActCyclic s (ActSelf s) where
  rorigin' :: s
rorigin' = s
forall s. Monoid s => s
mempty
  {-# INLINE rorigin' #-}
  rshift :: s -> ActSelf s
rshift = s -> ActSelf s
forall s. s -> ActSelf s
ActSelf
  {-# INLINE rshift #-}


-- ActSelf' --

instance (Eq x, Coercible x s, Monoid s) => LActGen x (ActSelf' s)

instance (Coercible x s, Monoid s) => LActCyclic x (ActSelf' s) where
  lorigin' :: x
lorigin' = s -> x
forall a b. Coercible a b => a -> b
coerce (s
forall s. Monoid s => s
mempty :: s)
  {-# INLINE lorigin' #-}
  lshift :: x -> ActSelf' s
lshift = x -> ActSelf' s
forall a b. Coercible a b => a -> b
coerce
  {-# INLINE lshift #-}

instance (Eq x, Coercible x s, Monoid s) => RActGen x (ActSelf' s)

instance (Coercible x s, Monoid s) => RActCyclic x (ActSelf' s) where
  rorigin' :: x
rorigin' = s -> x
forall a b. Coercible a b => a -> b
coerce (s
forall s. Monoid s => s
mempty :: s)
  {-# INLINE rorigin' #-}
  rshift :: x -> ActSelf' s
rshift = x -> ActSelf' s
forall a b. Coercible a b => a -> b
coerce
  {-# INLINE rshift #-}

-- Sum --

instance (Eq x, Num x) => LActGen x (Sum x)

instance Num x => LActCyclic x (Sum x) where
  lorigin' :: x
lorigin' = x
0
  {-# INLINE lorigin' #-}
  lshift :: x -> Sum x
lshift = x -> Sum x
forall a. a -> Sum a
Sum
  {-# INLINE lshift #-}

instance (Eq x, Num x) => RActGen x (Sum x)

instance Num x => RActCyclic x (Sum x) where
  rorigin' :: x
rorigin' = x
0
  {-# INLINE rorigin' #-}
  rshift :: x -> Sum x
rshift = x -> Sum x
forall a. a -> Sum a
Sum
  {-# INLINE rshift #-}

-- Product --

instance (Eq x, Num x) => LActGen x (Product x)

instance Num x => LActCyclic x (Product x) where
  lorigin' :: x
lorigin' = x
1
  {-# INLINE lorigin' #-}
  lshift :: x -> Product x
lshift = x -> Product x
forall a. a -> Product a
Product
  {-# INLINE lshift #-}

instance (Eq x, Num x) => RActGen x (Product x)

instance Num x => RActCyclic x (Product x) where
  rorigin' :: x
rorigin' = x
1
  {-# INLINE rorigin' #-}
  rshift :: x -> Product x
rshift = x -> Product x
forall a. a -> Product a
Product
  {-# INLINE rshift #-}

-- Product on Sum --

instance (Eq x, Num x) => LActGen (Sum x) (Product x)

instance Num x => LActCyclic (Sum x) (Product x) where
  lorigin' :: Sum x
lorigin' = Sum x
1
  {-# INLINE lorigin' #-}
  lshift :: Sum x -> Product x
lshift = Sum x -> Product x
forall a b. Coercible a b => a -> b
coerce
  {-# INLINE lshift #-}

instance (Eq x, Num x) => RActGen (Sum x) (Product x)

instance Num x => RActCyclic (Sum x) (Product x) where
  rorigin' :: Sum x
rorigin' = Sum x
1
  {-# INLINE rorigin' #-}
  rshift :: Sum x -> Product x
rshift = Sum x -> Product x
forall a b. Coercible a b => a -> b
coerce
  {-# INLINE rshift #-}

-- First --

instance Default x => LActCyclic x (Sg.First x) where
  lorigin' :: x
lorigin' = x
forall x. Default x => x
def
  lshift :: x -> First x
lshift = x -> First x
forall a. a -> First a
Sg.First

instance Default x => LActCyclic x (Mn.First x) where
  lorigin' :: x
lorigin' = x
forall x. Default x => x
def
  lshift :: x -> First x
lshift = Maybe x -> First x
forall a. Maybe a -> First a
Mn.First (Maybe x -> First x) -> (x -> Maybe x) -> x -> First x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Maybe x
forall a. a -> Maybe a
Just

instance Default x => RActCyclic x (Sg.Last x) where
  rorigin' :: x
rorigin' = x
forall x. Default x => x
def
  rshift :: x -> Last x
rshift = x -> Last x
forall a. a -> Last a
Sg.Last

instance Default x => RActCyclic x (Mn.Last x) where
  rorigin' :: x
rorigin' = x
forall x. Default x => x
def
  rshift :: x -> Last x
rshift = Maybe x -> Last x
forall a. Maybe a -> Last a
Mn.Last (Maybe x -> Last x) -> (x -> Maybe x) -> x -> Last x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Maybe x
forall a. a -> Maybe a
Just