module Control.Monad.Ology.General.Trans.Tunnel where
import Control.Monad.Ology.General.Function
import Control.Monad.Ology.General.IO
import Control.Monad.Ology.General.Inner
import Control.Monad.Ology.General.Trans.Constraint
import Control.Monad.Ology.General.Trans.Hoist
import Control.Monad.Ology.Specific.ComposeInner
import Import
type MonadTransTunnel :: TransKind -> Constraint
class (MonadTransHoist t, MonadInner (Tunnel t)) => MonadTransTunnel t where
type Tunnel t :: Type -> Type
tunnel ::
forall m r. Monad m
=> ((forall m1 a. Monad m1 => t m1 a -> m1 (Tunnel t a)) -> m (Tunnel t r))
-> t m r
tunnelHoist ::
forall t m1 m2. (MonadTransTunnel t, Monad m1, Monad m2)
=> (m1 --> m2)
-> t m1 --> t m2
tunnelHoist :: forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransTunnel t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
tunnelHoist m1 --> m2
mma t m1 a
sm1 = forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun -> m1 --> m2
mma forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
tun t m1 a
sm1
backHoist :: (MonadTransTunnel t, Monad ma, Monad mb) => (ma -/-> mb) -> t ma -/-> t mb
backHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
(ma -/-> mb) -> t ma -/-> t mb
backHoist ma -/-> mb
wt (t mb --> t ma) -> t ma r
tm = forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> ma -/-> mb
wt forall a b. (a -> b) -> a -> b
$ \mb --> ma
tba -> forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift forall a b. (a -> b) -> a -> b
$ (t mb --> t ma) -> t ma r
tm forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (m1 :: Type -> Type) (m2 :: Type -> Type).
(MonadTransHoist t, Monad m1, Monad m2) =>
(m1 --> m2) -> t m1 --> t m2
hoist mb --> ma
tba
wBackHoist :: (MonadTransTunnel t, Monad ma, Monad mb) => WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist :: forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
WBackraised ma mb -> WBackraised (t ma) (t mb)
wBackHoist (MkWBackraised ma -/-> mb
f) = forall k (p :: k -> Type) (q :: k -> Type).
(p -/-> q) -> WBackraised p q
MkWBackraised forall a b. (a -> b) -> a -> b
$ forall (t :: TransKind) (ma :: Type -> Type) (mb :: Type -> Type).
(MonadTransTunnel t, Monad ma, Monad mb) =>
(ma -/-> mb) -> t ma -/-> t mb
backHoist ma -/-> mb
f
commuteTWith ::
forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
=> (forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
commutef ta (tb m) a
tabm =
case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
(m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @ta @m of
Dict (Monad (ta m))
Dict ->
case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
(m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @Monad @tb @m of
Dict (Monad (tb m))
Dict -> forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
tb m1 a -> m1 (Tunnel tb a)
unliftb -> forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
ta m1 a -> m1 (Tunnel ta a)
unlifta -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r)
commutef forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
tb m1 a -> m1 (Tunnel tb a)
unliftb forall a b. (a -> b) -> a -> b
$ forall (m1 :: Type -> Type) a.
Monad m1 =>
ta m1 a -> m1 (Tunnel ta a)
unlifta ta (tb m) a
tabm
commuteT ::
forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
=> ta (tb m) --> tb (ta m)
commuteT :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) --> tb (ta m)
commuteT = forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
(forall r. Tunnel tb (Tunnel ta r) -> Tunnel ta (Tunnel tb r))
-> ta (tb m) --> tb (ta m)
commuteTWith forall (m :: Type -> Type) (f :: Type -> Type) a.
(MonadInner m, Applicative f) =>
m (f a) -> f (m a)
commuteInner
commuteTBack ::
forall ta tb m. (MonadTransTunnel ta, MonadTransTunnel tb, Monad m)
=> ta (tb m) -/-> tb (ta m)
commuteTBack :: forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) -/-> tb (ta m)
commuteTBack (tb (ta m) --> ta (tb m)) -> ta (tb m) r
call = forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) --> tb (ta m)
commuteT forall a b. (a -> b) -> a -> b
$ (tb (ta m) --> ta (tb m)) -> ta (tb m) r
call forall (ta :: TransKind) (tb :: TransKind) (m :: Type -> Type).
(MonadTransTunnel ta, MonadTransTunnel tb, Monad m) =>
ta (tb m) --> tb (ta m)
commuteT
instance MonadInner inner => MonadTransTunnel (ComposeInner inner) where
type Tunnel (ComposeInner inner) = inner
tunnel :: forall (m :: Type -> Type) r.
Monad m =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r))
-> ComposeInner inner m r
tunnel (forall (m1 :: Type -> Type) a.
Monad m1 =>
ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r)
call = forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner forall a b. (a -> b) -> a -> b
$ (forall (m1 :: Type -> Type) a.
Monad m1 =>
ComposeInner inner m1 a -> m1 (Tunnel (ComposeInner inner) a))
-> m (Tunnel (ComposeInner inner) r)
call forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner
class (MonadHoistIO m, MonadInner (TunnelIO m)) => MonadTunnelIO m where
type TunnelIO m :: Type -> Type
tunnelIO :: forall r. ((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
instance MonadTunnelIO IO where
type TunnelIO IO = Identity
tunnelIO :: forall r.
((forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r))
-> IO r
tunnelIO (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
call = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ (forall a. IO a -> IO (TunnelIO IO a)) -> IO (TunnelIO IO r)
call forall a b. (a -> b) -> a -> b
$ \IO a
ma -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ IO a
ma
instance (MonadTransTunnel t, MonadTunnelIO m, MonadIO (t m)) => MonadTunnelIO (t m) where
type TunnelIO (t m) = ComposeInner (Tunnel t) (TunnelIO m)
tunnelIO :: forall r.
((forall a. t m a -> IO (TunnelIO (t m) a))
-> IO (TunnelIO (t m) r))
-> t m r
tunnelIO (forall a. t m a -> IO (TunnelIO (t m) a)) -> IO (TunnelIO (t m) r)
call =
forall (t :: TransKind) (m :: Type -> Type) r.
(MonadTransTunnel t, Monad m) =>
((forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a))
-> m (Tunnel t r))
-> t m r
tunnel forall a b. (a -> b) -> a -> b
$ \forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift -> forall (m :: Type -> Type) r.
MonadTunnelIO m =>
((forall a. m a -> IO (TunnelIO m a)) -> IO (TunnelIO m r)) -> m r
tunnelIO forall a b. (a -> b) -> a -> b
$ \forall a. m a -> IO (TunnelIO m a)
unliftIO -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (inner :: Type -> Type) (outer :: Type -> Type) a.
ComposeInner inner outer a -> outer (inner a)
unComposeInner forall a b. (a -> b) -> a -> b
$ (forall a. t m a -> IO (TunnelIO (t m) a)) -> IO (TunnelIO (t m) r)
call forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (inner :: Type -> Type) (outer :: Type -> Type) a.
outer (inner a) -> ComposeInner inner outer a
MkComposeInner forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a. m a -> IO (TunnelIO m a)
unliftIO forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (m1 :: Type -> Type) a.
Monad m1 =>
t m1 a -> m1 (Tunnel t a)
unlift
instance (MonadTransTunnel t, TransConstraint MonadIO t) => TransConstraint MonadTunnelIO t where
hasTransConstraint :: forall (m :: Type -> Type).
MonadTunnelIO m =>
Dict (MonadTunnelIO (t m))
hasTransConstraint = forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
(m :: Type -> Type) (c' :: (Type -> Type) -> Constraint).
(TransConstraint c t, c m) =>
(c (t m) => Dict (c' (t m))) -> Dict (c' (t m))
withTransConstraintDict @MonadIO forall (a :: Constraint). a => Dict a
Dict