Safe Haskell	Safe-Inferred
Language	Haskell2010

Polysemy.Internal.Union

Contents

Building Unions
Using Unions
Witnesses
Checking membership

Description

Synopsis

data Union (r :: EffectRow) (mWoven :: Type -> Type) a where
- Union :: ElemOf e r -> Weaving e m a -> Union r m a
data Weaving e mAfter resultType where
- Weaving :: forall f e rInitial a resultType mAfter. Functor f => {..} -> Weaving e mAfter resultType
class Member (t :: Effect) (r :: EffectRow)
inj :: forall e r rInitial a. Member e r => e (Sem rInitial) a -> Union r (Sem rInitial) a
injUsing :: forall e r rInitial a. ElemOf e r -> e (Sem rInitial) a -> Union r (Sem rInitial) a
injWeaving :: forall e r m a. Member e r => Weaving e m a -> Union r m a
weaken :: forall e r m a. Union r m a -> Union (e ': r) m a
decomp :: Union (e ': r) m a -> Either (Union r m a) (Weaving e m a)
prj :: forall e r m a. Member e r => Union r m a -> Maybe (Weaving e m a)
prjUsing :: forall e r m a. ElemOf e r -> Union r m a -> Maybe (Weaving e m a)
extract :: Union '[e] m a -> Weaving e m a
absurdU :: Union '[] m a -> b
decompCoerce :: Union (e ': r) m a -> Either (Union (f ': r) m a) (Weaving e m a)
data ElemOf (e :: k) (r :: [k]) where
- 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
sameMember :: forall e e' r. ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
class KnownRow r
tryMembership :: forall e r. (Typeable e, KnownRow r) => Maybe (ElemOf e r)
extendMembershipLeft :: forall l r e. SList l -> ElemOf e r -> ElemOf e (Append l r)
extendMembershipRight :: forall l r e. ElemOf e l -> ElemOf e (Append l r)
injectMembership :: forall right e left mid. SList left -> SList mid -> ElemOf e (Append left right) -> ElemOf e (Append left (Append mid right))
weakenList :: SList l -> Union r m a -> Union (Append l r) m a
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

Documentation

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

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

Instances details

Functor (Union r mWoven) Source #
Instance details 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 Source #

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

Instances details

Functor (Weaving e m) Source #
Instance details 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) 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.

Minimal complete definition

membership'

Instances

Instances details

Member t z => Member t (_1 ': z) Source #
Instance details Defined in Polysemy.Internal.Union Methods membership' :: ElemOf t (_1 ': z)
Member t (t ': z) Source #
Instance details 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 Source #

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 Source #

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 Source #

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 Source #

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) Source #

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) Source #

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) Source #

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 Source #

Retrieve the last effect in a Union.

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

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) Source #

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

Witnesses

data ElemOf (e :: k) (r :: [k]) where 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.

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 Source #

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') 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

class KnownRow r 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])

Minimal complete definition

tryMembership'

Instances

Instances details

KnownRow ('[] :: [k]) Source #
Instance details Defined in Polysemy.Internal.Union Methods tryMembership' :: forall (e :: k0). Typeable e => Maybe (ElemOf e '[])
(Typeable e, KnownRow r) => KnownRow (e ': r :: [k]) Source #
Instance details 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) Source #

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

extendMembershipRight :: forall l r e. 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.

injectMembership :: forall right e left mid. 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.

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

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