Polysemy.Membership · polysemy-1.9.2.0

Witnesses

5 declarations

newtypenewtype ElemOf (e :: k) (r :: [k])

A proof that e is an element of r.

Due to technical reasons, ElemOf e r is not powerful enough to prove Member e r; however, it can still be used send actions of e into r by using subsumeUsing.

patternpattern Here :: () => r ~ (e ': r') => ElemOf e r

#

patternpattern There :: () => r' ~ (e' ': r) => ElemOf e r -> ElemOf e r'

#

valuemembership :: Member e r => ElemOf e r

#

Given Member e r, extract a proof that e is an element of r.

valuesameMember :: ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')

#

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

2 declarations

classclass KnownRow (r :: [k]) where

#

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])

Instances2KnownRow

KnownRow '[]Defined in polysemy-1.9.2.0 · Polysemy.Internal.Union
(Typeable e, KnownRow r) => KnownRow (e ': r)Defined in polysemy-1.9.2.0 · Polysemy.Internal.Union

valuetryMembership :: (Typeable e, KnownRow r) => Maybe (ElemOf e r)

#

Extracts a proof that e is an element of r if that is indeed the case; otherwise returns Nothing.

Using membership

3 declarations

valuesubsumeUsing :: ElemOf e r -> Sem (e ': r) a -> Sem r a

#

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 :: KnownRow r => Sem r a -> Maybe (Sem r ([Int], a))
tryListen m = case tryMembership @(Writer [Int]) of
  Just pr -> Just $ subsumeUsing pr (listen (raise m))
  _       -> Nothing

valueinterceptUsing

:: FirstOrder e "interceptUsing"
=> ElemOf e r
A proof that the handled effect exists in r. This can be retrieved through membership or tryMembership.
-> (forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
A natural transformation from the handled effect to other effects already in Sem.
-> Sem r a
Unlike interpret, intercept does not consume any effects.
-> 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.

valueinterceptUsingH

:: ElemOf e r
A proof that the handled effect exists in r. This can be retrieved through membership or tryMembership.
-> (forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Tactical e (Sem rInitial) r x)
A natural transformation from the handled effect to other effects already in Sem.
-> Sem r a
Unlike interpretH, interceptUsingH does not consume any effects.
-> 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.