Polysemy.Internal.Union

Documentation

data Union (r :: EffectRow) (mWoven :: Type -> Type) a where

An extensible, type-safe union. The r type parameter is a type-level list of effects, any one of which may be held within the Union.

Constructors

Union :: ElemOf e r -> Weaving e m a -> Union r m a

Instances

Functor (Union r mWoven)

Defined in Polysemy.Internal.Union

Methods

fmap :: (a -> b) -> Union r mWoven a -> Union r mWoven b

(<$) :: a -> Union r mWoven b -> Union r mWoven a

data Weaving e mAfter resultType where

Polysemy's core type that stores effect values together with information about the higher-order interpretation state of its construction site.

Constructors

Weaving

Fields

• :: forall f e rInitial a resultType mAfter. Functor f
• => { weaveEffect :: e (Sem rInitial) a

  The original effect GADT originally lifted via send. ^ rInitial is the effect row that was in scope when this Weaving was originally created.

•    , weaveState :: f ()

  A piece of state that other effects' interpreters have already woven through this Weaving. f is a Functor, so you can always fmap into this thing.

•    , weaveDistrib :: forall x. f (Sem rInitial x) -> mAfter (f x)

  Distribute f by transforming Sem rInitial into mAfter. This is usually of the form f (Sem (Some ': Effects ': r) x) -> Sem r (f x)

•    , weaveResult :: f a -> resultType

  Even though f a is the moral resulting type of Weaving, we can't expose that fact; such a thing would prevent Sem from being a Monad.

•    , weaveInspect :: forall x. f x -> Maybe x

  A function for attempting to see inside an f. This is no guarantees that such a thing will succeed (for example, Error might have thrown.)

•    } -> Weaving e mAfter resultType

Instances

Functor (Weaving e m)

Defined in Polysemy.Internal.Union

Methods

fmap :: (a -> b) -> Weaving e m a -> Weaving e m b

(<$) :: a -> Weaving e m b -> Weaving e m a

class Member (t :: Effect) (r :: EffectRow)

This class indicates that an effect must be present in the caller's stack. It is the main mechanism by which a program defines its effect dependencies.

Minimal complete definition

membership'

Instances

Member t z => Member t (_1 ': z)

Defined in Polysemy.Internal.Union

Methods

membership' :: ElemOf t (_1 ': z)

Member t (t ': z)

Defined in Polysemy.Internal.Union

Methods

membership' :: ElemOf t (t ': z)

Building Unions

inj :: forall e r rInitial a. Member e r => e (Sem rInitial) a -> Union r (Sem rInitial) a

Lift an effect e into a Union capable of holding it.

injUsing :: forall e r rInitial a. ElemOf e r -> e (Sem rInitial) a -> Union r (Sem rInitial) a

Lift an effect e into a Union capable of holding it, given an explicit proof that the effect exists in r

injWeaving :: forall e r m a. Member e r => Weaving e m a -> Union r m a

Lift a Weaving e into a Union capable of holding it.

weaken :: forall e r m a. Union r m a -> Union (e ': r) m a

Weaken a Union so it is capable of storing a new sort of effect at the head.

Using Unions

decomp :: Union (e ': r) m a -> Either (Union r m a) (Weaving e m a)

Decompose a Union. Either this union contains an effect e---the head of the r list---or it doesn't.

prj :: forall e r m a. Member e r => Union r m a -> Maybe (Weaving e m a)

Attempt to take an e effect out of a Union.

prjUsing :: forall e r m a. ElemOf e r -> Union r m a -> Maybe (Weaving e m a)

Attempt to take an e effect out of a Union, given an explicit proof that the effect exists in r.

extract :: Union '[e] m a -> Weaving e m a

Retrieve the last effect in a Union.

absurdU :: Union '[] m a -> b

An empty union contains nothing, so this function is uncallable.

decompCoerce :: Union (e ': r) m a -> Either (Union (f ': r) m a) (Weaving e m a)

Like decomp, but allows for a more efficient reinterpret function.

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.

extendMembershipLeft :: forall l r e. SList l -> ElemOf e r -> ElemOf e (Append l r)

Extends a proof that e is an element of r to a proof that e is an element of the concatenation of the lists l and r. l must be specified as a singleton list proof.

extendMembershipRight :: forall l r e. ElemOf e l -> ElemOf e (Append l r)

Extends a proof that e is an element of l to a proof that e is an element of the concatenation of the lists l and r.

injectMembership :: forall right e left mid. SList left -> SList mid -> ElemOf e (Append left right) -> ElemOf e (Append left (Append mid right))

Extends a proof that e is an element of left <> right to a proof that e is an element of left <> mid <> right. Both left and right must be specified as singleton list proofs.

weakenList :: SList l -> Union r m a -> Union (Append l r) m a

Weaken a Union so it is capable of storing a number of new effects at the head, specified as a singleton list proof.

weakenMid :: forall right m a left mid. SList left -> SList mid -> Union (Append left right) m a -> Union (Append left (Append mid right)) m a

Weaken a Union so it is capable of storing a number of new effects somewhere within the previous effect list. Both the prefix and the new effects are specified as singleton list proofs.