module Control.Monad.Trans.Heftia.Church where
import Control.Effect.Class (type (~>))
import Control.Effect.Class.Machinery.HFunctor (hfmap)
import Control.Heftia.Trans (TransHeftia (..))
import Control.Monad (join)
import Control.Monad.Trans (MonadTrans, lift)
import Control.Monad.Trans.Cont (ContT (ContT), runContT)
import Control.Monad.Trans.Heftia (MonadTransHeftia, elaborateMK, reelaborateMK)
newtype HeftiaChurchT h f a = HeftiaChurchT
{forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
HeftiaChurchT h f a
-> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
unHeftiaChurchT :: forall r. (h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a}
deriving stock (forall a b. a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
forall a b. (a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
(a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
<$ :: forall a b. a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
$c<$ :: forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
a -> HeftiaChurchT h f b -> HeftiaChurchT h f a
fmap :: forall a b. (a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
$cfmap :: forall (h :: (* -> *) -> * -> *) k (f :: k -> *) a b.
(a -> b) -> HeftiaChurchT h f a -> HeftiaChurchT h f b
Functor)
runHeftiaChurchT :: (h (HeftiaChurchT h f) ~> ContT r f) -> HeftiaChurchT h f b -> ContT r f b
runHeftiaChurchT :: forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) (r :: k) b.
(h (HeftiaChurchT h f) ~> ContT r f)
-> HeftiaChurchT h f b -> ContT r f b
runHeftiaChurchT h (HeftiaChurchT h f) ~> ContT r f
i (HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f b
f) = forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f b
f h (HeftiaChurchT h f) ~> ContT r f
i
instance Applicative (HeftiaChurchT h f) where
pure :: forall a. a -> HeftiaChurchT h f a
pure a
x = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h f) ~> ContT r f
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
{-# INLINE pure #-}
HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f (a -> b)
f <*> :: forall a b.
HeftiaChurchT h f (a -> b)
-> HeftiaChurchT h f a -> HeftiaChurchT h f b
<*> HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
g = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h f) ~> ContT r f
i -> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f (a -> b)
f h (HeftiaChurchT h f) ~> ContT r f
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
g h (HeftiaChurchT h f) ~> ContT r f
i
{-# INLINE (<*>) #-}
instance Monad (HeftiaChurchT h f) where
HeftiaChurchT forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
f >>= :: forall a b.
HeftiaChurchT h f a
-> (a -> HeftiaChurchT h f b) -> HeftiaChurchT h f b
>>= a -> HeftiaChurchT h f b
k =
forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h f) ~> ContT r f
i -> forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a
f h (HeftiaChurchT h f) ~> ContT r f
i forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) (r :: k) b.
(h (HeftiaChurchT h f) ~> ContT r f)
-> HeftiaChurchT h f b -> ContT r f b
runHeftiaChurchT h (HeftiaChurchT h f) ~> ContT r f
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> HeftiaChurchT h f b
k
{-# INLINE (>>=) #-}
instance TransHeftia Monad HeftiaChurchT where
liftSigT :: forall (sig :: (* -> *) -> * -> *) (f :: * -> *) a.
HFunctor sig =>
sig (HeftiaChurchT sig f) a -> HeftiaChurchT sig f a
liftSigT sig (HeftiaChurchT sig f) a
e = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig (HeftiaChurchT sig f) ~> ContT r f
i -> sig (HeftiaChurchT sig f) ~> ContT r f
i sig (HeftiaChurchT sig f) a
e
{-# INLINE liftSigT #-}
translateT :: forall (f :: * -> *) (sig :: (* -> *) -> * -> *)
(sig' :: (* -> *) -> * -> *).
(Monad f, HFunctor sig, HFunctor sig') =>
(sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f))
-> HeftiaChurchT sig f ~> HeftiaChurchT sig' f
translateT sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f)
phi (HeftiaChurchT forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f) =
forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig' (HeftiaChurchT sig' f) ~> ContT r f
i ->
forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f forall a b. (a -> b) -> a -> b
$ sig' (HeftiaChurchT sig' f) ~> ContT r f
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f)
phi forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(sig :: (* -> *) -> * -> *) (sig' :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig, HFunctor sig') =>
(sig (h sig' f) ~> sig' (h sig' f)) -> h sig f ~> h sig' f
translateT sig (HeftiaChurchT sig' f) ~> sig' (HeftiaChurchT sig' f)
phi)
liftLowerHT :: forall (sig :: (* -> *) -> * -> *) (f :: * -> *).
(Monad f, HFunctor sig) =>
f ~> HeftiaChurchT sig f
liftLowerHT f x
a = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig (HeftiaChurchT sig f) ~> ContT r f
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift f x
a
{-# INLINE liftLowerHT #-}
hoistHeftia :: forall (f :: * -> *) (g :: * -> *) (sig :: (* -> *) -> * -> *).
(Monad f, Monad g, HFunctor sig) =>
(f ~> g) -> HeftiaChurchT sig f ~> HeftiaChurchT sig g
hoistHeftia f ~> g
phi (HeftiaChurchT forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f) =
forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \sig (HeftiaChurchT sig g) ~> ContT r g
i ->
forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> g r
k ->
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
phi forall a b. (a -> b) -> a -> b
$
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT
( forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f \sig (HeftiaChurchT sig f) x
e -> forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT \x -> f (g r)
k' ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT (sig (HeftiaChurchT sig g) ~> ContT r g
i forall a b. (a -> b) -> a -> b
$ forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> h sig f ~> h sig g
hoistHeftia f ~> g
phi) sig (HeftiaChurchT sig f) x
e) (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
phi forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> f (g r)
k')
)
(forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> g r
k)
runElaborateH :: forall (f :: * -> *) (sig :: (* -> *) -> * -> *).
(Monad f, HFunctor sig) =>
(sig f ~> f) -> HeftiaChurchT sig f ~> f
runElaborateH sig f ~> f
g (HeftiaChurchT forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f) =
forall {k} (r :: k) (m :: k -> *) a.
ContT r m a -> (a -> m r) -> m r
runContT (forall r. (sig (HeftiaChurchT sig f) ~> ContT r f) -> ContT r f x
f forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig f ~> f
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
(sig f ~> f) -> h sig f ~> f
runElaborateH sig f ~> f
g)) forall (f :: * -> *) a. Applicative f => a -> f a
pure
instance MonadTrans (HeftiaChurchT h) where
lift :: forall (m :: * -> *) a. Monad m => m a -> HeftiaChurchT h m a
lift m a
m = forall {k} (h :: (* -> *) -> * -> *) (f :: k -> *) a.
(forall (r :: k).
(h (HeftiaChurchT h f) ~> ContT r f) -> ContT r f a)
-> HeftiaChurchT h f a
HeftiaChurchT \h (HeftiaChurchT h m) ~> ContT r m
_ -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m
{-# INLINE lift #-}
instance MonadTransHeftia HeftiaChurchT where
elaborateMK :: forall (m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(Monad m, HFunctor sig) =>
(sig (ContT r m) ~> ContT r m) -> HeftiaChurchT sig m ~> ContT r m
elaborateMK sig (ContT r m) ~> ContT r m
f (HeftiaChurchT forall r. (sig (HeftiaChurchT sig m) ~> ContT r m) -> ContT r m x
g) = forall r. (sig (HeftiaChurchT sig m) ~> ContT r m) -> ContT r m x
g forall a b. (a -> b) -> a -> b
$ sig (ContT r m) ~> ContT r m
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (forall (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(MonadTransHeftia h, Monad m, HFunctor sig) =>
(sig (ContT r m) ~> ContT r m) -> h sig m ~> ContT r m
elaborateMK sig (ContT r m) ~> ContT r m
f)
{-# INLINE elaborateMK #-}
reelaborateMK :: forall (m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(Monad m, HFunctor sig) =>
(sig (ContT r (HeftiaChurchT sig m))
~> ContT r (HeftiaChurchT sig m))
-> HeftiaChurchT sig m ~> ContT r (HeftiaChurchT sig m)
reelaborateMK sig (ContT r (HeftiaChurchT sig m))
~> ContT r (HeftiaChurchT sig m)
f = forall (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(m :: * -> *) (sig :: (* -> *) -> * -> *) r.
(MonadTransHeftia h, Monad m, HFunctor sig) =>
(sig (ContT r m) ~> ContT r m) -> h sig m ~> ContT r m
elaborateMK sig (ContT r (HeftiaChurchT sig m))
~> ContT r (HeftiaChurchT sig m)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> h sig f ~> h sig g
hoistHeftia forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT
{-# INLINE reelaborateMK #-}