{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Polysemy.Several
( HList (..),
TypeMap,
Append,
runSeveral,
)
where
import Data.Kind
import Polysemy
infixr 5 :::
data HList a where
HNil :: HList '[]
(:::) :: a -> HList (b :: [Type]) -> HList (a ': b)
type family TypeMap (f :: a -> b) (xs :: [a]) where
TypeMap _ '[] = '[]
TypeMap f (x ': xs) = f x ': TypeMap f xs
type family Append (a :: [t]) (b :: [t]) where
Append '[] b = b
Append (a ': as) b = a ': Append as b
runSeveral ::
(forall r' k x. k -> Sem (e k ': r') x -> Sem r' x) ->
HList t ->
Sem (Append (TypeMap e t) r) a ->
Sem r a
runSeveral :: (forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x)
-> HList t -> Sem (Append (TypeMap e t) r) a -> Sem r a
runSeveral forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x
f (a
a ::: HList b
as) = (forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x)
-> HList b -> Sem (Append (TypeMap e b) r) a -> Sem r a
forall (e :: * -> Effect) (t :: [*]) (r :: [Effect]) a.
(forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x)
-> HList t -> Sem (Append (TypeMap e t) r) a -> Sem r a
runSeveral forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x
f HList b
as (Sem (Append (TypeMap e b) r) a -> Sem r a)
-> (Sem (e a : Append (TypeMap e b) r) a
-> Sem (Append (TypeMap e b) r) a)
-> Sem (e a : Append (TypeMap e b) r) a
-> Sem r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a
-> Sem (e a : Append (TypeMap e b) r) a
-> Sem (Append (TypeMap e b) r) a
forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x
f a
a
runSeveral forall (r' :: [Effect]) k x. k -> Sem (e k : r') x -> Sem r' x
_ HList t
HNil = Sem (Append (TypeMap e t) r) a -> Sem r a
forall a. a -> a
id