Modulepolysemy-1.9.2.0Haskell2010

Polysemy.Internal.Union

Contents

Building Unions
Using Unions
Witnesses
Checking membership

Synopsis

data Union
data Weaving
class Member
value weave
value hoist
value inj
value injUsing
value injWeaving
value weaken
value decomp
value prj
value prjUsing
value extract
value absurdU
value decompCoerce
newtype ElemOf
pattern Here
pattern There
value membership
value sameMember
class KnownRow
value tryMembership
value extendMembershipLeft
value extendMembershipRight
value injectMembership
value weakenList
value weakenMid

Packagepolysemy-1.9.2.0
Exports27
LanguageHaskell2010
LicenceBSD-3-Clause
SourceUnion.hs

datadata 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 mWoven a

Instances1Functor

Functor (Union r mWoven)Defined in polysemy-1.9.2.0 · Polysemy.Internal.Union

datadata Weaving (e :: (Type -> Type) -> Type -> Type) (mAfter :: Type -> Type) resultType where

Source#

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

Constructors

Weaving :: Functor f => e (Sem rInitial) a -> f () -> (forall x. f (Sem rInitial x) -> mAfter (f x)) -> (f a -> resultType) -> (forall x. f x -> Maybe x) -> Weaving e mAfter resultType
- 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.)

Instances1Functor

Functor (Weaving e m)Defined in polysemy-1.9.2.0 · Polysemy.Internal.Union

classclass Member (t :: Effect) (r :: EffectRow) where

Source#

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.

Instances2Member

Member t (t ': z)Defined in polysemy-1.9.2.0 · Polysemy.Internal.Union
Member t z => Member t (_1 ': z)Defined in polysemy-1.9.2.0 · Polysemy.Internal.Union

valueweave

:: (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)

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

Building Unions

valueinj :: Member e r => e (Sem rInitial) a -> Union r (Sem rInitial) a

Source#

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

valueinjUsing :: ElemOf e r -> e (Sem rInitial) a -> Union r (Sem rInitial) a

Source#

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

valueinjWeaving :: Member e r => Weaving e m a -> Union r m a

Source#

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

valueweaken :: Union r m a -> Union (e ': r) m a

Source#

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

Using Unions

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

Source#

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

valueprj :: Member e r => Union r m a -> Maybe (Weaving e m a)

Source#

Attempt to take an e effect out of a Union.

valueprjUsing :: ElemOf e r -> Union r m a -> Maybe (Weaving e m a)

Source#

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

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

Source#

Retrieve the last effect in a Union.

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

Source#

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

valuedecompCoerce

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

Source#

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

Witnesses

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

Source#

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

Source#

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

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

classclass KnownRow (r :: [k]) where

Source#

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)

Source#

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

valueextendMembershipLeft :: SList l -> ElemOf e r -> ElemOf e (Append l r)

Source#

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.

valueextendMembershipRight :: ElemOf e l -> ElemOf e (Append l r)

Source#

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.

valueinjectMembership

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

Source#

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.

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

Source#

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

valueweakenMid

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

Source#

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.