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

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

type Member e r = MemberNoError e r

A proof that the effect e is available somewhere inside of the effect stack r.

type MemberWithError e r = (MemberNoError e r, WhenStuck (LocateEffect e r) (AmbiguousSend e r))

Like Member, but will produce an error message if the types are ambiguous. This is the constraint used for actions generated by makeSem.

Be careful with this. Due to quirks of TypeError, the custom error messages emitted by this can potentially override other, more helpful error messages. See the discussion in Issue #227.

Since: 1.2.3.0

weave :: (Functor s, Functor n) => s () -> (forall x. s (m x) -> n (s x)) -> (forall x. s x -> Maybe x) -> Union r m a -> Union r n (s a)

hoist :: (forall x. m x -> n x) -> Union r m a -> Union r n a

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

Constructors

Here :: ElemOf e (e ': r)

e is located at the head of the list.

There :: ElemOf e r -> ElemOf e (e' ': r)

e is located somewhere in the tail of the list.

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

Defined in Polysemy.Internal.Union

Methods

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

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

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)

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.