{-# LANGUAGE AllowAmbiguousTypes #-}

-- SPDX-License-Identifier: MPL-2.0

{- |
Copyright   :  (c) 2024 Sayo Koyoneda
License     :  MPL-2.0 (see the LICENSE file)
Maintainer  :  ymdfield@outlook.jp

This module provides functions for transforming effects.
Please refer to the documentation of the [top-level module]("Control.Monad.Hefty").
-}
module Control.Monad.Hefty.Transform where

import Control.Effect (type (~>))
import Control.Monad.Hefty.Interpret (iterAllEffHFBy)
import Control.Monad.Hefty.Types (Eff, sendUnionBy, sendUnionHBy)
import Data.Effect.HFunctor (HFunctor)
import Data.Effect.Key (Key (Key, unKey), KeyH (KeyH, unKeyH), type (##>), type (#>))
import Data.Effect.OpenUnion.Internal (
    BundleUnder,
    Drop,
    IsSuffixOf,
    Split,
    Strengthen,
    StrengthenN,
    StrengthenNUnder,
    StrengthenUnder,
    Take,
    WeakenN,
    WeakenNUnder,
    WeakenUnder,
 )
import Data.Effect.OpenUnion.Internal.FO (
    Union,
    bundleAllUnion,
    bundleUnion,
    bundleUnionN,
    bundleUnionUnder,
    decomp,
    inj,
    nil,
    prj,
    strengthen,
    strengthenN,
    strengthenNUnder,
    strengthenUnder,
    strengthens,
    strengthensUnder,
    unbundleAllUnion,
    unbundleUnion,
    unbundleUnionN,
    unbundleUnionUnder,
    weaken,
    weakenN,
    weakenNUnder,
    weakenUnder,
    weakens,
    weakensUnder,
    type (<|),
 )
import Data.Effect.OpenUnion.Internal.HO (
    UnionH,
    bundleAllUnionH,
    bundleUnionH,
    bundleUnionUnderH,
    decompH,
    hfmapUnion,
    injH,
    nilH,
    prjH,
    strengthenH,
    strengthenNH,
    strengthenNUnderH,
    strengthenUnderH,
    strengthensH,
    unbundleAllUnionH,
    unbundleUnionH,
    unbundleUnionUnderH,
    weakenH,
    weakenNH,
    weakenNUnderH,
    weakenUnderH,
    weakensH,
    type (<<|),
 )
import Data.Effect.Tag (Tag (Tag, unTag), TagH (TagH, unTagH), type (#), type (##))
import GHC.TypeNats (KnownNat)

-- * Rewriting effectful operations

{- | Transforms the first-order effect @e@ at the head of the list into another
first-order effect @e'@.
-}
transform
    :: forall e e' ef eh
     . (e ~> e')
    -> Eff eh (e ': ef) ~> Eff eh (e' ': ef)
transform :: forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform e ~> e'
f = (Union (e : ef) ~> Union (e' : ef))
-> Eff eh (e : ef) ~> Eff eh (e' : ef)
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff ((Union ef x -> Union (e' : ef) x)
-> (e x -> Union (e' : ef) x)
-> Either (Union ef x) (e x)
-> Union (e' : ef) x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Union ef x -> Union (e' : ef) x
forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken (e' x -> Union (e' : ef) x
forall a. e' a -> Union (e' : ef) a
forall (e :: * -> *) (es :: [* -> *]) a.
Member e es =>
e a -> Union es a
inj (e' x -> Union (e' : ef) x)
-> (e x -> e' x) -> e x -> Union (e' : ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e x -> e' x
e ~> e'
f) (Either (Union ef x) (e x) -> Union (e' : ef) x)
-> (Union (e : ef) x -> Either (Union ef x) (e x))
-> Union (e : ef) x
-> Union (e' : ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union (e : ef) x -> Either (Union ef x) (e x)
forall (e :: * -> *) (es :: [* -> *]) a.
Union (e : es) a -> Either (Union es a) (e a)
decomp)
{-# INLINE transform #-}

{- | Transforms the higher-order effect @e@ at the head of the list into another
higher-order effect @e'@.
-}
transformH
    :: forall e e' eh ef
     . (HFunctor e)
    => (e (Eff (e' ': eh) ef) ~> e' (Eff (e' ': eh) ef))
    -> Eff (e ': eh) ef ~> Eff (e' ': eh) ef
transformH :: forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef)
f = (UnionH (e : eh) (Eff (e' : eh) ef)
 ~> UnionH (e' : eh) (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH ((UnionH eh (Eff (e' : eh) ef) x
 -> UnionH (e' : eh) (Eff (e' : eh) ef) x)
-> (e (Eff (e' : eh) ef) x
    -> UnionH (e' : eh) (Eff (e' : eh) ef) x)
-> Either (UnionH eh (Eff (e' : eh) ef) x) (e (Eff (e' : eh) ef) x)
-> UnionH (e' : eh) (Eff (e' : eh) ef) x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either UnionH eh (Eff (e' : eh) ef) x
-> UnionH (e' : eh) (Eff (e' : eh) ef) x
forall (any :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
UnionH es f a -> UnionH (any : es) f a
weakenH (e' (Eff (e' : eh) ef) x -> UnionH (e' : eh) (Eff (e' : eh) ef) x
forall (f :: * -> *) a. e' f a -> UnionH (e' : eh) f a
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
MemberH e es =>
e f a -> UnionH es f a
injH (e' (Eff (e' : eh) ef) x -> UnionH (e' : eh) (Eff (e' : eh) ef) x)
-> (e (Eff (e' : eh) ef) x -> e' (Eff (e' : eh) ef) x)
-> e (Eff (e' : eh) ef) x
-> UnionH (e' : eh) (Eff (e' : eh) ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e (Eff (e' : eh) ef) x -> e' (Eff (e' : eh) ef) x
e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef)
f) (Either (UnionH eh (Eff (e' : eh) ef) x) (e (Eff (e' : eh) ef) x)
 -> UnionH (e' : eh) (Eff (e' : eh) ef) x)
-> (UnionH (e : eh) (Eff (e' : eh) ef) x
    -> Either
         (UnionH eh (Eff (e' : eh) ef) x) (e (Eff (e' : eh) ef) x))
-> UnionH (e : eh) (Eff (e' : eh) ef) x
-> UnionH (e' : eh) (Eff (e' : eh) ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH (e : eh) (Eff (e' : eh) ef) x
-> Either (UnionH eh (Eff (e' : eh) ef) x) (e (Eff (e' : eh) ef) x)
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
HFunctor e =>
UnionH (e : es) f a -> Either (UnionH es f a) (e f a)
decompH)
{-# INLINE transformH #-}

{- | Transforms the first-order effect @e@ at the head of the list into another
first-order effect @e'@ and embeds it into the list.

If multiple instances of @e'@ exist in the list, the one closest to the head
(with the smallest index) will be targeted.
-}
translate
    :: forall e e' ef eh
     . (e' <| ef)
    => (e ~> e')
    -> Eff eh (e ': ef) ~> Eff eh ef
translate :: forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e' <| ef) =>
(e ~> e') -> Eff eh (e : ef) ~> Eff eh ef
translate e ~> e'
f = (Union (e : ef) ~> Union ef) -> Eff eh (e : ef) ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff ((Union ef x -> Union ef x)
-> (e x -> Union ef x) -> Either (Union ef x) (e x) -> Union ef x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Union ef x -> Union ef x
forall a. a -> a
id (e' x -> Union ef x
forall a. e' a -> Union ef a
forall (e :: * -> *) (es :: [* -> *]) a.
Member e es =>
e a -> Union es a
inj (e' x -> Union ef x) -> (e x -> e' x) -> e x -> Union ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e x -> e' x
e ~> e'
f) (Either (Union ef x) (e x) -> Union ef x)
-> (Union (e : ef) x -> Either (Union ef x) (e x))
-> Union (e : ef) x
-> Union ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union (e : ef) x -> Either (Union ef x) (e x)
forall (e :: * -> *) (es :: [* -> *]) a.
Union (e : es) a -> Either (Union es a) (e a)
decomp)
{-# INLINE translate #-}

{- | Transforms the higher-order effect @e@ at the head of the list into another
higher-order effect @e'@ and embeds it into the list.

If multiple instances of @e'@ exist in the list, the one closest to the head
(with the smallest index) will be targeted.
-}
translateH
    :: forall e e' eh ef
     . (e' <<| eh, HFunctor e)
    => (e (Eff eh ef) ~> e' (Eff eh ef))
    -> Eff (e ': eh) ef ~> Eff eh ef
translateH :: forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
(e' <<| eh, HFunctor e) =>
(e (Eff eh ef) ~> e' (Eff eh ef)) -> Eff (e : eh) ef ~> Eff eh ef
translateH e (Eff eh ef) ~> e' (Eff eh ef)
f = (UnionH (e : eh) (Eff eh ef) ~> UnionH eh (Eff eh ef))
-> Eff (e : eh) ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH ((UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> (e (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> Either (UnionH eh (Eff eh ef) x) (e (Eff eh ef) x)
-> UnionH eh (Eff eh ef) x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh ef) x
forall a. a -> a
id (e' (Eff eh ef) x -> UnionH eh (Eff eh ef) x
forall (f :: * -> *) a. e' f a -> UnionH eh f a
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
MemberH e es =>
e f a -> UnionH es f a
injH (e' (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> (e (Eff eh ef) x -> e' (Eff eh ef) x)
-> e (Eff eh ef) x
-> UnionH eh (Eff eh ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e (Eff eh ef) x -> e' (Eff eh ef) x
e (Eff eh ef) ~> e' (Eff eh ef)
f) (Either (UnionH eh (Eff eh ef) x) (e (Eff eh ef) x)
 -> UnionH eh (Eff eh ef) x)
-> (UnionH (e : eh) (Eff eh ef) x
    -> Either (UnionH eh (Eff eh ef) x) (e (Eff eh ef) x))
-> UnionH (e : eh) (Eff eh ef) x
-> UnionH eh (Eff eh ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH (e : eh) (Eff eh ef) x
-> Either (UnionH eh (Eff eh ef) x) (e (Eff eh ef) x)
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
HFunctor e =>
UnionH (e : es) f a -> Either (UnionH es f a) (e f a)
decompH)
{-# INLINE translateH #-}

{- | Rewrites the first-order effect @e@ in the list.

If multiple instances of @e@ exist in the list, the one closest to the head
(with the smallest index) will be targeted.
-}
rewrite
    :: forall e ef eh
     . (e <| ef)
    => (e ~> e)
    -> Eff eh ef ~> Eff eh ef
rewrite :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]).
(e <| ef) =>
(e ~> e) -> Eff eh ef ~> Eff eh ef
rewrite e ~> e
f = (Union ef ~> Union ef) -> Eff eh ef ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff \Union ef x
u -> Union ef x -> (e x -> Union ef x) -> Maybe (e x) -> Union ef x
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Union ef x
u (e x -> Union ef x
forall a. e a -> Union ef a
forall (e :: * -> *) (es :: [* -> *]) a.
Member e es =>
e a -> Union es a
inj (e x -> Union ef x) -> (e x -> e x) -> e x -> Union ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e x -> e x
e ~> e
f) (Maybe (e x) -> Union ef x) -> Maybe (e x) -> Union ef x
forall a b. (a -> b) -> a -> b
$ forall (e :: * -> *) (es :: [* -> *]) a.
Member e es =>
Union es a -> Maybe (e a)
prj @e Union ef x
u
{-# INLINE rewrite #-}

{- | Rewrites the higher-order effect @e@ in the list.

If multiple instances of @e@ exist in the list, the one closest to the head
(with the smallest index) will be targeted.
-}
rewriteH
    :: forall e eh ef
     . (e <<| eh, HFunctor e)
    => (e (Eff eh ef) ~> e (Eff eh ef))
    -> Eff eh ef ~> Eff eh ef
rewriteH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
(e <<| eh, HFunctor e) =>
(e (Eff eh ef) ~> e (Eff eh ef)) -> Eff eh ef ~> Eff eh ef
rewriteH e (Eff eh ef) ~> e (Eff eh ef)
f = (UnionH eh (Eff eh ef) ~> UnionH eh (Eff eh ef))
-> Eff eh ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH \UnionH eh (Eff eh ef) x
u -> UnionH eh (Eff eh ef) x
-> (e (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> Maybe (e (Eff eh ef) x)
-> UnionH eh (Eff eh ef) x
forall b a. b -> (a -> b) -> Maybe a -> b
maybe UnionH eh (Eff eh ef) x
u (e (Eff eh ef) x -> UnionH eh (Eff eh ef) x
forall (f :: * -> *) a. e f a -> UnionH eh f a
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
MemberH e es =>
e f a -> UnionH es f a
injH (e (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> (e (Eff eh ef) x -> e (Eff eh ef) x)
-> e (Eff eh ef) x
-> UnionH eh (Eff eh ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e (Eff eh ef) x -> e (Eff eh ef) x
e (Eff eh ef) ~> e (Eff eh ef)
f) (Maybe (e (Eff eh ef) x) -> UnionH eh (Eff eh ef) x)
-> Maybe (e (Eff eh ef) x) -> UnionH eh (Eff eh ef) x
forall a b. (a -> b) -> a -> b
$ forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
(MemberH e es, HFunctor e) =>
UnionH es f a -> Maybe (e f a)
prjH @e UnionH eh (Eff eh ef) x
u
{-# INLINE rewriteH #-}

-- | Transforms all first-order effects in the open union at once.
transEff
    :: forall ef ef' eh
     . (Union ef ~> Union ef')
    -> Eff eh ef ~> Eff eh ef'
transEff :: forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff = (UnionH eh (Eff eh ef') ~> UnionH eh (Eff eh ef'))
-> (forall {x}. Union ef x -> Union ef' x)
-> forall {x}. Eff eh ef x -> Eff eh ef' x
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *])
       (ef' :: [* -> *]).
(UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
-> (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh' ef'
transEffHF UnionH eh (Eff eh ef') x -> UnionH eh (Eff eh ef') x
forall a. a -> a
UnionH eh (Eff eh ef') ~> UnionH eh (Eff eh ef')
id
{-# INLINE transEff #-}

-- | Transforms all higher-order effects in the open union at once.
transEffH
    :: forall eh eh' ef
     . (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
    -> Eff eh ef ~> Eff eh' ef
transEffH :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef)
f = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> (Union ef ~> Union ef) -> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *])
       (ef' :: [* -> *]).
(UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
-> (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh' ef'
transEffHF UnionH eh (Eff eh' ef) x -> UnionH eh' (Eff eh' ef) x
UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef)
f Union ef x -> Union ef x
forall a. a -> a
Union ef ~> Union ef
id
{-# INLINE transEffH #-}

{- | Transforms all higher-order and first-order effects in the open union at
once.
-}
transEffHF
    :: forall eh eh' ef ef'
     . (UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
    -> (Union ef ~> Union ef')
    -> Eff eh ef ~> Eff eh' ef'
transEffHF :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *])
       (ef' :: [* -> *]).
(UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
-> (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh' ef'
transEffHF UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef')
fh Union ef ~> Union ef'
ff = Eff eh ef x -> Eff eh' ef' x
Eff eh ef ~> Eff eh' ef'
loop
  where
    loop :: Eff eh ef ~> Eff eh' ef'
    loop :: Eff eh ef ~> Eff eh' ef'
loop =
        (x -> Eff eh' ef' x)
-> Interpreter (UnionH eh (Eff eh ef)) (Eff eh' ef') x
-> Interpreter (Union ef) (Eff eh' ef') x
-> Eff eh ef x
-> Eff eh' ef' x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy
            x -> Eff eh' ef' x
forall a. a -> Eff eh' ef' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (((x -> Eff eh' ef' x)
 -> UnionH eh' (Eff eh' ef') x -> Eff eh' ef' x)
-> UnionH eh' (Eff eh' ef') x
-> (x -> Eff eh' ef' x)
-> Eff eh' ef' x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh' ef' x) -> UnionH eh' (Eff eh' ef') x -> Eff eh' ef' x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
sendUnionHBy (UnionH eh' (Eff eh' ef') x
 -> (x -> Eff eh' ef' x) -> Eff eh' ef' x)
-> (UnionH eh (Eff eh ef) x -> UnionH eh' (Eff eh' ef') x)
-> UnionH eh (Eff eh ef) x
-> (x -> Eff eh' ef' x)
-> Eff eh' ef' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH eh (Eff eh' ef') x -> UnionH eh' (Eff eh' ef') x
UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef')
fh (UnionH eh (Eff eh' ef') x -> UnionH eh' (Eff eh' ef') x)
-> (UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh' ef') x)
-> UnionH eh (Eff eh ef) x
-> UnionH eh' (Eff eh' ef') x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff eh ef ~> Eff eh' ef')
-> UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh' ef') x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh ef x -> Eff eh' ef' x
Eff eh ef ~> Eff eh' ef'
loop)
            (((x -> Eff eh' ef' x) -> Union ef' x -> Eff eh' ef' x)
-> Union ef' x -> (x -> Eff eh' ef' x) -> Eff eh' ef' x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh' ef' x) -> Union ef' x -> Eff eh' ef' x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy (Union ef' x -> (x -> Eff eh' ef' x) -> Eff eh' ef' x)
-> (Union ef x -> Union ef' x)
-> Union ef x
-> (x -> Eff eh' ef' x)
-> Eff eh' ef' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union ef x -> Union ef' x
Union ef ~> Union ef'
ff)
{-# INLINE transEffHF #-}

-- * Manipulating the effect list (without rewriting effectful operations)

-- ** Insertion functions

-- | Adds an arbitrary first-order effect @e@ to the head of the list.
raise :: forall e ef eh. Eff eh ef ~> Eff eh (e ': ef)
raise :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) x.
Eff eh ef x -> Eff eh (e : ef) x
raise = (Union ef ~> Union (e : ef)) -> Eff eh ef ~> Eff eh (e : ef)
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union ef x -> Union (e : ef) x
Union ef ~> Union (e : ef)
forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken
{-# INLINE raise #-}

-- | Adds multiple arbitrary first-order effects to the head of the list.
raises :: (ef `IsSuffixOf` ef') => Eff eh ef ~> Eff eh ef'
raises :: forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
IsSuffixOf ef ef' =>
Eff eh ef ~> Eff eh ef'
raises = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union ef x -> Union ef' x
forall (es :: [* -> *]) (es' :: [* -> *]) a.
IsSuffixOf es es' =>
Union es a -> Union es' a
Union ef ~> Union ef'
weakens
{-# INLINE raises #-}

{- | Adds a specified number @len@ of arbitrary first-order effects to the head
of the list.
-}
raiseN
    :: forall len ef ef' eh
     . (WeakenN len ef ef')
    => Eff eh ef ~> Eff eh ef'
raiseN :: forall (len :: Natural) (ef :: [* -> *]) (ef' :: [* -> *])
       (eh :: [EffectH]).
WeakenN len ef ef' =>
Eff eh ef ~> Eff eh ef'
raiseN = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (len :: Natural) (es :: [* -> *]) (es' :: [* -> *]) a.
WeakenN len es es' =>
Union es a -> Union es' a
weakenN @len)
{-# INLINE raiseN #-}

-- | Raises an empty first-order effect list to an arbitrary effect list.
raiseAll :: Eff eh '[] ~> Eff eh ef
raiseAll :: forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh '[] x -> Eff eh ef x
raiseAll = (Union '[] ~> Union ef) -> Eff eh '[] ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union '[] x -> Union ef x
Union '[] ~> Union ef
forall a r. Union '[] a -> r
nil
{-# INLINE raiseAll #-}

{- | Inserts an arbitrary first-order effect @e2@ just below the head of the
list.
-}
raiseUnder
    :: forall e1 e2 ef eh
     . Eff eh (e1 ': ef) ~> Eff eh (e1 ': e2 ': ef)
raiseUnder :: forall (e1 :: * -> *) (e2 :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e1 : ef) x -> Eff eh (e1 : e2 : ef) x
raiseUnder = (Union (e1 : ef) ~> Union (e1 : e2 : ef))
-> Eff eh (e1 : ef) ~> Eff eh (e1 : e2 : ef)
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union (e1 : ef) x -> Union (e1 : e2 : ef) x
Union (e1 : ef) ~> Union (e1 : e2 : ef)
forall (any :: * -> *) (e :: * -> *) (es :: [* -> *]) a.
Union (e : es) a -> Union (e : any : es) a
weakenUnder
{-# INLINE raiseUnder #-}

{- | Inserts multiple arbitrary first-order effects at a position @offset@ steps
below the head of the list.
-}
raisesUnder
    :: forall offset ef ef' eh
     . (WeakenUnder offset ef ef')
    => Eff eh ef ~> Eff eh ef'
raisesUnder :: forall (offset :: Natural) (ef :: [* -> *]) (ef' :: [* -> *])
       (eh :: [EffectH]).
WeakenUnder offset ef ef' =>
Eff eh ef ~> Eff eh ef'
raisesUnder = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (offset :: Natural) (es :: [* -> *]) (es' :: [* -> *]) a.
WeakenUnder offset es es' =>
Union es a -> Union es' a
weakensUnder @offset)
{-# INLINE raisesUnder #-}

{- | Inserts @len@ arbitrary first-order effects at a position @offset@ steps
below the head of the list.
-}
raiseNUnder
    :: forall len offset ef ef' eh
     . (WeakenNUnder len offset ef ef')
    => Eff eh ef ~> Eff eh ef'
raiseNUnder :: forall (len :: Natural) (offset :: Natural) (ef :: [* -> *])
       (ef' :: [* -> *]) (eh :: [EffectH]).
WeakenNUnder len offset ef ef' =>
Eff eh ef ~> Eff eh ef'
raiseNUnder = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (len :: Natural) (offset :: Natural) (es :: [* -> *])
       (es' :: [* -> *]) a.
WeakenNUnder len offset es es' =>
Union es a -> Union es' a
weakenNUnder @len @offset)
{-# INLINE raiseNUnder #-}

{- | Adds a specified number @len@ of arbitrary higher-order effects to the head
of the list.
-}
raiseH :: forall e eh ef. Eff eh ef ~> Eff (e ': eh) ef
raiseH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh ef x -> Eff (e : eh) ef x
raiseH = (UnionH eh (Eff (e : eh) ef) ~> UnionH (e : eh) (Eff (e : eh) ef))
-> Eff eh ef ~> Eff (e : eh) ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH eh (Eff (e : eh) ef) x
-> UnionH (e : eh) (Eff (e : eh) ef) x
UnionH eh (Eff (e : eh) ef) ~> UnionH (e : eh) (Eff (e : eh) ef)
forall (any :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
UnionH es f a -> UnionH (any : es) f a
weakenH
{-# INLINE raiseH #-}

{- | Inserts an arbitrary higher-order effect @e2@ just below the head of the
list.
-}
raisesH :: (eh `IsSuffixOf` eh') => Eff eh ef ~> Eff eh' ef
raisesH :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
IsSuffixOf eh eh' =>
Eff eh ef ~> Eff eh' ef
raisesH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH eh (Eff eh' ef) x -> UnionH eh' (Eff eh' ef) x
forall (es :: [EffectH]) (es' :: [EffectH]) (f :: * -> *) a.
IsSuffixOf es es' =>
UnionH es f a -> UnionH es' f a
UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef)
weakensH
{-# INLINE raisesH #-}

{- | Adds a specified number @len@ of arbitrary higher-order effects to the head
of the list.
-}
raiseNH
    :: forall len eh eh' ef
     . (WeakenN len eh eh')
    => Eff eh ef ~> Eff eh' ef
raiseNH :: forall (len :: Natural) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]).
WeakenN len eh eh' =>
Eff eh ef ~> Eff eh' ef
raiseNH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH (forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
       (f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH @len)
{-# INLINE raiseNH #-}

-- | Raises an empty first-order effect list to an arbitrary effect list.
raiseAllH :: Eff '[] ef ~> Eff eh ef
raiseAllH :: forall (ef :: [* -> *]) (eh :: [EffectH]) x.
Eff '[] ef x -> Eff eh ef x
raiseAllH = (UnionH '[] (Eff eh ef) ~> UnionH eh (Eff eh ef))
-> Eff '[] ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH '[] (Eff eh ef) x -> UnionH eh (Eff eh ef) x
UnionH '[] (Eff eh ef) ~> UnionH eh (Eff eh ef)
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH
{-# INLINE raiseAllH #-}

{- | Inserts an arbitrary higher-order effect @e2@ just below the head of the
list.
-}
raiseUnderH
    :: forall e1 e2 eh ef
     . Eff (e1 ': eh) ef ~> Eff (e1 ': e2 ': eh) ef
raiseUnderH :: forall (e1 :: EffectH) (e2 :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]) x.
Eff (e1 : eh) ef x -> Eff (e1 : e2 : eh) ef x
raiseUnderH = (UnionH (e1 : eh) (Eff (e1 : e2 : eh) ef)
 ~> UnionH (e1 : e2 : eh) (Eff (e1 : e2 : eh) ef))
-> Eff (e1 : eh) ef ~> Eff (e1 : e2 : eh) ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH (e1 : eh) (Eff (e1 : e2 : eh) ef) x
-> UnionH (e1 : e2 : eh) (Eff (e1 : e2 : eh) ef) x
UnionH (e1 : eh) (Eff (e1 : e2 : eh) ef)
~> UnionH (e1 : e2 : eh) (Eff (e1 : e2 : eh) ef)
forall (any :: EffectH) (e :: EffectH) (es :: [EffectH])
       (f :: * -> *) a.
UnionH (e : es) f a -> UnionH (e : any : es) f a
weakenUnderH
{-# INLINE raiseUnderH #-}

{- | Inserts @len@ arbitrary higher-order effects at a position @offset@ steps
below the head of the list.
-}
raiseNUnderH
    :: forall len offset eh eh' ef
     . (WeakenNUnder len offset eh eh')
    => Eff eh ef ~> Eff eh' ef
raiseNUnderH :: forall (len :: Natural) (offset :: Natural) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]).
WeakenNUnder len offset eh eh' =>
Eff eh ef ~> Eff eh' ef
raiseNUnderH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH (forall (len :: Natural) (offset :: Natural) (es :: [EffectH])
       (es' :: [EffectH]) (f :: * -> *) a.
WeakenNUnder len offset es es' =>
UnionH es f a -> UnionH es' f a
weakenNUnderH @len @offset)
{-# INLINE raiseNUnderH #-}

-- ** Merging functions

{- | Merges the first first-order effect @e@ at the head of the list into the
same type of effect @e@ that is below it.

If multiple candidates of @e@ exist in the list, the one closest to the head
(with the smallest index) will be targeted.
-}
subsume
    :: forall e ef eh
     . (e <| ef)
    => Eff eh (e ': ef) ~> Eff eh ef
subsume :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]).
(e <| ef) =>
Eff eh (e : ef) ~> Eff eh ef
subsume = (Union (e : ef) ~> Union ef) -> Eff eh (e : ef) ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union (e : ef) x -> Union ef x
Union (e : ef) ~> Union ef
forall (e :: * -> *) (es :: [* -> *]) a.
(e <| es) =>
Union (e : es) a -> Union es a
strengthen
{-# INLINE subsume #-}

{- | Merges multiple first-order effects at the head of the list into effects of
the same types that are below them.
-}
subsumes
    :: forall ef ef' eh
     . (Strengthen ef ef')
    => Eff eh ef ~> Eff eh ef'
subsumes :: forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
Strengthen ef ef' =>
Eff eh ef ~> Eff eh ef'
subsumes = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union ef x -> Union ef' x
forall (es :: [* -> *]) (es' :: [* -> *]) a.
Strengthen es es' =>
Union es a -> Union es' a
Union ef ~> Union ef'
strengthens
{-# INLINE subsumes #-}

{- | Merges a specified number @len@ of first-order effects at the head of the
list into effects of the same types that are below them.
-}
subsumeN
    :: forall len ef ef' eh
     . (StrengthenN len ef ef')
    => Eff eh ef ~> Eff eh ef'
subsumeN :: forall (len :: Natural) (ef :: [* -> *]) (ef' :: [* -> *])
       (eh :: [EffectH]).
StrengthenN len ef ef' =>
Eff eh ef ~> Eff eh ef'
subsumeN = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (len :: Natural) (es :: [* -> *]) (es' :: [* -> *]) a.
StrengthenN len es es' =>
Union es a -> Union es' a
strengthenN @len)
{-# INLINE subsumeN #-}

{- | Merges the first-order effect @e2@ located just below the head into the
same type of effect @e2@ that is below it.
-}
subsumeUnder
    :: forall e2 e1 ef eh
     . (e2 <| ef)
    => Eff eh (e1 ': e2 ': ef) ~> Eff eh (e1 ': ef)
subsumeUnder :: forall (e2 :: * -> *) (e1 :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e2 <| ef) =>
Eff eh (e1 : e2 : ef) ~> Eff eh (e1 : ef)
subsumeUnder = (Union (e1 : e2 : ef) ~> Union (e1 : ef))
-> Eff eh (e1 : e2 : ef) ~> Eff eh (e1 : ef)
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union (e1 : e2 : ef) x -> Union (e1 : ef) x
Union (e1 : e2 : ef) ~> Union (e1 : ef)
forall (e2 :: * -> *) (e1 :: * -> *) (es :: [* -> *]) a.
(e2 <| es) =>
Union (e1 : e2 : es) a -> Union (e1 : es) a
strengthenUnder
{-# INLINE subsumeUnder #-}

{- | Merges multiple first-order effects at an @offset@ below the head into
effects of the same types that are below them.
-}
subsumesUnder
    :: forall offset ef ef' eh
     . (StrengthenUnder offset ef ef')
    => Eff eh ef ~> Eff eh ef'
subsumesUnder :: forall (offset :: Natural) (ef :: [* -> *]) (ef' :: [* -> *])
       (eh :: [EffectH]).
StrengthenUnder offset ef ef' =>
Eff eh ef ~> Eff eh ef'
subsumesUnder = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (offset :: Natural) (es :: [* -> *]) (es' :: [* -> *]) a.
StrengthenUnder offset es es' =>
Union es a -> Union es' a
strengthensUnder @offset)
{-# INLINE subsumesUnder #-}

{- | Merges @len@ first-order effects at an @offset@ below the head into effects
of the same types that are below them.
-}
subsumeNUnder
    :: forall len offset ef ef' eh
     . (StrengthenNUnder len offset ef ef')
    => Eff eh ef ~> Eff eh ef'
subsumeNUnder :: forall (len :: Natural) (offset :: Natural) (ef :: [* -> *])
       (ef' :: [* -> *]) (eh :: [EffectH]).
StrengthenNUnder len offset ef ef' =>
Eff eh ef ~> Eff eh ef'
subsumeNUnder = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (len :: Natural) (offset :: Natural) (es :: [* -> *])
       (es' :: [* -> *]) a.
StrengthenNUnder len offset es es' =>
Union es a -> Union es' a
strengthenNUnder @len @offset)
{-# INLINE subsumeNUnder #-}

{- | Merges the first higher-order effect @e@ at the head of the list into the
same type of effect @e@ that is below it.

If multiple candidates of @e@ exist in the list, the one closest to the head
(with the smallest index) will be targeted.
-}
subsumeH
    :: forall e eh ef
     . (e <<| eh)
    => Eff (e ': eh) ef ~> Eff eh ef
subsumeH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
(e <<| eh) =>
Eff (e : eh) ef ~> Eff eh ef
subsumeH = (UnionH (e : eh) (Eff eh ef) ~> UnionH eh (Eff eh ef))
-> Eff (e : eh) ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH (e : eh) (Eff eh ef) x -> UnionH eh (Eff eh ef) x
UnionH (e : eh) (Eff eh ef) ~> UnionH eh (Eff eh ef)
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
(e <<| es) =>
UnionH (e : es) f a -> UnionH es f a
strengthenH
{-# INLINE subsumeH #-}

{- | Merges multiple higher-order effects at the head of the list into effects of
the same types that are below them.
-}
subsumesH
    :: forall eh eh' ef
     . (Strengthen eh eh')
    => Eff eh ef ~> Eff eh' ef
subsumesH :: forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
Strengthen eh eh' =>
Eff eh ef ~> Eff eh' ef
subsumesH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH eh (Eff eh' ef) x -> UnionH eh' (Eff eh' ef) x
forall (es :: [EffectH]) (es' :: [EffectH]) (f :: * -> *) a.
Strengthen es es' =>
UnionH es f a -> UnionH es' f a
UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef)
strengthensH
{-# INLINE subsumesH #-}

{- | Merges a specified number @len@ of higher-order effects at the head of the
list into effects of the same types that are below them.
-}
subsumeNH
    :: forall len eh eh' ef
     . (StrengthenN len eh eh')
    => Eff eh ef ~> Eff eh' ef
subsumeNH :: forall (len :: Natural) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]).
StrengthenN len eh eh' =>
Eff eh ef ~> Eff eh' ef
subsumeNH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH (forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
       (f :: * -> *) a.
StrengthenN len es es' =>
UnionH es f a -> UnionH es' f a
strengthenNH @len)
{-# INLINE subsumeNH #-}

{- | Merges the higher-order effect @e2@ located just below the head into the
same type of effect @e2@ that is below it.
-}
subsumeUnderH
    :: forall e2 e1 eh ef
     . (e2 <<| eh)
    => Eff (e1 ': e2 ': eh) ef ~> Eff (e1 ': eh) ef
subsumeUnderH :: forall (e2 :: EffectH) (e1 :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
(e2 <<| eh) =>
Eff (e1 : e2 : eh) ef ~> Eff (e1 : eh) ef
subsumeUnderH = (UnionH (e1 : e2 : eh) (Eff (e1 : eh) ef)
 ~> UnionH (e1 : eh) (Eff (e1 : eh) ef))
-> Eff (e1 : e2 : eh) ef ~> Eff (e1 : eh) ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH (e1 : e2 : eh) (Eff (e1 : eh) ef) x
-> UnionH (e1 : eh) (Eff (e1 : eh) ef) x
UnionH (e1 : e2 : eh) (Eff (e1 : eh) ef)
~> UnionH (e1 : eh) (Eff (e1 : eh) ef)
forall (e2 :: EffectH) (e1 :: EffectH) (es :: [EffectH])
       (f :: * -> *) a.
(e2 <<| es) =>
UnionH (e1 : e2 : es) f a -> UnionH (e1 : es) f a
strengthenUnderH
{-# INLINE subsumeUnderH #-}

{- | Merges @len@ higher-order effects at an @offset@ below the head into effects
of the same types that are below them.
-}
subsumeNUnderH
    :: forall len offset eh eh' ef
     . (StrengthenNUnder len offset eh eh')
    => Eff eh ef ~> Eff eh' ef
subsumeNUnderH :: forall (len :: Natural) (offset :: Natural) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]).
StrengthenNUnder len offset eh eh' =>
Eff eh ef ~> Eff eh' ef
subsumeNUnderH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH (forall (len :: Natural) (offset :: Natural) (es :: [EffectH])
       (es' :: [EffectH]) (f :: * -> *) a.
StrengthenNUnder len offset es es' =>
UnionH es f a -> UnionH es' f a
strengthenNUnderH @len @offset)
{-# INLINE subsumeNUnderH #-}

-- ** Bundling functions

{- | Bundles several effects at the head of the list into a single element using
an open union.
-}
bundle
    :: forall ef bundle rest eh
     . (Split ef bundle rest)
    => Eff eh ef ~> Eff eh (Union bundle ': rest)
bundle :: forall (ef :: [* -> *]) (bundle :: [* -> *]) (rest :: [* -> *])
       (eh :: [EffectH]).
Split ef bundle rest =>
Eff eh ef ~> Eff eh (Union bundle : rest)
bundle = (Union ef ~> Union (Union bundle : rest))
-> Eff eh ef ~> Eff eh (Union bundle : rest)
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union ef x -> Union (Union bundle : rest) x
forall (es :: [* -> *]) (bundle :: [* -> *]) (rest :: [* -> *]) a.
Split es bundle rest =>
Union es a -> Union (Union bundle : rest) a
Union ef ~> Union (Union bundle : rest)
bundleUnion
{-# INLINE bundle #-}

{- | Bundles the first @len@ effects at the head of the list into a single
element using an open union.
-}
bundleN
    :: forall len ef eh
     . (KnownNat len)
    => Eff eh ef ~> Eff eh (Union (Take len ef) ': Drop len ef)
bundleN :: forall (len :: Natural) (ef :: [* -> *]) (eh :: [EffectH]).
KnownNat len =>
Eff eh ef ~> Eff eh (Union (Take len ef) : Drop len ef)
bundleN = (Union ef ~> Union (Union (Take len ef) : Drop len ef))
-> Eff eh ef ~> Eff eh (Union (Take len ef) : Drop len ef)
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (len :: Natural) (es :: [* -> *]) a.
KnownNat len =>
Union es a -> Union (Union (Take len es) : Drop len es) a
bundleUnionN @len)
{-# INLINE bundleN #-}

-- | Expands effects that have been bundled into an open union.
unbundle
    :: forall ef bundle rest eh
     . (Split ef bundle rest)
    => Eff eh (Union bundle ': rest) ~> Eff eh ef
unbundle :: forall (ef :: [* -> *]) (bundle :: [* -> *]) (rest :: [* -> *])
       (eh :: [EffectH]).
Split ef bundle rest =>
Eff eh (Union bundle : rest) ~> Eff eh ef
unbundle = (Union (Union bundle : rest) ~> Union ef)
-> Eff eh (Union bundle : rest) ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union (Union bundle : rest) x -> Union ef x
forall (es :: [* -> *]) (bundle :: [* -> *]) (rest :: [* -> *]) a.
Split es bundle rest =>
Union (Union bundle : rest) a -> Union es a
Union (Union bundle : rest) ~> Union ef
unbundleUnion
{-# INLINE unbundle #-}

-- | Expands the first @len@ effects that have been bundled into an open union.
unbundleN
    :: forall len ef eh
     . (KnownNat len)
    => Eff eh (Union (Take len ef) ': Drop len ef) ~> Eff eh ef
unbundleN :: forall (len :: Natural) (ef :: [* -> *]) (eh :: [EffectH]).
KnownNat len =>
Eff eh (Union (Take len ef) : Drop len ef) ~> Eff eh ef
unbundleN = (Union (Union (Take len ef) : Drop len ef) ~> Union ef)
-> Eff eh (Union (Take len ef) : Drop len ef) ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (len :: Natural) (es :: [* -> *]) a.
KnownNat len =>
Union (Union (Take len es) : Drop len es) a -> Union es a
unbundleUnionN @len)
{-# INLINE unbundleN #-}

{- | Expands effects at an @offset@ below the head of the list into a single
element using an open union.
-}
bundleUnder
    :: forall offset bundle ef ef' eh
     . (BundleUnder Union offset ef ef' bundle)
    => Eff eh ef ~> Eff eh ef'
bundleUnder :: forall (offset :: Natural) (bundle :: [* -> *]) (ef :: [* -> *])
       (ef' :: [* -> *]) (eh :: [EffectH]).
BundleUnder Union offset ef ef' bundle =>
Eff eh ef ~> Eff eh ef'
bundleUnder = (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (offset :: Natural) (bundle :: [* -> *]) (es :: [* -> *])
       (es' :: [* -> *]) a.
BundleUnder Union offset es es' bundle =>
Union es a -> Union es' a
bundleUnionUnder @offset)
{-# INLINE bundleUnder #-}

-- TODO: add *bundle*N(H) functions

{- | Expands effects that have been bundled into an open union at an @offset@
below the head of the list.
-}
unbundleUnder
    :: forall offset bundle ef ef' eh
     . (BundleUnder Union offset ef ef' bundle)
    => Eff eh ef' ~> Eff eh ef
unbundleUnder :: forall (offset :: Natural) (bundle :: [* -> *]) (ef :: [* -> *])
       (ef' :: [* -> *]) (eh :: [EffectH]).
BundleUnder Union offset ef ef' bundle =>
Eff eh ef' ~> Eff eh ef
unbundleUnder = (Union ef' ~> Union ef) -> Eff eh ef' ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff (forall (offset :: Natural) (bundle :: [* -> *]) (es :: [* -> *])
       (es' :: [* -> *]) a.
BundleUnder Union offset es es' bundle =>
Union es' a -> Union es a
unbundleUnionUnder @offset)
{-# INLINE unbundleUnder #-}

-- | Bundles all first-order effects into a single open union.
bundleAll :: Eff eh ef ~> Eff eh '[Union ef]
bundleAll :: forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh ef x -> Eff eh '[Union ef] x
bundleAll = (Union ef ~> Union '[Union ef]) -> Eff eh ef ~> Eff eh '[Union ef]
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union ef x -> Union '[Union ef] x
forall (es :: [* -> *]) a. Union es a -> Union '[Union es] a
Union ef ~> Union '[Union ef]
bundleAllUnion
{-# INLINE bundleAll #-}

-- | Expands all first-order effects from a single open union.
unbundleAll :: Eff eh '[Union ef] ~> Eff eh ef
unbundleAll :: forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh '[Union ef] x -> Eff eh ef x
unbundleAll = (Union '[Union ef] ~> Union ef) -> Eff eh '[Union ef] ~> Eff eh ef
forall (ef :: [* -> *]) (ef' :: [* -> *]) (eh :: [EffectH]).
(Union ef ~> Union ef') -> Eff eh ef ~> Eff eh ef'
transEff Union '[Union ef] x -> Union ef x
forall (es :: [* -> *]) a. Union '[Union es] a -> Union es a
Union '[Union ef] ~> Union ef
unbundleAllUnion
{-# INLINE unbundleAll #-}

{- | Bundles several effects at the head of the list into a single element using
an open union.
-}
bundleH
    :: forall eh bundle rest ef
     . (Split eh bundle rest)
    => Eff eh ef ~> Eff (UnionH bundle ': rest) ef
bundleH :: forall (eh :: [EffectH]) (bundle :: [EffectH]) (rest :: [EffectH])
       (ef :: [* -> *]).
Split eh bundle rest =>
Eff eh ef ~> Eff (UnionH bundle : rest) ef
bundleH = (UnionH eh (Eff (UnionH bundle : rest) ef)
 ~> UnionH (UnionH bundle : rest) (Eff (UnionH bundle : rest) ef))
-> Eff eh ef ~> Eff (UnionH bundle : rest) ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH eh (Eff (UnionH bundle : rest) ef) x
-> UnionH (UnionH bundle : rest) (Eff (UnionH bundle : rest) ef) x
forall (bundle :: [EffectH]) (es :: [EffectH]) (rest :: [EffectH])
       (f :: * -> *) a.
Split es bundle rest =>
UnionH es f a -> UnionH (UnionH bundle : rest) f a
UnionH eh (Eff (UnionH bundle : rest) ef)
~> UnionH (UnionH bundle : rest) (Eff (UnionH bundle : rest) ef)
bundleUnionH
{-# INLINE bundleH #-}

-- | Expands effects that have been bundled into an open union.
unbundleH
    :: forall eh bundle rest ef
     . (Split eh bundle rest)
    => Eff (UnionH bundle ': rest) ef ~> Eff eh ef
unbundleH :: forall (eh :: [EffectH]) (bundle :: [EffectH]) (rest :: [EffectH])
       (ef :: [* -> *]).
Split eh bundle rest =>
Eff (UnionH bundle : rest) ef ~> Eff eh ef
unbundleH = (UnionH (UnionH bundle : rest) (Eff eh ef)
 ~> UnionH eh (Eff eh ef))
-> Eff (UnionH bundle : rest) ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH (UnionH bundle : rest) (Eff eh ef) x
-> UnionH eh (Eff eh ef) x
forall (bundle :: [EffectH]) (es :: [EffectH]) (rest :: [EffectH])
       (f :: * -> *) a.
Split es bundle rest =>
UnionH (UnionH bundle : rest) f a -> UnionH es f a
UnionH (UnionH bundle : rest) (Eff eh ef) ~> UnionH eh (Eff eh ef)
unbundleUnionH
{-# INLINE unbundleH #-}

{- | Expands effects at an @offset@ below the head of the list into a single
element using an open union.
-}
bundleUnderH
    :: forall offset bundle eh eh' ef
     . (BundleUnder UnionH offset eh eh' bundle)
    => Eff eh ef ~> Eff eh' ef
bundleUnderH :: forall (offset :: Natural) (bundle :: [EffectH]) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]).
BundleUnder UnionH offset eh eh' bundle =>
Eff eh ef ~> Eff eh' ef
bundleUnderH = (UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH (forall (offset :: Natural) (bundle :: [EffectH]) (es :: [EffectH])
       (es' :: [EffectH]) (f :: * -> *) a.
BundleUnder UnionH offset es es' bundle =>
UnionH es f a -> UnionH es' f a
bundleUnionUnderH @offset)
{-# INLINE bundleUnderH #-}

{- | Expands effects that have been bundled into an open union at an @offset@
below the head of the list.
-}
unbundleUnderH
    :: forall offset bundle eh eh' ef
     . (BundleUnder UnionH offset eh eh' bundle)
    => Eff eh' ef ~> Eff eh ef
unbundleUnderH :: forall (offset :: Natural) (bundle :: [EffectH]) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]).
BundleUnder UnionH offset eh eh' bundle =>
Eff eh' ef ~> Eff eh ef
unbundleUnderH = (UnionH eh' (Eff eh ef) ~> UnionH eh (Eff eh ef))
-> Eff eh' ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH (forall (offset :: Natural) (bundle :: [EffectH]) (es :: [EffectH])
       (es' :: [EffectH]) (f :: * -> *) a.
BundleUnder UnionH offset es es' bundle =>
UnionH es' f a -> UnionH es f a
unbundleUnionUnderH @offset)
{-# INLINE unbundleUnderH #-}

-- | Bundles all higher-order effects into a single open union.
bundleAllH :: Eff eh ef ~> Eff '[UnionH eh] ef
bundleAllH :: forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh ef x -> Eff '[UnionH eh] ef x
bundleAllH = (UnionH eh (Eff '[UnionH eh] ef)
 ~> UnionH '[UnionH eh] (Eff '[UnionH eh] ef))
-> Eff eh ef ~> Eff '[UnionH eh] ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH eh (Eff '[UnionH eh] ef) x
-> UnionH '[UnionH eh] (Eff '[UnionH eh] ef) x
forall (es :: [EffectH]) (f :: * -> *) a.
UnionH es f a -> UnionH '[UnionH es] f a
UnionH eh (Eff '[UnionH eh] ef)
~> UnionH '[UnionH eh] (Eff '[UnionH eh] ef)
bundleAllUnionH
{-# INLINE bundleAllH #-}

-- | Expands all higher-order effects from a single open union.
unbundleAllH :: Eff '[UnionH eh] ef ~> Eff eh ef
unbundleAllH :: forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff '[UnionH eh] ef x -> Eff eh ef x
unbundleAllH = (UnionH '[UnionH eh] (Eff eh ef) ~> UnionH eh (Eff eh ef))
-> Eff '[UnionH eh] ef ~> Eff eh ef
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *]).
(UnionH eh (Eff eh' ef) ~> UnionH eh' (Eff eh' ef))
-> Eff eh ef ~> Eff eh' ef
transEffH UnionH '[UnionH eh] (Eff eh ef) x -> UnionH eh (Eff eh ef) x
forall (es :: [EffectH]) (f :: * -> *) a.
UnionH '[UnionH es] f a -> UnionH es f a
UnionH '[UnionH eh] (Eff eh ef) ~> UnionH eh (Eff eh ef)
unbundleAllUnionH
{-# INLINE unbundleAllH #-}

-- ** Manipulating Tags & Keys

-- | Attaches the @tag@ to the first-order effect at the head of the list.
tag
    :: forall tag e ef eh
     . Eff eh (e ': ef) ~> Eff eh (e # tag ': ef)
tag :: forall {k} (tag :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((e # tag) : ef) x
tag = (e ~> (e # tag)) -> Eff eh (e : ef) ~> Eff eh ((e # tag) : ef)
forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform e x -> Tag e tag x
e ~> (e # tag)
forall {k} (ins :: * -> *) (tag :: k) a. ins a -> Tag ins tag a
Tag
{-# INLINE tag #-}

-- | Removes the @tag@ from the tagged first-order effect at the head of the list.
untag
    :: forall tag e ef eh
     . Eff eh (e # tag ': ef) ~> Eff eh (e ': ef)
untag :: forall {k} (tag :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh ((e # tag) : ef) x -> Eff eh (e : ef) x
untag = ((e # tag) ~> e) -> Eff eh ((e # tag) : ef) ~> Eff eh (e : ef)
forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform Tag e tag x -> e x
(e # tag) ~> e
forall {k} (ins :: * -> *) (tag :: k) a. Tag ins tag a -> ins a
unTag
{-# INLINE untag #-}

{- | Changes the @tag@ of the tagged first-order effect at the head of the list
to another tag @tag'@.
-}
retag
    :: forall tag' tag e ef eh
     . Eff eh (e # tag ': ef) ~> Eff eh (e # tag' ': ef)
retag :: forall {k} {k} (tag' :: k) (tag :: k) (e :: * -> *)
       (ef :: [* -> *]) (eh :: [EffectH]) x.
Eff eh ((e # tag) : ef) x -> Eff eh ((e # tag') : ef) x
retag = ((e # tag) ~> (e # tag'))
-> Eff eh ((e # tag) : ef) ~> Eff eh ((e # tag') : ef)
forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform (((e # tag) ~> (e # tag'))
 -> Eff eh ((e # tag) : ef) ~> Eff eh ((e # tag') : ef))
-> ((e # tag) ~> (e # tag'))
-> Eff eh ((e # tag) : ef) ~> Eff eh ((e # tag') : ef)
forall a b. (a -> b) -> a -> b
$ e x -> Tag e tag' x
forall {k} (ins :: * -> *) (tag :: k) a. ins a -> Tag ins tag a
Tag (e x -> Tag e tag' x)
-> ((#) e tag x -> e x) -> (#) e tag x -> Tag e tag' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (#) e tag x -> e x
forall {k} (ins :: * -> *) (tag :: k) a. Tag ins tag a -> ins a
unTag
{-# INLINE retag #-}

-- | Attaches the @tag@ to the higher-order effect at the head of the list.
tagH
    :: forall tag e ef eh
     . (HFunctor e)
    => Eff (e ': eh) ef ~> Eff (e ## tag ': eh) ef
tagH :: forall {k} (tag :: k) (e :: EffectH) (ef :: [* -> *])
       (eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((e ## tag) : eh) ef
tagH = (e (Eff ((e ## tag) : eh) ef)
 ~> (##) e tag (Eff ((e ## tag) : eh) ef))
-> Eff (e : eh) ef ~> Eff ((e ## tag) : eh) ef
forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH e (Eff ((e ## tag) : eh) ef) x
-> TagH e tag (Eff ((e ## tag) : eh) ef) x
e (Eff ((e ## tag) : eh) ef)
~> (##) e tag (Eff ((e ## tag) : eh) ef)
forall {k} (sig :: EffectH) (tag :: k) (f :: * -> *) a.
sig f a -> TagH sig tag f a
TagH
{-# INLINE tagH #-}

{- | Removes the @tag@ from the tagged higher-order effect at the head of the
 list.
-}
untagH
    :: forall tag e eh ef
     . (HFunctor e)
    => Eff (e ## tag ': eh) ef ~> Eff (e ': eh) ef
untagH :: forall {k} (tag :: k) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
Eff ((e ## tag) : eh) ef ~> Eff (e : eh) ef
untagH = ((##) e tag (Eff (e : eh) ef) ~> e (Eff (e : eh) ef))
-> Eff ((e ## tag) : eh) ef ~> Eff (e : eh) ef
forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH TagH e tag (Eff (e : eh) ef) x -> e (Eff (e : eh) ef) x
(##) e tag (Eff (e : eh) ef) ~> e (Eff (e : eh) ef)
forall {k} (sig :: EffectH) (tag :: k) (f :: * -> *) a.
TagH sig tag f a -> sig f a
unTagH
{-# INLINE untagH #-}

{- | Changes the @tag@ of the tagged higher-order effect at the head of the list
to another tag @tag'@.
-}
retagH
    :: forall tag' tag e eh ef
     . (HFunctor e)
    => Eff (e ## tag ': eh) ef ~> Eff (e ## tag' ': eh) ef
retagH :: forall {k} {k} (tag' :: k) (tag :: k) (e :: EffectH)
       (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
Eff ((e ## tag) : eh) ef ~> Eff ((e ## tag') : eh) ef
retagH = ((##) e tag (Eff ((e ## tag') : eh) ef)
 ~> (##) e tag' (Eff ((e ## tag') : eh) ef))
-> Eff ((e ## tag) : eh) ef ~> Eff ((e ## tag') : eh) ef
forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH (((##) e tag (Eff ((e ## tag') : eh) ef)
  ~> (##) e tag' (Eff ((e ## tag') : eh) ef))
 -> Eff ((e ## tag) : eh) ef ~> Eff ((e ## tag') : eh) ef)
-> ((##) e tag (Eff ((e ## tag') : eh) ef)
    ~> (##) e tag' (Eff ((e ## tag') : eh) ef))
-> Eff ((e ## tag) : eh) ef ~> Eff ((e ## tag') : eh) ef
forall a b. (a -> b) -> a -> b
$ e (Eff ((e ## tag') : eh) ef) x
-> TagH e tag' (Eff ((e ## tag') : eh) ef) x
forall {k} (sig :: EffectH) (tag :: k) (f :: * -> *) a.
sig f a -> TagH sig tag f a
TagH (e (Eff ((e ## tag') : eh) ef) x
 -> TagH e tag' (Eff ((e ## tag') : eh) ef) x)
-> ((##) e tag (Eff ((e ## tag') : eh) ef) x
    -> e (Eff ((e ## tag') : eh) ef) x)
-> (##) e tag (Eff ((e ## tag') : eh) ef) x
-> TagH e tag' (Eff ((e ## tag') : eh) ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (##) e tag (Eff ((e ## tag') : eh) ef) x
-> e (Eff ((e ## tag') : eh) ef) x
forall {k} (sig :: EffectH) (tag :: k) (f :: * -> *) a.
TagH sig tag f a -> sig f a
unTagH
{-# INLINE retagH #-}

-- | Attaches the @key@ to the first-order effect at the head of the list.
key
    :: forall key e ef eh
     . Eff eh (e ': ef) ~> Eff eh (key #> e ': ef)
key :: forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((key #> e) : ef) x
key = (e ~> (key #> e)) -> Eff eh (e : ef) ~> Eff eh ((key #> e) : ef)
forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform e x -> Key key e x
e ~> (key #> e)
forall {k} (key :: k) (ins :: * -> *) a. ins a -> Key key ins a
Key
{-# INLINE key #-}

-- | Removes the @key@ from the keyed first-order effect at the head of the list.
unkey
    :: forall key e ef eh
     . Eff eh (key #> e ': ef) ~> Eff eh (e ': ef)
unkey :: forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh ((key #> e) : ef) x -> Eff eh (e : ef) x
unkey = ((key #> e) ~> e) -> Eff eh ((key #> e) : ef) ~> Eff eh (e : ef)
forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform Key key e x -> e x
(key #> e) ~> e
forall {k} (key :: k) (ins :: * -> *) a. Key key ins a -> ins a
unKey
{-# INLINE unkey #-}

{- | Changes the @key@ of the keyed first-order effect at the head of the list
to another key @key'@.
-}
rekey
    :: forall key' key e ef eh
     . Eff eh (key #> e ': ef) ~> Eff eh (key' #> e ': ef)
rekey :: forall {k} {k} (key' :: k) (key :: k) (e :: * -> *)
       (ef :: [* -> *]) (eh :: [EffectH]) x.
Eff eh ((key #> e) : ef) x -> Eff eh ((key' #> e) : ef) x
rekey = ((key #> e) ~> (key' #> e))
-> Eff eh ((key #> e) : ef) ~> Eff eh ((key' #> e) : ef)
forall (e :: * -> *) (e' :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]).
(e ~> e') -> Eff eh (e : ef) ~> Eff eh (e' : ef)
transform (((key #> e) ~> (key' #> e))
 -> Eff eh ((key #> e) : ef) ~> Eff eh ((key' #> e) : ef))
-> ((key #> e) ~> (key' #> e))
-> Eff eh ((key #> e) : ef) ~> Eff eh ((key' #> e) : ef)
forall a b. (a -> b) -> a -> b
$ e x -> Key key' e x
forall {k} (key :: k) (ins :: * -> *) a. ins a -> Key key ins a
Key (e x -> Key key' e x)
-> ((#>) key e x -> e x) -> (#>) key e x -> Key key' e x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (#>) key e x -> e x
forall {k} (key :: k) (ins :: * -> *) a. Key key ins a -> ins a
unKey
{-# INLINE rekey #-}

-- | Attaches the @key@ to the higher-order effect at the head of the list.
keyH
    :: forall key e ef eh
     . (HFunctor e)
    => Eff (e ': eh) ef ~> Eff (key ##> e ': eh) ef
keyH :: forall {k} (key :: k) (e :: EffectH) (ef :: [* -> *])
       (eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((key ##> e) : eh) ef
keyH = (e (Eff ((key ##> e) : eh) ef)
 ~> (##>) key e (Eff ((key ##> e) : eh) ef))
-> Eff (e : eh) ef ~> Eff ((key ##> e) : eh) ef
forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH e (Eff ((key ##> e) : eh) ef) x
-> KeyH key e (Eff ((key ##> e) : eh) ef) x
e (Eff ((key ##> e) : eh) ef)
~> (##>) key e (Eff ((key ##> e) : eh) ef)
forall {k} (key :: k) (sig :: EffectH) (f :: * -> *) a.
sig f a -> KeyH key sig f a
KeyH
{-# INLINE keyH #-}

-- | Removes the @key@ from the keyed higher-order effect at the head of the list.
unkeyH
    :: forall key e eh ef
     . (HFunctor e)
    => Eff (key ##> e ': eh) ef ~> Eff (e ': eh) ef
unkeyH :: forall {k} (key :: k) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
Eff ((key ##> e) : eh) ef ~> Eff (e : eh) ef
unkeyH = ((##>) key e (Eff (e : eh) ef) ~> e (Eff (e : eh) ef))
-> Eff ((key ##> e) : eh) ef ~> Eff (e : eh) ef
forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH KeyH key e (Eff (e : eh) ef) x -> e (Eff (e : eh) ef) x
(##>) key e (Eff (e : eh) ef) ~> e (Eff (e : eh) ef)
forall {k} (key :: k) (sig :: EffectH) (f :: * -> *) a.
KeyH key sig f a -> sig f a
unKeyH
{-# INLINE unkeyH #-}

{- | Changes the @key@ of the keyed higher-order effect at the head of the list
to another key @key'@.
-}
rekeyH
    :: forall key' key e eh ef
     . (HFunctor e)
    => Eff (key ##> e ': eh) ef ~> Eff (key' ##> e ': eh) ef
rekeyH :: forall {k} {k} (key' :: k) (key :: k) (e :: EffectH)
       (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
Eff ((key ##> e) : eh) ef ~> Eff ((key' ##> e) : eh) ef
rekeyH = ((##>) key e (Eff ((key' ##> e) : eh) ef)
 ~> (##>) key' e (Eff ((key' ##> e) : eh) ef))
-> Eff ((key ##> e) : eh) ef ~> Eff ((key' ##> e) : eh) ef
forall (e :: EffectH) (e' :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
(e (Eff (e' : eh) ef) ~> e' (Eff (e' : eh) ef))
-> Eff (e : eh) ef ~> Eff (e' : eh) ef
transformH (((##>) key e (Eff ((key' ##> e) : eh) ef)
  ~> (##>) key' e (Eff ((key' ##> e) : eh) ef))
 -> Eff ((key ##> e) : eh) ef ~> Eff ((key' ##> e) : eh) ef)
-> ((##>) key e (Eff ((key' ##> e) : eh) ef)
    ~> (##>) key' e (Eff ((key' ##> e) : eh) ef))
-> Eff ((key ##> e) : eh) ef ~> Eff ((key' ##> e) : eh) ef
forall a b. (a -> b) -> a -> b
$ e (Eff ((key' ##> e) : eh) ef) x
-> KeyH key' e (Eff ((key' ##> e) : eh) ef) x
forall {k} (key :: k) (sig :: EffectH) (f :: * -> *) a.
sig f a -> KeyH key sig f a
KeyH (e (Eff ((key' ##> e) : eh) ef) x
 -> KeyH key' e (Eff ((key' ##> e) : eh) ef) x)
-> ((##>) key e (Eff ((key' ##> e) : eh) ef) x
    -> e (Eff ((key' ##> e) : eh) ef) x)
-> (##>) key e (Eff ((key' ##> e) : eh) ef) x
-> KeyH key' e (Eff ((key' ##> e) : eh) ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (##>) key e (Eff ((key' ##> e) : eh) ef) x
-> e (Eff ((key' ##> e) : eh) ef) x
forall {k} (key :: k) (sig :: EffectH) (f :: * -> *) a.
KeyH key sig f a -> sig f a
unKeyH
{-# INLINE rekeyH #-}