{-# LANGUAGE QuantifiedConstraints #-}
module Control.Freer.Trans where
import Control.Effect.Class (type (~>))
import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)
import Data.Free.Sum (pattern L1, pattern R1, type (+))
class (forall ins f. c f => c (fr ins f)) => TransFreer c fr | fr -> c where
{-# MINIMAL liftInsT, liftLowerFT, (hoistFreer, runInterpretF | interpretFT) #-}
liftInsT :: ins ~> fr ins f
liftLowerFT :: forall ins f. c f => f ~> fr ins f
transformT :: c f => (ins ~> ins') -> fr ins f ~> fr ins' f
transformT ins ~> ins'
f = 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 {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
. ins ~> ins'
f)
{-# INLINE transformT #-}
hoistFreer :: (c f, c g) => (f ~> g) -> fr ins f ~> fr ins g
hoistFreer f ~> g
f = 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 {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT forall b c a. (b -> c) -> (a -> b) -> a -> c
. f ~> g
f) forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT
{-# INLINE hoistFreer #-}
interposeLowerT :: (c f, c g) => (f ~> fr ins g) -> fr ins f ~> fr ins g
interposeLowerT f ~> fr ins g
f = 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 f ~> fr ins g
f forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT
{-# INLINE interposeLowerT #-}
runInterpretF :: c f => (ins ~> f) -> fr ins f a -> f a
default runInterpretF :: (c f, c (IdentityT f)) => (ins ~> f) -> fr ins f a -> f a
runInterpretF ins ~> 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 {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 {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
. ins ~> f
f)
{-# INLINE runInterpretF #-}
interpretFT :: (c f, c g) => (f ~> g) -> (ins ~> g) -> fr ins f ~> g
interpretFT f ~> g
f ins ~> g
i = forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(ins :: k -> *) (a :: k).
(TransFreer c fr, c f) =>
(ins ~> f) -> fr ins f a -> f a
runInterpretF ins ~> g
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *)
(ins :: k -> *).
(TransFreer c fr, c f, c g) =>
(f ~> g) -> fr ins f ~> fr ins g
hoistFreer f ~> g
f
{-# INLINE interpretFT #-}
reinterpretFT :: c f => (ins ~> fr ins f) -> fr ins f ~> fr ins f
reinterpretFT = 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 {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT
{-# INLINE reinterpretFT #-}
mergeFreer ::
forall fr m ins ins' c.
(TransFreer c fr, c m) =>
fr ins (fr ins' m) ~> fr (ins + ins') m
mergeFreer :: forall {k} (fr :: (k -> *) -> (k -> *) -> k -> *) (m :: k -> *)
(ins :: k -> *) (ins' :: k -> *) (c :: (k -> *) -> Constraint).
(TransFreer c fr, c m) =>
fr ins (fr ins' m) ~> fr (ins + ins') m
mergeFreer = 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 {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(ins :: k -> *) (ins' :: k -> *).
(TransFreer c fr, c f) =>
(ins ~> ins') -> fr ins f ~> fr ins' f
transformT @c forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) (forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT @c forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)
splitFreer ::
forall fr m ins ins' c.
(TransFreer c fr, c m) =>
fr (ins + ins') m ~> fr ins (fr ins' m)
splitFreer :: forall {k} (fr :: (k -> *) -> (k -> *) -> k -> *) (m :: k -> *)
(ins :: k -> *) (ins' :: k -> *) (c :: (k -> *) -> Constraint).
(TransFreer c fr, c m) =>
fr (ins + ins') m ~> fr ins (fr ins' m)
splitFreer = 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 {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT) \case
L1 ins x
e -> forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT ins x
e
R1 ins' x
e -> forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
(TransFreer c fr, c f) =>
f ~> fr ins f
liftLowerFT forall a b. (a -> b) -> a -> b
$ forall {k} (c :: (k -> *) -> Constraint)
(fr :: (k -> *) -> (k -> *) -> k -> *) (ins :: k -> *)
(f :: k -> *).
TransFreer c fr =>
ins ~> fr ins f
liftInsT ins' x
e