Modulepolysemy-1.9.2.0Haskell2010

Polysemy.Internal.Union

3 types
2 classes
20 values

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

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

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

4 declarations

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

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

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

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

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

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

6 declarations

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

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

Attempt to take an e effect out of a Union.

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

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

Retrieve the last effect in a Union.

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

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)

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

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

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

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

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

valueinjectMembership

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

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

valueweakenMid

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