{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Control.Heftia.Trans where
import Control.Effect.Class (LiftIns (LiftIns), unliftIns, type (~>))
import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr))
import Control.Freer.Trans (TransFreer, interpretFT, liftInsT, liftLowerFT)
import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)
class (forall sig f. c f => c (h sig f)) => TransHeftia c h | h -> c where
{-# MINIMAL liftSigT, liftLowerHT, (hoistHeftia, runElaborateH | elaborateHT) #-}
liftSigT :: HFunctor sig => sig (h sig f) a -> h sig f a
transformHT ::
(c f, HFunctor sig, HFunctor sig') =>
(forall g. sig g ~> sig' g) ->
h sig f ~> h sig' f
transformHT forall (g :: * -> *). sig g ~> sig' g
f = 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 forall (g :: * -> *). sig g ~> sig' g
f
{-# INLINE transformHT #-}
translateT ::
(c f, HFunctor sig, HFunctor sig') =>
(sig (h sig' f) ~> sig' (h sig' f)) ->
h sig f ~> h sig' f
translateT sig (h sig' f) ~> sig' (h sig' f)
f = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig (h sig' f) ~> sig' (h sig' f)
f)
{-# INLINE translateT #-}
liftLowerHT :: forall sig f. (c f, HFunctor sig) => f ~> h sig f
hoistHeftia :: (c f, c g, HFunctor sig) => (f ~> g) -> h sig f ~> h sig g
hoistHeftia f ~> g
phi = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
phi) forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT
{-# INLINE hoistHeftia #-}
interpretLowerHT :: (HFunctor sig, c f, c g) => (f ~> h sig g) -> h sig f ~> h sig g
interpretLowerHT f ~> h sig g
f = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT f ~> h sig g
f forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT
{-# INLINE interpretLowerHT #-}
runElaborateH :: (c f, HFunctor sig) => (sig f ~> f) -> h sig f ~> f
default runElaborateH :: (c f, c (IdentityT f), HFunctor sig) => (sig f ~> f) -> h sig f ~> f
runElaborateH sig f ~> f
f = forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT 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) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall b c a. (b -> c) -> (a -> b) -> a -> c
. sig f ~> f
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 {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT)
{-# INLINE runElaborateH #-}
elaborateHT :: (c f, c g, HFunctor sig) => (f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT f ~> g
f sig g ~> g
i = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
(sig f ~> f) -> h sig f ~> f
runElaborateH sig g ~> g
i 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 f ~> g
f
{-# INLINE elaborateHT #-}
reelaborateHT :: (c f, HFunctor sig) => (sig (h sig f) ~> h sig f) -> h sig f ~> h sig f
reelaborateHT = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT
{-# INLINE reelaborateHT #-}
heftiaToFreer ::
(TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) =>
h (LiftIns ins) f ~> fr ins f
heftiaToFreer :: forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(c' :: (* -> *) -> Constraint)
(fr :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(ins :: * -> *).
(TransHeftia c h, TransFreer c' fr, c f, c (fr ins f), c' f) =>
h (LiftIns ins) f ~> fr ins f
heftiaToFreer = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT (forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns)
{-# INLINE heftiaToFreer #-}
freerToHeftia ::
(TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f), c' (h (LiftIns ins) f), c f) =>
fr ins f ~> h (LiftIns ins) f
freerToHeftia :: forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(c' :: (* -> *) -> Constraint)
(fr :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(ins :: * -> *).
(TransHeftia c h, TransFreer c' fr, c' f, c' (fr ins f),
c' (h (LiftIns ins) f), c f) =>
fr ins f ~> h (LiftIns ins) f
freerToHeftia = forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
(ins :: k -> *).
(TransFreer c fr, c f, c g) =>
(f ~> g) -> (ins ~> g) -> fr ins f ~> g
interpretFT forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *).
(TransHeftia c h, c f, HFunctor sig) =>
f ~> h sig f
liftLowerHT (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns)
{-# INLINE freerToHeftia #-}
mergeHeftia ::
forall h m sig sig' a c.
(HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>
h sig (h sig' m) a ->
h (sig :+: sig') m a
mergeHeftia :: forall (h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(m :: * -> *) (sig :: (* -> *) -> * -> *)
(sig' :: (* -> *) -> * -> *) a (c :: (* -> *) -> Constraint).
(HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>
h sig (h sig' m) a -> h (sig :+: sig') m a
mergeHeftia = forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (sig :: (* -> *) -> * -> *).
(TransHeftia c h, c f, c g, HFunctor sig) =>
(f ~> g) -> (sig g ~> g) -> h sig f ~> g
elaborateHT (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 @c forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
(h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr) (forall (c :: (* -> *) -> Constraint)
(h :: ((* -> *) -> * -> *) -> (* -> *) -> * -> *)
(sig :: (* -> *) -> * -> *) (f :: * -> *) a.
(TransHeftia c h, HFunctor sig) =>
sig (h sig f) a -> h sig f a
liftSigT @c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
(h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl)