Cyclic.hs

{-# 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 = 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 = 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 `elem` 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' = [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 = (lorigin @s, lshift 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 = 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 = lgeneratorsList' @x @s
{-# INLINE lgeneratorsList #-}

-- | An alias for @'lgeneratorsList'@.
lorigins :: forall s x. LActGen x s => [x]
lorigins = 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 `elem` 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' = [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 = (rorigin @s, rshift 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 = 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 = rgeneratorsList' @x @s
{-# INLINE rgeneratorsList #-}

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



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

-- Identity --

instance LActGen x s => LActGen (Identity x) (Identity s) where
  lgenerators' (Identity x) = lgenerators @s x
  {-# INLINE lgenerators' #-}
  lgeneratorsList' = Identity <$> lgeneratorsList @s
  {-# INLINE lgeneratorsList' #-}
  lshiftFromGen (Identity x) = bimap Identity Identity $ lshiftFromGen x
  {-# INLINE lshiftFromGen #-}

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

instance RActGen x s => RActGen (Identity x) (Identity s) where
  rgenerators' (Identity x) = rgenerators @s x
  {-# INLINE rgenerators' #-}
  rgeneratorsList' = Identity <$> rgeneratorsList @s
  {-# INLINE rgeneratorsList' #-}
  rshiftFromGen (Identity x) = bimap Identity Identity $ rshiftFromGen x
  {-# INLINE rshiftFromGen #-}

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

-- ActSelf --

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

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

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

instance Monoid s => RActCyclic s (ActSelf s) where
  rorigin' = mempty
  {-# INLINE rorigin' #-}
  rshift = 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' = coerce (mempty :: s)
  {-# INLINE lorigin' #-}
  lshift = 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' = coerce (mempty :: s)
  {-# INLINE rorigin' #-}
  rshift = coerce
  {-# INLINE rshift #-}

-- Sum --

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

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

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

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

-- Product --

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

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

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

instance Num x => RActCyclic x (Product x) where
  rorigin' = 1
  {-# INLINE rorigin' #-}
  rshift = 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' = 1
  {-# INLINE lorigin' #-}
  lshift = coerce
  {-# INLINE lshift #-}

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

instance Num x => RActCyclic (Sum x) (Product x) where
  rorigin' = 1
  {-# INLINE rorigin' #-}
  rshift = coerce
  {-# INLINE rshift #-}

-- First --

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

instance Default x => LActCyclic x (Mn.First x) where
  lorigin' = def
  lshift = Mn.First . Just

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

instance Default x => RActCyclic x (Mn.Last x) where
  rorigin' = def
  rshift = Mn.Last . Just