{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE KindSignatures #-}

-- |
--    This module provides 'DepT', a monad transformer similar to 'ReaderT'.
--
--    The difference is that the environment of 'DepT' must be parameterized by
--    @DepT@'s own monad stack.
--
--    There's a function 'withDepT' which is analogous to 'withReaderT'.
--    There's no analogue of 'mapReaderT' however. 
module Control.Monad.Dep
  ( 
    -- * The DepT transformer
    DepT (DepT),
    runDepT,
    toReaderT,
    withDepT,
    zoomEnv,
    -- * The simplest environment
    NilEnv(NilEnv),
    -- * The next simplest environment
    -- $constant
    Constant(..),
    -- * Re-exports
    module Control.Monad.Trans,
    module Control.Monad.Dep.Class,
    module Control.Monad.Reader.Class
  )
where

import Control.Applicative
import Control.Monad.Trans
import Control.Monad.Cont.Class
import Control.Monad.Error.Class
import Control.Monad.IO.Unlift
import Control.Monad.Reader
import Control.Monad.Reader.Class
import Control.Monad.State.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.Identity
import Control.Monad.Writer.Class
import Control.Monad.Zip
import Control.Monad.Dep.Class
import Data.Kind (Type)
import Data.Coerce
import Data.Functor.Constant

-- $setup
--
-- >>> :set -XTypeApplications
-- >>> :set -XImportQualifiedPost
-- >>> :set -XTemplateHaskell
-- >>> :set -XStandaloneKindSignatures
-- >>> :set -XNamedFieldPuns
-- >>> import Control.Monad.Dep
-- >>> import Rank2 qualified
-- >>> import Rank2.TH qualified
--


-- |
--    A monad transformer which adds a read-only environment to the given monad.
--    The environment type must be parameterized with the transformer's stack.
--
--    The 'return' function ignores the environment, while @>>=@ passes the
--    inherited environment to both subcomputations.
type DepT ::
  ((Type -> Type) -> Type) ->
  (Type -> Type) ->
  Type ->
  Type
newtype DepT (e_ :: (Type -> Type) -> Type) (m :: Type -> Type) (r :: Type) = DepT {forall (e_ :: (* -> *) -> *) (m :: * -> *) r.
DepT e_ m r -> ReaderT (e_ (DepT e_ m)) m r
toReaderT :: ReaderT (e_ (DepT e_ m)) m r}
  deriving
    ( forall a b. a -> DepT e_ m b -> DepT e_ m a
forall a b. (a -> b) -> DepT e_ m a -> DepT e_ m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
a -> DepT e_ m b -> DepT e_ m a
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
(a -> b) -> DepT e_ m a -> DepT e_ m b
<$ :: forall a b. a -> DepT e_ m b -> DepT e_ m a
$c<$ :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
a -> DepT e_ m b -> DepT e_ m a
fmap :: forall a b. (a -> b) -> DepT e_ m a -> DepT e_ m b
$cfmap :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
(a -> b) -> DepT e_ m a -> DepT e_ m b
Functor,
      forall a. a -> DepT e_ m a
forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m a
forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m b
forall a b. DepT e_ m (a -> b) -> DepT e_ m a -> DepT e_ m b
forall a b c.
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
Applicative m =>
Functor (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Applicative m =>
a -> DepT e_ m a
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m a
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m b
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT e_ m (a -> b) -> DepT e_ m a -> DepT e_ m b
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
<* :: forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m a
$c<* :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m a
*> :: forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m b
$c*> :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m b
liftA2 :: forall a b c.
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
$cliftA2 :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
<*> :: forall a b. DepT e_ m (a -> b) -> DepT e_ m a -> DepT e_ m b
$c<*> :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT e_ m (a -> b) -> DepT e_ m a -> DepT e_ m b
pure :: forall a. a -> DepT e_ m a
$cpure :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Applicative m =>
a -> DepT e_ m a
Applicative,
      forall a. DepT e_ m a
forall a. DepT e_ m a -> DepT e_ m [a]
forall a. DepT e_ m a -> DepT e_ m a -> DepT e_ m a
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
Alternative m =>
Applicative (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a -> DepT e_ m [a]
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a -> DepT e_ m a -> DepT e_ m a
many :: forall a. DepT e_ m a -> DepT e_ m [a]
$cmany :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a -> DepT e_ m [a]
some :: forall a. DepT e_ m a -> DepT e_ m [a]
$csome :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a -> DepT e_ m [a]
<|> :: forall a. DepT e_ m a -> DepT e_ m a -> DepT e_ m a
$c<|> :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a -> DepT e_ m a -> DepT e_ m a
empty :: forall a. DepT e_ m a
$cempty :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT e_ m a
Alternative,
      forall a. a -> DepT e_ m a
forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m b
forall a b. DepT e_ m a -> (a -> DepT e_ m b) -> DepT e_ m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
Monad m =>
Applicative (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Monad m =>
a -> DepT e_ m a
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m b
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT e_ m a -> (a -> DepT e_ m b) -> DepT e_ m b
return :: forall a. a -> DepT e_ m a
$creturn :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
Monad m =>
a -> DepT e_ m a
>> :: forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m b
$c>> :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m b
>>= :: forall a b. DepT e_ m a -> (a -> DepT e_ m b) -> DepT e_ m b
$c>>= :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT e_ m a -> (a -> DepT e_ m b) -> DepT e_ m b
Monad,
      forall a. (a -> DepT e_ m a) -> DepT e_ m a
forall (m :: * -> *).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadFix m =>
Monad (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadFix m =>
(a -> DepT e_ m a) -> DepT e_ m a
mfix :: forall a. (a -> DepT e_ m a) -> DepT e_ m a
$cmfix :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadFix m =>
(a -> DepT e_ m a) -> DepT e_ m a
MonadFix,
      forall a. String -> DepT e_ m a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadFail m =>
Monad (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadFail m =>
String -> DepT e_ m a
fail :: forall a. String -> DepT e_ m a
$cfail :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadFail m =>
String -> DepT e_ m a
MonadFail,
      forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m (a, b)
forall a b. DepT e_ m (a, b) -> (DepT e_ m a, DepT e_ m b)
forall a b c.
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
forall (m :: * -> *).
Monad m
-> (forall a b. m a -> m b -> m (a, b))
-> (forall a b c. (a -> b -> c) -> m a -> m b -> m c)
-> (forall a b. m (a, b) -> (m a, m b))
-> MonadZip m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadZip m =>
Monad (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m (a, b)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT e_ m (a, b) -> (DepT e_ m a, DepT e_ m b)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
munzip :: forall a b. DepT e_ m (a, b) -> (DepT e_ m a, DepT e_ m b)
$cmunzip :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT e_ m (a, b) -> (DepT e_ m a, DepT e_ m b)
mzipWith :: forall a b c.
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
$cmzipWith :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> DepT e_ m a -> DepT e_ m b -> DepT e_ m c
mzip :: forall a b. DepT e_ m a -> DepT e_ m b -> DepT e_ m (a, b)
$cmzip :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT e_ m a -> DepT e_ m b -> DepT e_ m (a, b)
MonadZip,
      forall a. DepT e_ m a
forall a. DepT e_ m a -> DepT e_ m a -> DepT e_ m a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadPlus m =>
Monad (DepT e_ m)
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadPlus m =>
Alternative (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT e_ m a
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT e_ m a -> DepT e_ m a -> DepT e_ m a
mplus :: forall a. DepT e_ m a -> DepT e_ m a -> DepT e_ m a
$cmplus :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT e_ m a -> DepT e_ m a -> DepT e_ m a
mzero :: forall a. DepT e_ m a
$cmzero :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT e_ m a
MonadPlus,
      forall a b. ((a -> DepT e_ m b) -> DepT e_ m a) -> DepT e_ m a
forall (m :: * -> *).
Monad m -> (forall a b. ((a -> m b) -> m a) -> m a) -> MonadCont m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadCont m =>
Monad (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
MonadCont m =>
((a -> DepT e_ m b) -> DepT e_ m a) -> DepT e_ m a
callCC :: forall a b. ((a -> DepT e_ m b) -> DepT e_ m a) -> DepT e_ m a
$ccallCC :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a b.
MonadCont m =>
((a -> DepT e_ m b) -> DepT e_ m a) -> DepT e_ m a
MonadCont,
      forall a. IO a -> DepT e_ m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadIO m =>
Monad (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadIO m =>
IO a -> DepT e_ m a
liftIO :: forall a. IO a -> DepT e_ m a
$cliftIO :: forall (e_ :: (* -> *) -> *) (m :: * -> *) a.
MonadIO m =>
IO a -> DepT e_ m a
MonadIO,
      forall b. ((forall a. DepT e_ m a -> IO a) -> IO b) -> DepT e_ m b
forall (m :: * -> *).
MonadIO m
-> (forall b. ((forall a. m a -> IO a) -> IO b) -> m b)
-> MonadUnliftIO m
forall {e_ :: (* -> *) -> *} {m :: * -> *}.
MonadUnliftIO m =>
MonadIO (DepT e_ m)
forall (e_ :: (* -> *) -> *) (m :: * -> *) b.
MonadUnliftIO m =>
((forall a. DepT e_ m a -> IO a) -> IO b) -> DepT e_ m b
withRunInIO :: forall b. ((forall a. DepT e_ m a -> IO a) -> IO b) -> DepT e_ m b
$cwithRunInIO :: forall (e_ :: (* -> *) -> *) (m :: * -> *) b.
MonadUnliftIO m =>
((forall a. DepT e_ m a -> IO a) -> IO b) -> DepT e_ m b
MonadUnliftIO,
      MonadReader (e_ (DepT e_ m))
    )

instance MonadTrans (DepT e_) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> DepT e_ m a
lift = forall (e_ :: (* -> *) -> *) (m :: * -> *) r.
ReaderT (e_ (DepT e_ m)) m r -> DepT e_ m r
DepT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

deriving instance MonadState s m => MonadState s (DepT e_ m)

deriving instance MonadWriter w m => MonadWriter w (DepT e_ m)

deriving instance MonadError e m => MonadError e (DepT e_ m)

-- | 'DepT' can be d-lifted to a 'ReaderT' in which the environment record
-- containing further 'DepT' actions has been hidden behind a newtype. 
--
-- This can be useful to "deceive" a function into using an environment
-- possessing different instances than the instances seen by the function's
-- dependencies.
instance (Monad m, Coercible newtyped (e_ (DepT e_ m))) => LiftDep (DepT e_ m) (ReaderT newtyped m) where
  liftD :: forall x. DepT e_ m x -> ReaderT newtyped m x
liftD = coerce :: forall a b. Coercible a b => a -> b
coerce


-- | 'DepT' can be d-lifted to itself.
instance Monad m => LiftDep (DepT e_ m) (DepT e_ m) where
  liftD :: forall x. DepT e_ m x -> DepT e_ m x
liftD = forall a. a -> a
id

-- |
--    Runs a 'DepT' action in an environment.
--      
-- >>> runDepT (pure "foo") NilEnv
-- "foo"
--
--    For more sophisticated invocation functions, see @runFinalDepT@ and @runFromEnv@ from <http://hackage.haskell.org/package/dep-t-advice dep-t-advice>.
runDepT :: DepT e_ m r -> e_ (DepT e_ m) -> m r
runDepT :: forall (e_ :: (* -> *) -> *) (m :: * -> *) r.
DepT e_ m r -> e_ (DepT e_ m) -> m r
runDepT = forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e_ :: (* -> *) -> *) (m :: * -> *) r.
DepT e_ m r -> ReaderT (e_ (DepT e_ m)) m r
toReaderT

-- |
--    Changes the environment of a 'DepT', for example making the 'DepT' work in
--    a "bigger" environment than the one in which was defined initially.
--
--    The scary first parameter is a function that, given a natural
--    transformation of monads, changes the monad parameter of the environment
--    record. This function can be defined manually for each environment record,
--    or it can be generated using TH from the <http://hackage.haskell.org/package/rank2classes-1.4.1/docs/Rank2-TH.html#v:deriveFunctor rank2classes> package.
withDepT ::
  forall small big m a.
  Monad m =>
  -- | rank-2 map function
  ( forall p q.
    (forall x. p x -> q x) ->
    small p ->
    small q
  ) ->
  -- | get a small environment from a big one
  (forall t. big t -> small t) ->
  DepT small m a ->
  DepT big m a
withDepT :: forall (small :: (* -> *) -> *) (big :: (* -> *) -> *)
       (m :: * -> *) a.
Monad m =>
(forall (p :: * -> *) (q :: * -> *).
 (forall x. p x -> q x) -> small p -> small q)
-> (forall (t :: * -> *). big t -> small t)
-> DepT small m a
-> DepT big m a
withDepT forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv forall (t :: * -> *). big t -> small t
inner (DepT (ReaderT small (DepT small m) -> m a
f)) =
  forall (e_ :: (* -> *) -> *) (m :: * -> *) r.
ReaderT (e_ (DepT e_ m)) m r -> DepT e_ m r
DepT
    ( forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT
        ( \big (DepT big m)
big ->
            let small :: small (DepT small m)
                -- we have a big environment at hand, so let's extract the
                -- small environment, transform every function in the small
                -- environment by supplying the big environment and, as a
                -- finishing touch, lift from the base monad m so that it
                -- matches the monad expected by f.
                small :: small (DepT small m)
small = forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (e_ :: (* -> *) -> *) (m :: * -> *) r.
DepT e_ m r -> e_ (DepT e_ m) -> m r
runDepT big (DepT big m)
big) (forall (t :: * -> *). big t -> small t
inner big (DepT big m)
big)
             in small (DepT small m) -> m a
f small (DepT small m)
small
        )
    )

-- |
--    Makes the functions inside a small environment require a bigger environment.
--
--    The scary first parameter is a function that, given a natural
--    transformation of monads, changes the monad parameter of the environment
--    record. This function can be defined manually for each environment record,
--    or it can be generated using TH from the <http://hackage.haskell.org/package/rank2classes-1.4.1/docs/Rank2-TH.html#v:deriveFunctor rank2classes> package.
--
--    'zoomEnv' can be useful if we are encasing some preexisting small environment as a field of
--    a big environment, in order to make the types match:
--
-- >>> :{ 
--   type Env :: (Type -> Type) -> Type
--   data Env m = Env
--     { _logger :: String -> m (),
--       _repository :: Int -> m (),
--       _controller :: Int -> m String
--     }
--   $(Rank2.TH.deriveFunctor ''Env)
--   env :: Env (DepT Env IO)
--   env = Env 
--     { _logger = \_ -> pure (), 
--       _repository = \_ -> pure (), 
--       _controller = \_ -> pure "foo" 
--     }
--   type BiggerEnv :: (Type -> Type) -> Type
--   data BiggerEnv m = BiggerEnv
--     { _inner :: Env m,
--       _extra :: Int -> m Int
--     }
--   biggerEnv :: BiggerEnv (DepT BiggerEnv IO)
--   biggerEnv = BiggerEnv 
--     { _inner = zoomEnv (Rank2.<$>) _inner env, 
--       _extra = pure
--     }
-- :}
--
-- __However__, this is only needed when the monad of the smaller environment
-- is already \"fixed\" before inserting it in the bigger one—which I expect
-- to be an infrequent case. When the concrete monad is selected after nesting
-- the environments, 'zoomEnv' shouldn't be necessary.
--
{-# NOINLINE zoomEnv #-}
-- For the reason for not inlining, see https://twitter.com/DiazCarrete/status/1350116413445439493
zoomEnv ::
  forall small big m a.
  Monad m =>
  -- | rank-2 map function
  ( forall p q.
    (forall x. p x -> q x) ->
    small p ->
    small q
  ) ->
  -- | get a small environment from a big one
  (forall t. big t -> small t) ->
  small (DepT small m) ->
  small (DepT big m)
zoomEnv :: forall (small :: (* -> *) -> *) (big :: (* -> *) -> *)
       (m :: * -> *) a.
Monad m =>
(forall (p :: * -> *) (q :: * -> *).
 (forall x. p x -> q x) -> small p -> small q)
-> (forall (t :: * -> *). big t -> small t)
-> small (DepT small m)
-> small (DepT big m)
zoomEnv forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv forall (t :: * -> *). big t -> small t
inner = forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv (forall (small :: (* -> *) -> *) (big :: (* -> *) -> *)
       (m :: * -> *) a.
Monad m =>
(forall (p :: * -> *) (q :: * -> *).
 (forall x. p x -> q x) -> small p -> small q)
-> (forall (t :: * -> *). big t -> small t)
-> DepT small m a
-> DepT big m a
withDepT forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv forall (t :: * -> *). big t -> small t
inner)

-- | An empty environment that carries no functions, analogous to `()` for `ReaderT`.
type NilEnv :: (Type -> Type) -> Type
data NilEnv m = NilEnv


-- $constant
--
-- 'Constant', which has a phantom type parameter, is a valid environment for
-- 'DepT'.
-- 
-- @DepT (Constant e) m@ makes 'DepT' behave similarly to @ReaderT e m@,
-- in that the environment @e@ is independent of the monad. 
--