| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Polysemy.Membership
Synopsis
- data ElemOf e r where
- membership :: Member e r => ElemOf e r
- sameMember :: forall e e' r. ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
- class KnownRow r
- tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r)
- subsumeUsing :: forall e r a. ElemOf e r -> Sem (e ': r) a -> Sem r a
- interceptUsing :: FirstOrder e "interceptUsing" => ElemOf e r -> (forall x rInitial. e (Sem rInitial) x -> Sem r x) -> Sem r a -> Sem r a
- interceptUsingH :: ElemOf e r -> (forall x rInitial. e (Sem rInitial) x -> Tactical e (Sem rInitial) r x) -> Sem r a -> Sem r a
Witnesses
data ElemOf e r where Source #
A proof that e is an element of r.
Due to technical reasons, is not powerful enough to
prove ElemOf e r; however, it can still be used send actions of Member e re
into r by using subsumeUsing.
Since: 1.3.0.0
membership :: Member e r => ElemOf e r Source #
Given , extract a proof that Member e re is an element of r.
sameMember :: forall e e' r. ElemOf e r -> ElemOf e' r -> Maybe (e :~: e') Source #
Checks if two membership proofs are equal. If they are, then that means that the effects for which membership is proven must also be equal.
Checking membership
A class for effect rows whose elements are inspectable.
This constraint is eventually satisfied as r is instantied to a
monomorphic list.
(E.g when r becomes something like
'[)State Int, Output String, Embed IO]
Minimal complete definition
tryMembership'
Instances
| KnownRow ('[] :: [a]) Source # | |
Defined in Polysemy.Internal.Union Methods tryMembership' :: forall (e :: a0). Typeable e => Maybe (ElemOf e '[]) | |
| (Typeable e, KnownRow r) => KnownRow (e ': r :: [a]) Source # | |
Defined in Polysemy.Internal.Union Methods tryMembership' :: forall (e0 :: a0). Typeable e0 => Maybe (ElemOf e0 (e ': r)) | |
tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r) Source #
Extracts a proof that e is an element of r if that
is indeed the case; otherwise returns Nothing.
Using membership
subsumeUsing :: forall e r a. ElemOf e r -> Sem (e ': r) a -> Sem r a Source #
Interprets an effect in terms of another identical effect, given an
explicit proof that the effect exists in r.
This is useful in conjunction with tryMembership
in order to conditionally make use of effects. For example:
tryListen ::KnownRowr =>Semr a -> Maybe (Semr ([Int], a)) tryListen m = casetryMembership@(Writer[Int]) of Just pr -> Just $subsumeUsingpr (listen(raisem)) _ -> Nothing
Since: 1.3.0.0
Arguments
| :: FirstOrder e "interceptUsing" | |
| => ElemOf e r | A proof that the handled effect exists in |
| -> (forall x rInitial. e (Sem rInitial) x -> Sem r x) | A natural transformation from the handled effect to other effects
already in |
| -> Sem r a | |
| -> Sem r a |
A variant of intercept that accepts an explicit proof that the effect
is in the effect stack rather then requiring a Member constraint.
This is useful in conjunction with tryMembership
in order to conditionally perform intercept.
Since: 1.3.0.0
Arguments
| :: ElemOf e r | A proof that the handled effect exists in |
| -> (forall x rInitial. e (Sem rInitial) x -> Tactical e (Sem rInitial) r x) | A natural transformation from the handled effect to other effects
already in |
| -> Sem r a | Unlike |
| -> Sem r a |
A variant of interceptH that accepts an explicit proof that the effect
is in the effect stack rather then requiring a Member constraint.
This is useful in conjunction with tryMembership
in order to conditionally perform interceptH.
See the notes on Tactical for how to use this function.
Since: 1.3.0.0