{-# OPTIONS_HADDOCK hide                #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE FlexibleInstances          #-}
-- | A module that abstracts out monoidal actions.
module Raaz.Core.MonoidalAction
       ( -- * Monoidal action
         -- $basics$
         LAction (..), Distributive, SemiR (..), semiRSpace, semiRMonoid
         -- ** Monoidal action on functors
       , LActionF(..), DistributiveF, TwistRF(..), twistFunctorValue, twistMonoidValue
         -- * Fields
         -- $fields$
       , FieldA, FieldM, Field, computeField, runFieldM, liftToFieldM
       ) where

import Control.Arrow
import Raaz.Core.Prelude
import Raaz.Core.Types.Pointer

------------------ Actions and Monoidal actions -----------------------

-- $basics$
--
-- Consider any instance @l@ of a length unit as a monoid under
-- addition. Length units acts on pointers by displacing them. It
-- turns out that this action is crucial in abstracting out many
-- pointer manipulations in our library. In particular, Applicative
-- parsers, memory allocators and data serialisers can be abstractly
-- captured using this action.
--
-- We start with setting up some terminology.  Our setting here is a
-- space of points (captured by the type @space@) on which a monoid
-- (captured by the type @m@) acts. The space which we are most
-- interested in is the space of pointers and the monoid that act on
-- it can be any instance of `LengthUnit` as described above.
--
-- In this module, we consider /left/ actions of monoids, although
-- right actions can be analogously defined as well. For applications
-- we have in mind, namely for parsers etc, it is sufficient to
-- restrict our attention to left actions.  The left action will be
-- written in multiplicative notation with the operator `<.>` being the
-- multiplication.

-- | A monoid @m@ acting on the left of a space. Think of a left
-- action as a multiplication with the monoid. It should satisfy the
-- law:
--
-- > 1 <.> p = p                         -- identity
-- > a <> b <.> p  = a <.> b <.> p   -- successive displacements
--
class Monoid m => LAction m space where
  (<.>) :: m -> space -> space


infixr 5 <.>


-- | Uniform action of a monoid on a functor. The laws that should
-- be satisfied are:
--
-- > 1 <<.>> fx  = fx
-- > (a <> b) <<.>> fx  = a . (b <<.>> fx)
-- > m <<.>> fmap f u = fmap f (m <<.>> u)   -- acts uniformly
class (Monoid m, Functor f) => LActionF m f where
  (<<.>>) :: m -> f a -> f a

infixr 5 <<.>>

---------------------- The semi-direct products ------------------------

-- | A left-monoid action on a monoidal-space, i.e. the space on which
-- the monoid acts is itself a monoid, is /distributive/ if it
-- satisfies the law:
--
-- > a <.> p <> q  = (a <.> p) <> (a <.> q).
--
-- The above law implies that every element @m@ is a monoid
-- homomorphism.
class (LAction m space, Monoid space) => Distributive m space

-- | The semidirect product Space ⋊ Monoid. For monoids acting on
-- monoidal spaces distributively the semi-direct product is itself a
-- monoid. It turns out that data serialisers can essentially seen as
-- a semidirect product.
data SemiR space m = SemiR space !m


instance Distributive m space => Semigroup (SemiR space m) where
  <> :: SemiR space m -> SemiR space m -> SemiR space m
(<>) (SemiR space
x m
a) (SemiR space
y m
b) = space -> m -> SemiR space m
forall space m. space -> m -> SemiR space m
SemiR (space
x space -> space -> space
forall a. Monoid a => a -> a -> a
`mappend`  (m
a m -> space -> space
forall m space. LAction m space => m -> space -> space
<.> space
y))  (m
a m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` m
b)

instance Distributive m space => Monoid (SemiR space m) where

  mempty :: SemiR space m
mempty = space -> m -> SemiR space m
forall space m. space -> m -> SemiR space m
SemiR space
forall a. Monoid a => a
mempty m
forall a. Monoid a => a
mempty
  {-# INLINE mempty #-}

  mappend :: SemiR space m -> SemiR space m -> SemiR space m
mappend = SemiR space m -> SemiR space m -> SemiR space m
forall a. Semigroup a => a -> a -> a
(<>)
  {-# INLINE mappend #-}

-- | From the an element of semi-direct product Space ⋊ Monoid return
-- the point.
semiRSpace :: SemiR space m -> space
{-# INLINE semiRSpace #-}
semiRSpace :: forall space m. SemiR space m -> space
semiRSpace (SemiR space
space m
_) = space
space

-- | From the an element of semi-direct product Space ⋊ Monoid return
-- the monoid element.
semiRMonoid :: SemiR space m -> m
{-# INLINE semiRMonoid #-}
semiRMonoid :: forall space m. SemiR space m -> m
semiRMonoid (SemiR space
_ m
m) =  m
m

--------------------------- Twisted functors ----------------------------



-- | The generalisation of distributivity to applicative
-- functors. This generalisation is what allows us to capture
-- applicative functors like parsers. For an applicative functor, and
-- a monoid acting uniformly on it, we say that the action is
-- distributive if the following laws are satisfied:
--
-- > m <<.>> (pure a) = pure a            -- pure values are stoic
-- > m <<.>> (a <*> b) = (m <<.>> a) <*> (m <<.>> b)  -- dist
class (Applicative f, LActionF m f) => DistributiveF m f

-- | The twisted functor is essentially a generalisation of
-- semi-direct product to applicative functors.
data TwistRF f m a = TwistRF (f a) !m

-- | Get the underlying functor value.
twistFunctorValue :: TwistRF f m a -> f a
twistFunctorValue :: forall (f :: * -> *) m a. TwistRF f m a -> f a
twistFunctorValue (TwistRF f a
fa m
_) = f a
fa
{-# INLINE twistFunctorValue #-}

-- | Get the underlying monoid value.
twistMonoidValue :: TwistRF f m a -> m
twistMonoidValue :: forall (f :: * -> *) m a. TwistRF f m a -> m
twistMonoidValue (TwistRF f a
_ m
m) =  m
m
{-# INLINE twistMonoidValue #-}

instance Functor f => Functor (TwistRF f m) where
  fmap :: forall a b. (a -> b) -> TwistRF f m a -> TwistRF f m b
fmap a -> b
f (TwistRF f a
x m
m) = f b -> m -> TwistRF f m b
forall (f :: * -> *) m a. f a -> m -> TwistRF f m a
TwistRF ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f f a
x) m
m

-- Proof of functor laws.
--
-- fmap id (TwistRF (x, m)) = TwistRF (fmap id x, m)
--                          = TwistRF (x, m)
--
-- fmap (f . g)  (TwistRF fx m) = TwistRF (fmap (f . g) x, m)
--                              = TwistRF (fmap f . fmap g $ x, m)
--                              = TwistRF (fmap f (fmap g x), m)
--                              = fmap f   $ TwistRF (fmap g x,  m)
--                              = (fmap f . fmap g) (TwistRF fx) m)
--

instance DistributiveF m f => Applicative (TwistRF f m) where
  pure :: forall a. a -> TwistRF f m a
pure a
a = f a -> m -> TwistRF f m a
forall (f :: * -> *) m a. f a -> m -> TwistRF f m a
TwistRF (a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a) m
forall a. Monoid a => a
mempty
  {-# INLINE pure #-}

  (TwistRF f (a -> b)
f m
mf)  <*> :: forall a b. TwistRF f m (a -> b) -> TwistRF f m a -> TwistRF f m b
<*> (TwistRF f a
val m
mval)  = f b -> m -> TwistRF f m b
forall (f :: * -> *) m a. f a -> m -> TwistRF f m a
TwistRF f b
res m
mres
    where res :: f b
res  = f (a -> b)
f f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m
mf m -> f a -> f a
forall a. m -> f a -> f a
forall m (f :: * -> *) a. LActionF m f => m -> f a -> f a
<<.>> f a
val
          mres :: m
mres = m
mf m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` m
mval

-- Consider an expression @u = u1 <*> u2 <*> ... <ur>@ where
-- ui = TwistRF fi mi
--
-- u = TwistRF f m where m = m1 <> m2 <> .. <> mr
-- f = f1 <*> m1 f2 <*> (m1 m2) f3 ...    <*> (m1 m2 .. mr-1) fr.
--
-- We will separately verify the functor part and the monoid
-- part of the  ofNow we can verify the laws of applicative
--
--


------------------------- A generic field -----------------------------------

-- $fields$
--
-- The main goal behind looking at monoidal actions are to captures
-- concrete objects of interest to us like parsers, serialisers and
-- memory allocators. These are essentially functions with domain
-- `Ptr`. For example, a parser is a function that takes a `Ptr`,
-- reads @n@ bytes say and produces a result a. To sequence the next
-- parse we need to essentially keep track of this @n@. If we abstract
-- this out to the general setting we need to consider functions whose
-- domain is the space of points. We use the physicist's terminology
-- and call them fields. The action of the monoid on a space of points
-- naturally extends to fields on them
--
-- @F^g   = λ x -> F (x^g) @
--
-- For our applications, we need to define generalised fields
-- associated with arrows. This is because we often have to deal with
-- functions that have side effects (i.e. `Kleisli` arrows). However,
-- for conceptual understanding, it is sufficient to stick to ordinary
-- functions. In fact, the informal proofs that we have scattered in
-- the source all have been written only for the arrow @->@.

-- | A field on the space is a function from the points in the space
-- to some value. Here we define it for a general arrow.

type FieldA arrow = WrappedArrow arrow


-- | A field where the underlying arrow is the (->). This is normally
-- what we call a field.
type Field = FieldA (->)

-- | Compute the value of a field at a given point in the space.
computeField :: Field space b -> space -> b
computeField :: forall space b. Field space b -> space -> b
computeField = WrappedArrow (->) space b -> space -> b
forall (a :: * -> * -> *) b c. WrappedArrow a b c -> a b c
unwrapArrow
{-# INLINE computeField #-}

-- | A monadic arrow field.
type FieldM monad = FieldA (Kleisli monad)

-- | Lift a monadic action to FieldM.
liftToFieldM :: (a -> m b) -> FieldM m a b
liftToFieldM :: forall a (m :: * -> *) b. (a -> m b) -> FieldM m a b
liftToFieldM = Kleisli m a b -> WrappedArrow (Kleisli m) a b
forall (a :: * -> * -> *) b c. a b c -> WrappedArrow a b c
WrapArrow (Kleisli m a b -> WrappedArrow (Kleisli m) a b)
-> ((a -> m b) -> Kleisli m a b)
-> (a -> m b)
-> WrappedArrow (Kleisli m) a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m b) -> Kleisli m a b
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli
{-# INLINE liftToFieldM #-}
-- | Runs a monadic field at a given point in the space.
runFieldM :: FieldM monad space b -> space -> monad b
runFieldM :: forall (monad :: * -> *) space b.
FieldM monad space b -> space -> monad b
runFieldM = Kleisli monad space b -> space -> monad b
forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli (Kleisli monad space b -> space -> monad b)
-> (FieldM monad space b -> Kleisli monad space b)
-> FieldM monad space b
-> space
-> monad b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldM monad space b -> Kleisli monad space b
forall (a :: * -> * -> *) b c. WrappedArrow a b c -> a b c
unwrapArrow
{-# INLINE runFieldM #-}

-- | The action on the space translates to the action on field.
instance (Arrow arrow, LAction m space) => LActionF m (WrappedArrow arrow space) where
  m
m <<.>> :: forall a.
m -> WrappedArrow arrow space a -> WrappedArrow arrow space a
<<.>> WrappedArrow arrow space a
field =   arrow space a -> WrappedArrow arrow space a
forall (a :: * -> * -> *) b c. a b c -> WrappedArrow a b c
WrapArrow (arrow space a -> WrappedArrow arrow space a)
-> arrow space a -> WrappedArrow arrow space a
forall a b. (a -> b) -> a -> b
$ WrappedArrow arrow space a -> arrow space a
forall (a :: * -> * -> *) b c. WrappedArrow a b c -> a b c
unwrapArrow WrappedArrow arrow space a
field arrow space a -> (space -> space) -> arrow space a
forall (a :: * -> * -> *) c d b.
Arrow a =>
a c d -> (b -> c) -> a b d
<<^ (m
mm -> space -> space
forall m space. LAction m space => m -> space -> space
<.>)
  {-# INLINE (<<.>>) #-}

instance (Arrow arrow, LAction m space) => DistributiveF m (WrappedArrow arrow space)

-- | The most interesting monoidal action for us.
instance LengthUnit u => LAction u (Ptr a) where
  u
a <.> :: u -> Ptr a -> Ptr a
<.> Ptr a
ptr  = Ptr a -> u -> Ptr a
forall l a. LengthUnit l => Ptr a -> l -> Ptr a
movePtr Ptr a
ptr u
a
  {-# INLINE (<.>) #-}