{-# LANGUAGE PolyKinds #-}
module Barbies.Internal.MonadT
  ( MonadT(..)
  )
where

import Barbies.Internal.FunctorT(FunctorT(..))

import Control.Applicative (Alternative(..))
import Control.Applicative.Lift as Lift (Lift(..))
import Control.Applicative.Backwards as Backwards (Backwards(..))
import Control.Monad (join)
import Control.Monad.Trans.Identity(IdentityT(..))
import Control.Monad.Trans.Reader(ReaderT(..))

import Data.Coerce (coerce)
import Data.Functor.Compose (Compose(..))
import Data.Functor.Reverse (Reverse(..))
import Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))

-- | Some endo-functors on indexed-types are monads. Common examples would be
--   "functor-transformers", like 'Compose' or 'ReaderT'. In that sense, 'MonadT'
--   is similar to 'Control.Monad.Trans.Class.MonadTrans' but with additional
--   structure (see also <https://hackage.haskell.org.package/mmorph mmorph>'s
--   @MMonad@ class).
--
--   Notice though that while 'Control.Monad.Trans.Class.lift' assumes
--   a 'Monad' instance of the value to be lifted, 'tlift' has no such constraint.
--   This means we cannot have instances for most "monad transformers", since
--   lifting typically involves an 'fmap'.
--
--   'MonadT' also corresponds to the indexed-monad of
--   <https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf Kleisli arrows of outrageous fortune>.
--
--   Instances of this class should to satisfy the monad laws. They laws can stated
--   either in terms of @('tlift', 'tjoin')@ or @('tlift', 'tembed')@. In the former:
--
-- @
-- 'tmap' h . 'tlift' = 'tlift' . h
-- 'tmap' h . 'tjoin' = 'tjoin' . 'tmap' ('tmap' h)
-- 'tjoin' . 'tlift'  = 'id'
-- 'tjoin' . 'tmap tlift' = 'id'
-- 'tjoin' . 'tjoin' = 'tjoin' . 'tmap' 'tjoin'
-- @
--
--   In the latter:
--
-- @
-- 'tembed' f . 'tlift' = f
-- 'tembed' 'tlift' = 'id'
-- 'tembed' f . 'tembed' g = 'tembed' ('tembed' f . g)
-- @
--
class FunctorT t => MonadT t where
  -- | Lift a functor to a transformed functor.
  tlift :: f a -> t f a

  -- | The conventional monad join operator. It is used to remove
  --   one level of monadic structure, projecting its bound argument
  --   into the outer level.
  tjoin :: t (t f) a -> t f a
  tjoin
    = forall {k'} (t :: (k' -> *) -> k' -> *) (f :: k' -> *)
       (g :: k' -> *) (a :: k').
(MonadT t, MonadT t) =>
(forall (x :: k'). f x -> t g x) -> t f a -> t g a
tembed forall a. a -> a
id

  -- | Analogous to @('Control.Monad.=<<')@.
  tembed :: MonadT t => (forall x. f x -> t g x) -> t f a -> t g a
  tembed forall (x :: k'). f x -> t g x
h
    = forall {k'} (t :: (k' -> *) -> k' -> *) (f :: k' -> *) (a :: k').
MonadT t =>
t (t f) a -> t f a
tjoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap forall (x :: k'). f x -> t g x
h

  {-# MINIMAL tlift, tjoin | tlift, tembed #-}


-- --------------------------------
-- Instances for base types
-- --------------------------------

instance Monad f => MonadT (Compose f) where
  tlift :: forall (f :: k' -> *) (a :: k'). f a -> Compose f f a
tlift = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE tlift #-}

  tjoin :: forall (f :: k' -> *) (a :: k').
Compose f (Compose f f) a -> Compose f f a
tjoin (Compose f (Compose f f a)
ffga)
    = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Compose f f a)
ffga)
  {-# INLINE tjoin #-}


instance Alternative f => MonadT (Product f) where
  tlift :: forall (f :: * -> *) a. f a -> Product f f a
tlift = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall (f :: * -> *) a. Alternative f => f a
empty
  {-# INLINE tlift #-}

  tjoin :: forall (f :: * -> *) a. Product f (Product f f) a -> Product f f a
tjoin (Pair f a
fa (Pair f a
fa' f a
ga))
    = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (f a
fa forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> f a
fa') f a
ga
  {-# INLINE tjoin #-}


instance MonadT (Sum f) where
  tlift :: forall (f :: k' -> *) (a :: k'). f a -> Sum f f a
tlift = forall k' (f :: k' -> *) (f :: k' -> *) (a :: k'). f a -> Sum f f a
InR
  {-# INLINE tlift #-}

  tjoin :: forall (f :: k' -> *) (a :: k'). Sum f (Sum f f) a -> Sum f f a
tjoin = \case
    InL f a
fa -> forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL f a
fa
    InR (InL f a
fa) -> forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL f a
fa
    InR (InR f a
ga) -> forall k' (f :: k' -> *) (f :: k' -> *) (a :: k'). f a -> Sum f f a
InR f a
ga


-- --------------------------------
-- Instances for transformers types
-- --------------------------------

instance MonadT Backwards where
  tlift :: forall (f :: k' -> *) (a :: k'). f a -> Backwards f a
tlift = forall k' (f :: k' -> *) (a :: k'). f a -> Backwards f a
Backwards
  {-# INLINE tlift #-}

  tjoin :: forall (f :: k' -> *) (a :: k').
Backwards (Backwards f) a -> Backwards f a
tjoin = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE tjoin #-}


instance MonadT Lift where
  tlift :: forall (f :: * -> *) a. f a -> Lift f a
tlift = forall (f :: * -> *) a. f a -> Lift f a
Lift.Other
  {-# INLINE tlift #-}

  tjoin :: forall (f :: * -> *) a. Lift (Lift f) a -> Lift f a
tjoin = \case
    Lift.Pure a
a
      -> forall (f :: * -> *) a. a -> Lift f a
Lift.Pure a
a

    Lift.Other (Lift.Pure a
a)
      -> forall (f :: * -> *) a. a -> Lift f a
Lift.Pure a
a

    Lift.Other (Lift.Other f a
fa)
      -> forall (f :: * -> *) a. f a -> Lift f a
Lift.Other f a
fa
  {-# INLINE tjoin #-}


instance MonadT IdentityT where
  tlift :: forall (f :: k' -> *) (a :: k'). f a -> IdentityT f a
tlift = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE tlift #-}

  tjoin :: forall (f :: k' -> *) (a :: k').
IdentityT (IdentityT f) a -> IdentityT f a
tjoin = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE tjoin #-}


instance MonadT (ReaderT r) where
  tlift :: forall (f :: * -> *) a. f a -> ReaderT r f a
tlift = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const
  {-# INLINE tlift #-}

  tjoin :: forall (f :: * -> *) a. ReaderT r (ReaderT r f) a -> ReaderT r f a
tjoin ReaderT r (ReaderT r f) a
rra
    = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \r
e -> coerce :: forall a b. Coercible a b => a -> b
coerce ReaderT r (ReaderT r f) a
rra r
e r
e
  {-# INLINE tjoin #-}


instance MonadT Reverse where
  tlift :: forall (f :: k' -> *) (a :: k'). f a -> Reverse f a
tlift = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE tlift #-}

  tjoin :: forall (f :: k' -> *) (a :: k').
Reverse (Reverse f) a -> Reverse f a
tjoin = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE tjoin #-}