Polysemy.Membership

Witnesses

data ElemOf (e :: k) (r :: [k]) where

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.

Since: 1.3.0.0

Bundled Patterns

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

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

membership :: Member e r => ElemOf e r

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

sameMember :: forall e e' r. 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

class KnownRow r

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 ('[] :: [k])

Defined in Polysemy.Internal.Union

Methods

tryMembership' :: forall (e :: k0). Typeable e => Maybe (ElemOf e '[])

(Typeable e, KnownRow r) => KnownRow (e ': r :: [k])

Defined in Polysemy.Internal.Union

Methods

tryMembership' :: forall (e0 :: k0). Typeable e0 => Maybe (ElemOf e0 (e ': r))

tryMembership :: forall e r. (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

subsumeUsing :: forall e r a. 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

Since: 1.3.0.0

interceptUsing

Arguments

:: 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. 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.

Since: 1.3.0.0

interceptUsingH

Arguments

:: ElemOf e r

A proof that the handled effect exists in r. This can be retrieved through membership or tryMembership.

-> (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.

-> 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.

Since: 1.3.0.0