module Control.Monad.Hefty.Provider (
module Control.Monad.Hefty.Provider,
module Data.Effect.Provider,
)
where
import Control.Monad.Hefty (
Eff,
HFunctor,
KeyH (KeyH),
MemberHBy,
Type,
interpretH,
key,
keyH,
transEffHF,
unkey,
unkeyH,
weaken,
weakenNH,
type (##>),
type (#>),
type (~>),
)
import Data.Effect.Provider
import Data.Functor.Const (Const (Const))
import Data.Functor.Identity (Identity (Identity))
type Provide ctx i sh sf eh ef = Provider ctx i (ProviderEff ctx i sh sf eh ef)
newtype ProviderEff ctx i sh sf eh ef p a
= ProviderEff {forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
ProviderEff ctx i sh sf eh ef p a
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
unProviderEff :: Eff (sh p ': Provide ctx i sh sf eh ef ': eh) (sf p ': ef) a}
type Provide_ i sh sf eh ef =
Provider (Const1 Identity) (Const i :: () -> Type) (Const1 (ProviderEff_ i sh sf eh ef))
newtype ProviderEff_ i sh sf eh ef a
= ProviderEff_ {forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]) a.
ProviderEff_ i sh sf eh ef a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
unProviderEff_ :: Eff (sh ': Provide_ i sh sf eh ef ': eh) (sf ': ef) a}
runProvider
:: forall ctx i sh sf eh ef
. ( forall p x
. i p
-> Eff (sh p ': Provide ctx i sh sf eh ef ': eh) (sf p ': ef) x
-> Eff (Provide ctx i sh sf eh ef ': eh) ef (ctx p x)
)
-> Eff (Provide ctx i sh sf eh ef ': eh) ef ~> Eff eh ef
runProvider :: forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]).
(forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x))
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
run =
(Provide ctx i sh sf eh ef ~~> Eff eh ef)
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH \(KeyH (Provide i p
i (forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1
f)) ->
(forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x))
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]).
(forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x))
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
run (Eff (Provide ctx i sh sf eh ef : eh) ef x -> Eff eh ef x)
-> Eff (Provide ctx i sh sf eh ef : eh) ef x -> Eff eh ef x
forall a b. (a -> b) -> a -> b
$
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p a1)
forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
run i p
i (ProviderEff ctx i sh sf eh ef p a1
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
ProviderEff ctx i sh sf eh ef p a
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
unProviderEff (ProviderEff ctx i sh sf eh ef p a1
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1)
-> ProviderEff ctx i sh sf eh ef p a1
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1
forall a b. (a -> b) -> a -> b
$ (forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1
f ((forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1)
-> (forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1
forall a b. (a -> b) -> a -> b
$ Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> ProviderEff ctx i sh sf eh ef p x
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
-> ProviderEff ctx i sh sf eh ef p a
ProviderEff (Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> ProviderEff ctx i sh sf eh ef p x)
-> (Eff eh ef x
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x)
-> Eff eh ef x
-> ProviderEff ctx i sh sf eh ef p x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnionH
eh (Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef))
~> UnionH
(sh p : Provide ctx i sh sf eh ef : eh)
(Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef)))
-> (Union ef ~> Union (sf p : ef))
-> Eff eh ef
~> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : 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 (forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH @2) Union ef x -> Union (sf p : ef) x
Union ef ~> Union (sf p : ef)
forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken)
runProvider_
:: forall i sh sf eh ef
. (HFunctor sh)
=> ( forall x
. i
-> Eff (sh ': Provide_ i sh sf eh ef ': eh) (sf ': ef) x
-> Eff (Provide_ i sh sf eh ef ': eh) ef x
)
-> Eff (Provide_ i sh sf eh ef ': eh) ef ~> Eff eh ef
runProvider_ :: forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]).
HFunctor sh =>
(forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider_ forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
run =
(Provide_ i sh sf eh ef ~~> Eff eh ef)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH \(KeyH (Provide (Const i
i) (forall x. Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
f)) ->
(forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]).
HFunctor sh =>
(forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider_ i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
run (Eff (Provide_ i sh sf eh ef : eh) ef x -> Eff eh ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef x -> Eff eh ef x
forall a b. (a -> b) -> a -> b
$
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
run
i
i
( (a1 -> x)
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
forall a b.
(a -> b)
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity a1 -> x
Identity a1 -> Const1 Identity p a1
forall {k} {k1} (f :: k -> *) (x :: k1) (a :: k).
f a -> Const1 f x a
Const1 (Identity a1 -> x) -> (a1 -> Identity a1) -> a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a1 -> Identity a1
forall a. a -> Identity a
Identity)
(Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x)
-> (Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderEff_ i sh sf eh ef a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]) a.
ProviderEff_ i sh sf eh ef a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
unProviderEff_
(ProviderEff_ i sh sf eh ef a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1)
-> (Const1 (ProviderEff_ i sh sf eh ef) p a1
-> ProviderEff_ i sh sf eh ef a1)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const1 (ProviderEff_ i sh sf eh ef) p a1
-> ProviderEff_ i sh sf eh ef a1
forall {k1} {k2} (f :: k1 -> *) (x :: k2) (a :: k1).
Const1 f x a -> f a
getConst1
(Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
forall a b. (a -> b) -> a -> b
$ (forall x. Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
f
((forall x. Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1)
-> (forall x.
Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
forall a b. (a -> b) -> a -> b
$ ProviderEff_ i sh sf eh ef x
-> Const1 (ProviderEff_ i sh sf eh ef) p x
forall {k} {k1} (f :: k -> *) (x :: k1) (a :: k).
f a -> Const1 f x a
Const1
(ProviderEff_ i sh sf eh ef x
-> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> (Eff eh ef x -> ProviderEff_ i sh sf eh ef x)
-> Eff eh ef x
-> Const1 (ProviderEff_ i sh sf eh ef) p x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> ProviderEff_ i sh sf eh ef x
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]) a.
Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
-> ProviderEff_ i sh sf eh ef a
ProviderEff_
(Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> ProviderEff_ i sh sf eh ef x)
-> (Eff eh ef x
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x)
-> Eff eh ef x
-> ProviderEff_ i sh sf eh ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnionH eh (Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef))
~> UnionH
(sh : Provide_ i sh sf eh ef : eh)
(Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef)))
-> (Union ef ~> Union (sf : ef))
-> Eff eh ef ~> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : 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 (forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH @2) Union ef x -> Union (sf : ef) x
Union ef ~> Union (sf : ef)
forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken
)
scope
:: forall key ctx i p eh ef a sh sf bh bf
. ( MemberHBy
(ProviderKey ctx i)
(Provider' ctx i (ProviderEff ctx i sh sf bh bf))
eh
, HFunctor (sh p)
)
=> i p
-> ( Eff eh ef ~> Eff (key ##> sh p ': Provide ctx i sh sf bh bf ': bh) (key #> sf p ': bf)
-> Eff (key ##> sh p ': Provide ctx i sh sf bh bf ': bh) (key #> sf p ': bf) a
)
-> Eff eh ef (ctx p a)
scope :: forall {k} {k} (key :: k) (ctx :: k -> * -> *) (i :: k -> *)
(p :: k) (eh :: [EffectH]) (ef :: [* -> *]) a (sh :: k -> EffectH)
(sf :: k -> * -> *) (bh :: [EffectH]) (bf :: [* -> *]).
(MemberHBy
(ProviderKey ctx i)
(Provider' ctx i (ProviderEff ctx i sh sf bh bf))
eh,
HFunctor (sh p)) =>
i p
-> ((Eff eh ef
~> Eff
((key ##> sh p) : Provide ctx i sh sf bh bf : bh)
((key #> sf p) : bf))
-> Eff
((key ##> sh p) : Provide ctx i sh sf bh bf : bh)
((key #> sf p) : bf)
a)
-> Eff eh ef (ctx p a)
scope i p
i (Eff eh ef
~> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf))
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
f =
i p
i i p
-> ((Eff eh ef ~> ProviderEff ctx i sh sf bh bf p)
-> ProviderEff ctx i sh sf bh bf p a)
-> Eff eh ef (ctx p a)
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (p :: k)
(f :: * -> *) a (b :: k -> * -> *).
SendHOEBy (ProviderKey ctx i) (Provider' ctx i b) f =>
i p -> ((f ~> b p) -> b p a) -> f (ctx p a)
..! \Eff eh ef ~> ProviderEff ctx i sh sf bh bf p
runInScope ->
Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
-> ProviderEff ctx i sh sf bh bf p a
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
-> ProviderEff ctx i sh sf eh ef p a
ProviderEff (Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
-> ProviderEff ctx i sh sf bh bf p a)
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
-> ProviderEff ctx i sh sf bh bf p a
forall a b. (a -> b) -> a -> b
$ Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
~> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
forall {k} (key :: k) (e :: EffectH) (eh :: [EffectH])
(ef :: [* -> *]).
HFunctor e =>
Eff ((key ##> e) : eh) ef ~> Eff (e : eh) ef
unkeyH (Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a)
-> (Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a)
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
(eh :: [EffectH]) x.
Eff eh ((key #> e) : ef) x -> Eff eh (e : ef) x
unkey (Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a)
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
a
forall a b. (a -> b) -> a -> b
$ (Eff eh ef
~> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf))
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
a
f (Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x
Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
~> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
forall {k} (key :: k) (e :: EffectH) (ef :: [* -> *])
(eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((key ##> e) : eh) ef
keyH (Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x)
-> (Eff eh ef x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x)
-> Eff eh ef x
-> Eff
((key ##> sh p)
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
(eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((key #> e) : ef) x
key (Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x)
-> (Eff eh ef x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
x)
-> Eff eh ef x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
((key #> sf p) : bf)
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderEff ctx i sh sf bh bf p x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
x
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
(sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
ProviderEff ctx i sh sf eh ef p a
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
unProviderEff (ProviderEff ctx i sh sf bh bf p x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
x)
-> (Eff eh ef x -> ProviderEff ctx i sh sf bh bf p x)
-> Eff eh ef x
-> Eff
(sh p
: (ProviderKey ctx i
##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
: bh)
(sf p : bf)
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff eh ef x -> ProviderEff ctx i sh sf bh bf p x
Eff eh ef ~> ProviderEff ctx i sh sf bh bf p
runInScope)
scope_
:: forall key i eh ef a sh sf bh bf
. ( MemberHBy
(ProviderKey (Const1 Identity :: () -> Type -> Type) (Const i :: () -> Type))
( Provider'
(Const1 Identity)
(Const i)
(Const1 (ProviderEff_ i sh sf bh bf))
)
eh
, HFunctor sh
)
=> i
-> ( Eff eh ef ~> Eff (key ##> sh ': Provide_ i sh sf bh bf ': bh) (key #> sf ': bf)
-> Eff (key ##> sh ': Provide_ i sh sf bh bf ': bh) (key #> sf ': bf) a
)
-> Eff eh ef a
scope_ :: forall {k} {k} (key :: k) i (eh :: [EffectH]) (ef :: [* -> *]) a
(sh :: EffectH) (sf :: * -> *) (bh :: [EffectH]) (bf :: [* -> *]).
(MemberHBy
(ProviderKey (Const1 Identity) (Const i))
(Provider'
(Const1 Identity) (Const i) (Const1 (ProviderEff_ i sh sf bh bf)))
eh,
HFunctor sh) =>
i
-> ((Eff eh ef
~> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf))
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a)
-> Eff eh ef a
scope_ i
i (Eff eh ef
~> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf))
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
f =
i
i i
-> ((Eff eh ef ~> ProviderEff_ i sh sf bh bf)
-> ProviderEff_ i sh sf bh bf a)
-> Eff eh ef a
forall {k} i (f :: * -> *) a (b :: * -> *).
(SendHOEBy
(ProviderKey (Const1 Identity) (Const i))
(Provider' (Const1 Identity) (Const i) (Const1 b))
f,
Functor f) =>
i -> ((f ~> b) -> b a) -> f a
.! \Eff eh ef ~> ProviderEff_ i sh sf bh bf
runInScope ->
Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> ProviderEff_ i sh sf bh bf a
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]) a.
Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
-> ProviderEff_ i sh sf eh ef a
ProviderEff_ (Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> ProviderEff_ i sh sf bh bf a)
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> ProviderEff_ i sh sf bh bf a
forall a b. (a -> b) -> a -> b
$ Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf)
~> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf)
forall {k} (key :: k) (e :: EffectH) (eh :: [EffectH])
(ef :: [* -> *]).
HFunctor e =>
Eff ((key ##> e) : eh) ef ~> Eff (e : eh) ef
unkeyH (Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a)
-> (Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a)
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
(eh :: [EffectH]) x.
Eff eh ((key #> e) : ef) x -> Eff eh (e : ef) x
unkey (Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a)
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
forall a b. (a -> b) -> a -> b
$ (Eff eh ef
~> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf))
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
f (Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf)
~> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf)
forall {k} (key :: k) (e :: EffectH) (ef :: [* -> *])
(eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((key ##> e) : eh) ef
keyH (Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x)
-> (Eff eh ef x
-> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x)
-> Eff eh ef x
-> Eff
((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
-> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
(eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((key #> e) : ef) x
key (Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
-> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x)
-> (Eff eh ef x
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x)
-> Eff eh ef x
-> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderEff_ i sh sf bh bf x
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
(ef :: [* -> *]) a.
ProviderEff_ i sh sf eh ef a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
unProviderEff_ (ProviderEff_ i sh sf bh bf x
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x)
-> (Eff eh ef x -> ProviderEff_ i sh sf bh bf x)
-> Eff eh ef x
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff eh ef x -> ProviderEff_ i sh sf bh bf x
Eff eh ef ~> ProviderEff_ i sh sf bh bf
runInScope)