{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Monad.Dep
(
DepT (DepT),
runDepT,
toReaderT,
withDepT,
zoomEnv,
NilEnv(NilEnv),
module Control.Monad.Reader.Class
)
where
import Control.Applicative
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 Data.Kind (Type)
type DepT ::
((Type -> Type) -> Type) ->
(Type -> Type) ->
Type ->
Type
newtype DepT env m r = DepT {DepT env m r -> ReaderT (env (DepT env m)) m r
toReaderT :: ReaderT (env (DepT env m)) m r}
deriving
( a -> DepT env m b -> DepT env m a
(a -> b) -> DepT env m a -> DepT env m b
(forall a b. (a -> b) -> DepT env m a -> DepT env m b)
-> (forall a b. a -> DepT env m b -> DepT env m a)
-> Functor (DepT env m)
forall a b. a -> DepT env m b -> DepT env m a
forall a b. (a -> b) -> DepT env m a -> DepT env m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
a -> DepT env m b -> DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
(a -> b) -> DepT env m a -> DepT env m b
<$ :: a -> DepT env m b -> DepT env m a
$c<$ :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
a -> DepT env m b -> DepT env m a
fmap :: (a -> b) -> DepT env m a -> DepT env m b
$cfmap :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Functor m =>
(a -> b) -> DepT env m a -> DepT env m b
Functor,
Functor (DepT env m)
a -> DepT env m a
Functor (DepT env m)
-> (forall a. a -> DepT env m a)
-> (forall a b.
DepT env m (a -> b) -> DepT env m a -> DepT env m b)
-> (forall a b c.
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c)
-> (forall a b. DepT env m a -> DepT env m b -> DepT env m b)
-> (forall a b. DepT env m a -> DepT env m b -> DepT env m a)
-> Applicative (DepT env m)
DepT env m a -> DepT env m b -> DepT env m b
DepT env m a -> DepT env m b -> DepT env m a
DepT env m (a -> b) -> DepT env m a -> DepT env m b
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
forall a. a -> DepT env m a
forall a b. DepT env m a -> DepT env m b -> DepT env m a
forall a b. DepT env m a -> DepT env m b -> DepT env m b
forall a b. DepT env m (a -> b) -> DepT env m a -> DepT env m b
forall a b c.
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env 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 (env :: (* -> *) -> *) (m :: * -> *).
Applicative m =>
Functor (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
Applicative m =>
a -> DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT env m a -> DepT env m b -> DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT env m a -> DepT env m b -> DepT env m b
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT env m (a -> b) -> DepT env m a -> DepT env m b
forall (env :: (* -> *) -> *) (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
<* :: DepT env m a -> DepT env m b -> DepT env m a
$c<* :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT env m a -> DepT env m b -> DepT env m a
*> :: DepT env m a -> DepT env m b -> DepT env m b
$c*> :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT env m a -> DepT env m b -> DepT env m b
liftA2 :: (a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
$cliftA2 :: forall (env :: (* -> *) -> *) (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
<*> :: DepT env m (a -> b) -> DepT env m a -> DepT env m b
$c<*> :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Applicative m =>
DepT env m (a -> b) -> DepT env m a -> DepT env m b
pure :: a -> DepT env m a
$cpure :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
Applicative m =>
a -> DepT env m a
$cp1Applicative :: forall (env :: (* -> *) -> *) (m :: * -> *).
Applicative m =>
Functor (DepT env m)
Applicative,
Applicative (DepT env m)
DepT env m a
Applicative (DepT env m)
-> (forall a. DepT env m a)
-> (forall a. DepT env m a -> DepT env m a -> DepT env m a)
-> (forall a. DepT env m a -> DepT env m [a])
-> (forall a. DepT env m a -> DepT env m [a])
-> Alternative (DepT env m)
DepT env m a -> DepT env m a -> DepT env m a
DepT env m a -> DepT env m [a]
DepT env m a -> DepT env m [a]
forall a. DepT env m a
forall a. DepT env m a -> DepT env m [a]
forall a. DepT env m a -> DepT env m a -> DepT env 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 (env :: (* -> *) -> *) (m :: * -> *).
Alternative m =>
Applicative (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a -> DepT env m [a]
forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a -> DepT env m a -> DepT env m a
many :: DepT env m a -> DepT env m [a]
$cmany :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a -> DepT env m [a]
some :: DepT env m a -> DepT env m [a]
$csome :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a -> DepT env m [a]
<|> :: DepT env m a -> DepT env m a -> DepT env m a
$c<|> :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a -> DepT env m a -> DepT env m a
empty :: DepT env m a
$cempty :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
Alternative m =>
DepT env m a
$cp1Alternative :: forall (env :: (* -> *) -> *) (m :: * -> *).
Alternative m =>
Applicative (DepT env m)
Alternative,
Applicative (DepT env m)
a -> DepT env m a
Applicative (DepT env m)
-> (forall a b.
DepT env m a -> (a -> DepT env m b) -> DepT env m b)
-> (forall a b. DepT env m a -> DepT env m b -> DepT env m b)
-> (forall a. a -> DepT env m a)
-> Monad (DepT env m)
DepT env m a -> (a -> DepT env m b) -> DepT env m b
DepT env m a -> DepT env m b -> DepT env m b
forall a. a -> DepT env m a
forall a b. DepT env m a -> DepT env m b -> DepT env m b
forall a b. DepT env m a -> (a -> DepT env m b) -> DepT env 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 (env :: (* -> *) -> *) (m :: * -> *).
Monad m =>
Applicative (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
Monad m =>
a -> DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT env m a -> DepT env m b -> DepT env m b
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT env m a -> (a -> DepT env m b) -> DepT env m b
return :: a -> DepT env m a
$creturn :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
Monad m =>
a -> DepT env m a
>> :: DepT env m a -> DepT env m b -> DepT env m b
$c>> :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT env m a -> DepT env m b -> DepT env m b
>>= :: DepT env m a -> (a -> DepT env m b) -> DepT env m b
$c>>= :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
Monad m =>
DepT env m a -> (a -> DepT env m b) -> DepT env m b
$cp1Monad :: forall (env :: (* -> *) -> *) (m :: * -> *).
Monad m =>
Applicative (DepT env m)
Monad,
Monad (DepT env m)
Monad (DepT env m)
-> (forall a. (a -> DepT env m a) -> DepT env m a)
-> MonadFix (DepT env m)
(a -> DepT env m a) -> DepT env m a
forall a. (a -> DepT env m a) -> DepT env m a
forall (m :: * -> *).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadFix m =>
Monad (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadFix m =>
(a -> DepT env m a) -> DepT env m a
mfix :: (a -> DepT env m a) -> DepT env m a
$cmfix :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadFix m =>
(a -> DepT env m a) -> DepT env m a
$cp1MonadFix :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadFix m =>
Monad (DepT env m)
MonadFix,
Monad (DepT env m)
Monad (DepT env m)
-> (forall a. String -> DepT env m a) -> MonadFail (DepT env m)
String -> DepT env m a
forall a. String -> DepT env m a
forall (m :: * -> *).
Monad m -> (forall a. String -> m a) -> MonadFail m
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadFail m =>
Monad (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadFail m =>
String -> DepT env m a
fail :: String -> DepT env m a
$cfail :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadFail m =>
String -> DepT env m a
$cp1MonadFail :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadFail m =>
Monad (DepT env m)
MonadFail,
Monad (DepT env m)
Monad (DepT env m)
-> (forall a b. DepT env m a -> DepT env m b -> DepT env m (a, b))
-> (forall a b c.
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c)
-> (forall a b. DepT env m (a, b) -> (DepT env m a, DepT env m b))
-> MonadZip (DepT env m)
DepT env m a -> DepT env m b -> DepT env m (a, b)
DepT env m (a, b) -> (DepT env m a, DepT env m b)
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
forall a b. DepT env m a -> DepT env m b -> DepT env m (a, b)
forall a b. DepT env m (a, b) -> (DepT env m a, DepT env m b)
forall a b c.
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env 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 (env :: (* -> *) -> *) (m :: * -> *).
MonadZip m =>
Monad (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT env m a -> DepT env m b -> DepT env m (a, b)
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT env m (a, b) -> (DepT env m a, DepT env m b)
forall (env :: (* -> *) -> *) (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
munzip :: DepT env m (a, b) -> (DepT env m a, DepT env m b)
$cmunzip :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT env m (a, b) -> (DepT env m a, DepT env m b)
mzipWith :: (a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
$cmzipWith :: forall (env :: (* -> *) -> *) (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> DepT env m a -> DepT env m b -> DepT env m c
mzip :: DepT env m a -> DepT env m b -> DepT env m (a, b)
$cmzip :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
MonadZip m =>
DepT env m a -> DepT env m b -> DepT env m (a, b)
$cp1MonadZip :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadZip m =>
Monad (DepT env m)
MonadZip,
Monad (DepT env m)
Alternative (DepT env m)
DepT env m a
Alternative (DepT env m)
-> Monad (DepT env m)
-> (forall a. DepT env m a)
-> (forall a. DepT env m a -> DepT env m a -> DepT env m a)
-> MonadPlus (DepT env m)
DepT env m a -> DepT env m a -> DepT env m a
forall a. DepT env m a
forall a. DepT env m a -> DepT env m a -> DepT env m a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadPlus m =>
Monad (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadPlus m =>
Alternative (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT env m a -> DepT env m a -> DepT env m a
mplus :: DepT env m a -> DepT env m a -> DepT env m a
$cmplus :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT env m a -> DepT env m a -> DepT env m a
mzero :: DepT env m a
$cmzero :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadPlus m =>
DepT env m a
$cp2MonadPlus :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadPlus m =>
Monad (DepT env m)
$cp1MonadPlus :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadPlus m =>
Alternative (DepT env m)
MonadPlus,
Monad (DepT env m)
Monad (DepT env m)
-> (forall a b.
((a -> DepT env m b) -> DepT env m a) -> DepT env m a)
-> MonadCont (DepT env m)
((a -> DepT env m b) -> DepT env m a) -> DepT env m a
forall a b. ((a -> DepT env m b) -> DepT env m a) -> DepT env m a
forall (m :: * -> *).
Monad m -> (forall a b. ((a -> m b) -> m a) -> m a) -> MonadCont m
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadCont m =>
Monad (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a b.
MonadCont m =>
((a -> DepT env m b) -> DepT env m a) -> DepT env m a
callCC :: ((a -> DepT env m b) -> DepT env m a) -> DepT env m a
$ccallCC :: forall (env :: (* -> *) -> *) (m :: * -> *) a b.
MonadCont m =>
((a -> DepT env m b) -> DepT env m a) -> DepT env m a
$cp1MonadCont :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadCont m =>
Monad (DepT env m)
MonadCont,
Monad (DepT env m)
Monad (DepT env m)
-> (forall a. IO a -> DepT env m a) -> MonadIO (DepT env m)
IO a -> DepT env m a
forall a. IO a -> DepT env m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadIO m =>
Monad (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadIO m =>
IO a -> DepT env m a
liftIO :: IO a -> DepT env m a
$cliftIO :: forall (env :: (* -> *) -> *) (m :: * -> *) a.
MonadIO m =>
IO a -> DepT env m a
$cp1MonadIO :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadIO m =>
Monad (DepT env m)
MonadIO,
MonadIO (DepT env m)
MonadIO (DepT env m)
-> (forall b.
((forall a. DepT env m a -> IO a) -> IO b) -> DepT env m b)
-> MonadUnliftIO (DepT env m)
((forall a. DepT env m a -> IO a) -> IO b) -> DepT env m b
forall b.
((forall a. DepT env m a -> IO a) -> IO b) -> DepT env m b
forall (m :: * -> *).
MonadIO m
-> (forall b. ((forall a. m a -> IO a) -> IO b) -> m b)
-> MonadUnliftIO m
forall (env :: (* -> *) -> *) (m :: * -> *).
MonadUnliftIO m =>
MonadIO (DepT env m)
forall (env :: (* -> *) -> *) (m :: * -> *) b.
MonadUnliftIO m =>
((forall a. DepT env m a -> IO a) -> IO b) -> DepT env m b
withRunInIO :: ((forall a. DepT env m a -> IO a) -> IO b) -> DepT env m b
$cwithRunInIO :: forall (env :: (* -> *) -> *) (m :: * -> *) b.
MonadUnliftIO m =>
((forall a. DepT env m a -> IO a) -> IO b) -> DepT env m b
$cp1MonadUnliftIO :: forall (env :: (* -> *) -> *) (m :: * -> *).
MonadUnliftIO m =>
MonadIO (DepT env m)
MonadUnliftIO,
MonadReader (env (DepT env m))
)
instance MonadTrans (DepT env) where
lift :: m a -> DepT env m a
lift = ReaderT (env (DepT env m)) m a -> DepT env m a
forall (env :: (* -> *) -> *) (m :: * -> *) r.
ReaderT (env (DepT env m)) m r -> DepT env m r
DepT (ReaderT (env (DepT env m)) m a -> DepT env m a)
-> (m a -> ReaderT (env (DepT env m)) m a) -> m a -> DepT env m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> ReaderT (env (DepT env m)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
deriving instance MonadState s m => MonadState s (DepT env m)
deriving instance MonadWriter w m => MonadWriter w (DepT env m)
deriving instance MonadError e m => MonadError e (DepT env m)
runDepT :: DepT env m r -> env (DepT env m) -> m r
runDepT :: DepT env m r -> env (DepT env m) -> m r
runDepT = ReaderT (env (DepT env m)) m r -> env (DepT env m) -> m r
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT (env (DepT env m)) m r -> env (DepT env m) -> m r)
-> (DepT env m r -> ReaderT (env (DepT env m)) m r)
-> DepT env m r
-> env (DepT env m)
-> m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DepT env m r -> ReaderT (env (DepT env m)) m r
forall (env :: (* -> *) -> *) (m :: * -> *) r.
DepT env m r -> ReaderT (env (DepT env m)) m r
toReaderT
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)
-> (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)) =
ReaderT (big (DepT big m)) m a -> DepT big m a
forall (env :: (* -> *) -> *) (m :: * -> *) r.
ReaderT (env (DepT env m)) m r -> DepT env m r
DepT
( (big (DepT big m) -> m a) -> ReaderT (big (DepT big m)) m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT
( \big (DepT big m)
big ->
let small :: small (DepT small m)
small :: small (DepT small m)
small = (forall x. DepT big m x -> DepT small m x)
-> small (DepT big m) -> small (DepT small m)
forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv (m x -> DepT small m x
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m x -> DepT small m x)
-> (DepT big m x -> m x) -> DepT big m x -> DepT small m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DepT big m x -> big (DepT big m) -> m x)
-> big (DepT big m) -> DepT big m x -> m x
forall a b c. (a -> b -> c) -> b -> a -> c
flip DepT big m x -> big (DepT big m) -> m x
forall (env :: (* -> *) -> *) (m :: * -> *) r.
DepT env m r -> env (DepT env m) -> m r
runDepT big (DepT big m)
big) (big (DepT big m) -> small (DepT big m)
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
)
)
{-# NOINLINE zoomEnv #-}
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)
-> (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 x. DepT small m x -> DepT big m x)
-> small (DepT small m) -> small (DepT big m)
forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q
mapEnv ((forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> small p -> small q)
-> (forall (t :: * -> *). big t -> small t)
-> DepT small m x
-> DepT big m x
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)
type NilEnv :: (Type -> Type) -> Type
data NilEnv m = NilEnv