    {-# 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 (x :: k'). t f x -> t f x) -> t (t f) a -> t f a
    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
    forall (f :: k' -> *) (g :: k' -> *) (a :: k').
    MonadT t =>
    (forall (x :: k'). f x -> t g x) -> t f a -> t g a
    tembed t f x -> t f x
    forall (x :: k'). t f x -> t f x
    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
        = t (t g) a -> t g a
    forall {k'} (t :: (k' -> *) -> k' -> *) (f :: k' -> *) (a :: k').
    MonadT t =>
    t (t f) a -> t f a
    forall (f :: k' -> *) (a :: k'). t (t f) a -> t f a
    tjoin (t (t g) a -> t g a) -> (t f a -> t (t g) a) -> t f a -> t g a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (x :: k'). f x -> t g x) -> t f a -> t (t g) a
    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
    forall (f :: k' -> *) (g :: k' -> *) (x :: k').
    (forall (a :: k'). f a -> g a) -> t f x -> t g x
    tmap f a -> t g a
    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 = f (f a) -> Compose f f a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f (f a) -> Compose f f a)
    -> (f a -> f (f a)) -> f a -> Compose f f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f a -> f (f a)
    forall a. a -> f a
    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)
        = f (f a) -> Compose f f a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f (f (f a)) -> f (f a)
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (f (f (f a)) -> f (f a)) -> f (f (f a)) -> f (f a)
    forall a b. (a -> b) -> a -> b
    $ Compose f f a -> f (f a)
    forall a b. Coercible a b => a -> b
    coerce (Compose f f a -> f (f a)) -> f (Compose f f a) -> f (f (f a))
    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 = f a -> f a -> Product f f a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f a
    forall a. f a
    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))
        = f a -> f a -> Product f f a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (f a
    fa f a -> f a -> f a
    forall a. f a -> f a -> f a
    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 = f a -> Sum f f a
    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 -> f a -> Sum f f a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL f a
    fa
        InR (InL f a
    fa) -> f a -> Sum f f a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL f a
    fa
        InR (InR f a
    ga) -> f a -> Sum f f a
    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 = f a -> Backwards f a
    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 = Backwards (Backwards f) a -> Backwards f a
    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 = f a -> Lift f a
    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
          -> a -> Lift f a
    forall (f :: * -> *) a. a -> Lift f a
    Lift.Pure a
    a

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

        Lift.Other (Lift.Other f a
    fa)
          -> f a -> Lift f a
    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 = f a -> IdentityT f a
    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 = IdentityT (IdentityT f) a -> IdentityT f a
    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 = (r -> f a) -> ReaderT r f a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((r -> f a) -> ReaderT r f a)
    -> (f a -> r -> f a) -> f a -> ReaderT r f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f a -> r -> f a
    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
        = (r -> f a) -> ReaderT r f a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((r -> f a) -> ReaderT r f a) -> (r -> f a) -> ReaderT r f a
    forall a b. (a -> b) -> a -> b
    $ \r
    e -> ReaderT r (ReaderT r f) a -> r -> r -> f a
    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 = f a -> Reverse f a
    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 = Reverse (Reverse f) a -> Reverse f a
    forall a b. Coercible a b => a -> b
    coerce
      {-# INLINE tjoin #-}