{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Polysemy.Extra
(
contramapInput,
contramapInputSem,
contramapInput',
runInputConstF,
mapOutput,
mapOutputSem,
mapOutput',
runOutputMapAsKVStore,
raise4Under,
reinterpretUnder,
reinterpretUnder2,
reinterpret2Under,
rotateEffects2,
rotateEffects3L,
rotateEffects3R,
rotateEffects4L,
rotateEffects4R,
reverseEffects2,
reverseEffects3,
reverseEffects4,
)
where
import Control.Arrow ((>>>))
import Data.Map as Map (Map, toList)
import Polysemy (Members, Sem, interpret, raise2Under,
raise3Under, raiseUnder)
import Polysemy.Input (Input (Input), input, runInputConst)
import Polysemy.Internal (hoistSem, subsumeUsing)
import Polysemy.Internal.Union (ElemOf (Here, There), Union (Union),
hoist)
import Polysemy.KVStore (KVStore, writeKV)
import Polysemy.Output (Output (Output), output)
runOutputMapAsKVStore ::
Members '[KVStore k v] r =>
Sem (Output (Map k v) ': r) a ->
Sem r a
runOutputMapAsKVStore :: forall k v (r :: EffectRow) a.
Members '[KVStore k v] r =>
Sem (Output (Map k v) : r) a -> Sem r a
runOutputMapAsKVStore = forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall (rInitial :: EffectRow) x. e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
Output Map k v
xs -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall k v (r :: EffectRow).
Member (KVStore k v) r =>
k -> v -> Sem r ()
writeKV) (forall k a. Map k a -> [(k, a)]
Map.toList Map k v
xs)
{-# INLINE runOutputMapAsKVStore #-}
mapOutput ::
Members '[Output o'] r =>
(o -> o') ->
Sem (Output o ': r) a ->
Sem r a
mapOutput :: forall o' (r :: EffectRow) o a.
Members '[Output o'] r =>
(o -> o') -> Sem (Output o : r) a -> Sem r a
mapOutput o -> o'
f = forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall (rInitial :: EffectRow) x. e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
Output o
o -> forall o (r :: EffectRow). Member (Output o) r => o -> Sem r ()
output (o -> o'
f o
o)
{-# INLINE mapOutput #-}
mapOutput' ::
Members '[Output o'] r =>
(o -> o') ->
Sem (Output o ': r) a ->
Sem (Output o' ': r) a
mapOutput' :: forall o' (r :: EffectRow) o a.
Members '[Output o'] r =>
(o -> o') -> Sem (Output o : r) a -> Sem (Output o' : r) a
mapOutput' o -> o'
f = forall (e2 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall o' (r :: EffectRow) o a.
Members '[Output o'] r =>
(o -> o') -> Sem (Output o : r) a -> Sem r a
mapOutput o -> o'
f
{-# INLINE mapOutput' #-}
mapOutputSem ::
forall o o' r a.
Members '[Output o'] r =>
(o -> Sem r o') ->
Sem (Output o ': r) a ->
Sem r a
mapOutputSem :: forall o o' (r :: EffectRow) a.
Members '[Output o'] r =>
(o -> Sem r o') -> Sem (Output o : r) a -> Sem r a
mapOutputSem o -> Sem r o'
f = forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall (rInitial :: EffectRow) x. e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
Output o
o -> o -> Sem r o'
f o
o forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall o (r :: EffectRow). Member (Output o) r => o -> Sem r ()
output
{-# INLINE mapOutputSem #-}
contramapInput ::
forall i i' r a.
Members '[Input i'] r =>
(i' -> i) ->
Sem (Input i ': r) a ->
Sem r a
contramapInput :: forall i i' (r :: EffectRow) a.
Members '[Input i'] r =>
(i' -> i) -> Sem (Input i : r) a -> Sem r a
contramapInput i' -> i
f = forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall (rInitial :: EffectRow) x. e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
Input i (Sem rInitial) x
Input -> i' -> i
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (r :: EffectRow). Member (Input i) r => Sem r i
input @i'
{-# INLINE contramapInput #-}
contramapInput' ::
forall i i' r a.
Members '[Input i'] r =>
(i' -> i) ->
Sem (Input i ': r) a ->
Sem (Input i' ': r) a
contramapInput' :: forall i i' (r :: EffectRow) a.
Members '[Input i'] r =>
(i' -> i) -> Sem (Input i : r) a -> Sem (Input i' : r) a
contramapInput' i' -> i
f = forall (e2 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : r) a -> Sem (e1 : e2 : r) a
raiseUnder forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall i i' (r :: EffectRow) a.
Members '[Input i'] r =>
(i' -> i) -> Sem (Input i : r) a -> Sem r a
contramapInput i' -> i
f
{-# INLINE contramapInput' #-}
contramapInputSem ::
forall i i' r a.
Members '[Input i'] r =>
(i' -> Sem r i) ->
Sem (Input i ': r) a ->
Sem r a
contramapInputSem :: forall i i' (r :: EffectRow) a.
Members '[Input i'] r =>
(i' -> Sem r i) -> Sem (Input i : r) a -> Sem r a
contramapInputSem i' -> Sem r i
f = forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall (rInitial :: EffectRow) x. e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
Input i (Sem rInitial) x
Input -> i' -> Sem r i
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (r :: EffectRow). Member (Input i) r => Sem r i
input @i'
{-# INLINE contramapInputSem #-}
runInputConstF ::
forall b f r a.
f b ->
Sem (Input (f b) ': r) a ->
Sem r a
runInputConstF :: forall {k} (b :: k) (f :: k -> *) (r :: EffectRow) a.
f b -> Sem (Input (f b) : r) a -> Sem r a
runInputConstF = forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst @(f b)
{-# INLINE runInputConstF #-}
reinterpretUnder ::
forall e1 e2 e3 r a.
(forall m x. Sem (e2 ': m) x -> Sem (e3 ': m) x) ->
Sem (e1 ': e2 ': r) a ->
Sem (e1 ': e3 ': r) a
reinterpretUnder :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
(forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : m) x)
-> Sem (e1 : e2 : r) a -> Sem (e1 : e3 : r) a
reinterpretUnder forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : m) x
f =
forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under @e1 @e1 @e2
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e1 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : m) x
f
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under @e3 @e3 @e1
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e3 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
{-# INLINE reinterpretUnder #-}
reinterpretUnder2 ::
forall e1 e2 e3 e4 r a.
(forall m x. Sem (e3 ': m) x -> Sem (e4 ': m) x) ->
Sem (e1 ': e2 ': e3 ': r) a ->
Sem (e1 ': e2 ': e4 ': r) a
reinterpretUnder2 :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
(forall (m :: EffectRow) x. Sem (e3 : m) x -> Sem (e4 : m) x)
-> Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e4 : r) a
reinterpretUnder2 forall (m :: EffectRow) x. Sem (e3 : m) x -> Sem (e4 : m) x
f =
forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e1 @e1 @e2 @e3
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e1 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e2 @e2 @e3 @e1
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e2 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (m :: EffectRow) x. Sem (e3 : m) x -> Sem (e4 : m) x
f
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e4 @e4 @e1 @e2
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e4 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
{-# INLINE reinterpretUnder2 #-}
reinterpret2Under ::
forall e1 e2 e3 e4 r a.
(forall m x. Sem (e2 ': m) x -> Sem (e3 ': e4 ': m) x) ->
Sem (e1 ': e2 ': r) a ->
Sem (e1 ': e3 ': e4 ': r) a
reinterpret2Under :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
(forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : e4 : m) x)
-> Sem (e1 : e2 : r) a -> Sem (e1 : e3 : e4 : r) a
reinterpret2Under forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : e4 : m) x
f =
forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under @e1 @e1 @e2
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e1 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : e4 : m) x
f
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e3 @e3 @e4 @e1
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e3 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e4 @e4 @e1 @e3
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e4 (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
{-# INLINE reinterpret2Under #-}
raise4Under :: forall e5 e1 e2 e3 e4 r a. Sem (e1 ': e2 ': e3 ': e4 ': r) a -> Sem (e1 ': e2 ': e3 ': e4 ': e5 ': r) a
raise4Under :: forall (e5 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(e4 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : e3 : e4 : e5 : r) a
raise4Under = forall (r :: EffectRow) (r' :: EffectRow) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (n :: * -> *) (r :: EffectRow) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist forall (e5 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(e4 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : e3 : e4 : e5 : r) a
raise4Under forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) x.
Union (e1 : e2 : e3 : e4 : r) m x
-> Union (e1 : e2 : e3 : e4 : e5 : r) m x
weaken4Under
where
weaken4Under :: forall m x. Union (e1 ': e2 ': e3 ': e4 ': r) m x -> Union (e1 ': e2 ': e3 ': e4 ': e5 ': r) m x
weaken4Under :: forall (m :: * -> *) x.
Union (e1 : e2 : e3 : e4 : r) m x
-> Union (e1 : e2 : e3 : e4 : e5 : r) m x
weaken4Under (Union ElemOf e (e1 : e2 : e3 : e4 : r)
Here Weaving e m x
a) = forall (e :: (* -> *) -> * -> *) (r :: EffectRow)
(mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here Weaving e m x
a
weaken4Under (Union (There ElemOf e r
Here) Weaving e m x
a) = forall (e :: (* -> *) -> * -> *) (r :: EffectRow)
(mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here) Weaving e m x
a
weaken4Under (Union (There (There ElemOf e r
Here)) Weaving e m x
a) = forall (e :: (* -> *) -> * -> *) (r :: EffectRow)
(mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)) Weaving e m x
a
weaken4Under (Union (There (There (There ElemOf e r
Here))) Weaving e m x
a) = forall (e :: (* -> *) -> * -> *) (r :: EffectRow)
(mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here))) Weaving e m x
a
weaken4Under (Union (There (There (There (There ElemOf e r
n)))) Weaving e m x
a) = forall (e :: (* -> *) -> * -> *) (r :: EffectRow)
(mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There ElemOf e r
n))))) Weaving e m x
a
{-# INLINE weaken4Under #-}
{-# INLINE raise4Under #-}
rotateEffects2 :: forall e1 e2 r a. Sem (e1 ': e2 ': r) a -> Sem (e2 ': e1 ': r) a
rotateEffects2 :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e2 : e1 : r) a
rotateEffects2 = forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
{-# INLINE rotateEffects2 #-}
rotateEffects3L :: forall e1 e2 e3 r a. Sem (e1 ': e2 ': e3 ': r) a -> Sem (e2 ': e3 ': e1 ': r) a
rotateEffects3L :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e2 : e3 : e1 : r) a
rotateEffects3L = forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
{-# INLINE rotateEffects3L #-}
rotateEffects3R :: forall e1 e2 e3 r a. Sem (e1 ': e2 ': e3 ': r) a -> Sem (e3 ': e1 ': e2 ': r) a
rotateEffects3R :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e3 : e1 : e2 : r) a
rotateEffects3R = forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e2 : e3 : e1 : r) a
rotateEffects3L forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e2 : e3 : e1 : r) a
rotateEffects3L
{-# INLINE rotateEffects3R #-}
rotateEffects4L :: forall e1 e2 e3 e4 r a. Sem (e1 ': e2 ': e3 ': e4 ': r) a -> Sem (e2 ': e3 ': e4 ': e1 ': r) a
rotateEffects4L :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e2 : e3 : e4 : e1 : r) a
rotateEffects4L = forall (e5 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
(e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
(e4 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : e3 : e4 : e5 : r) a
raise4Under forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing (forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall a b. (a -> b) -> a -> b
$ forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here)
{-# INLINE rotateEffects4L #-}
rotateEffects4R :: forall e1 e2 e3 e4 r a. Sem (e1 ': e2 ': e3 ': e4 ': r) a -> Sem (e4 ': e1 ': e2 ': e3 ': r) a
rotateEffects4R :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e4 : e1 : e2 : e3 : r) a
rotateEffects4R = forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e2 : e3 : e4 : e1 : r) a
rotateEffects4L forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e2 : e3 : e4 : e1 : r) a
rotateEffects4L forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e2 : e3 : e4 : e1 : r) a
rotateEffects4L
{-# INLINE rotateEffects4R #-}
reverseEffects2 :: forall e1 e2 r a. Sem (e1 ': e2 ': r) a -> Sem (e2 ': e1 ': r) a
reverseEffects2 :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e2 : e1 : r) a
reverseEffects2 = forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e2 : e1 : r) a
rotateEffects2
{-# INLINE reverseEffects2 #-}
reverseEffects3 :: forall e1 e2 e3 r a. Sem (e1 ': e2 ': e3 ': r) a -> Sem (e3 ': e2 ': e1 ': r) a
reverseEffects3 :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e3 : e2 : e1 : r) a
reverseEffects3 = forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e2 : e3 : e1 : r) a
rotateEffects3L forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e2 : e1 : r) a
rotateEffects2
{-# INLINE reverseEffects3 #-}
reverseEffects4 :: forall e1 e2 e3 e4 r a. Sem (e1 ': e2 ': e3 ': e4 ': r) a -> Sem (e4 ': e3 ': e2 ': e1 ': r) a
reverseEffects4 :: forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e4 : e3 : e2 : e1 : r) a
reverseEffects4 = forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e2 : e3 : e4 : e1 : r) a
rotateEffects4L forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(e3 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e2 : e3 : e1 : r) a
rotateEffects3L forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e2 : e1 : r) a
rotateEffects2
{-# INLINE reverseEffects4 #-}