Control.Effect.Internal.KnownList

Documentation

type family StripPrefix xs r where ...

Remove the prefix xs from the list r.

IntroC, ReinterpretC and friends don't as much introduce effects as they hide them, through removing effects from the derived effects that the transformed carrier carries. This is done thorugh StripPrefix.

For example:

   Derivs (ReinterpretSimpleC e '[newE, newE2])
 = e ': StripPrefix '[newE, newE2] (Derivs m)

Equations

StripPrefix '[] r = r

StripPrefix (x ': xs) (x ': r) = StripPrefix xs r

data SList l where

Constructors

SEnd :: SList '[]

SCons :: SList xs -> SList (x ': xs)

class KnownList l where

Methods

singList :: SList l

Instances

KnownList ([] :: [a])

Defined in Control.Effect.Internal.KnownList

Methods

singList :: SList []

KnownList xs => KnownList (x ': xs :: [a])

Defined in Control.Effect.Internal.KnownList

Methods

singList :: SList (x ': xs)

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

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

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

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

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

weakenAlgN :: SList l -> Algebra (Append l r) m -> Algebra r m

weakenAlgMid :: forall right m left mid. SList left -> SList mid -> Algebra (Append left (Append mid right)) m -> Algebra (Append left right) m

weakenReformMid :: forall right p m z a left mid. SList left -> SList mid -> Reformulation' (Append left (Append mid right)) p m z a -> Reformulation' (Append left right) p m z a

weakenReformUnder :: forall new e r p m z a. KnownList new => Reformulation' (e ': Append new r) p m z a -> Reformulation' (e ': r) p m z a

Weaken a Reformulation by removing a number of derived effects under the topmost effect.

This needs a type application to specify what effects to remove.

weakenReformUnder1 :: forall e' e r p m z a. Reformulation' (e ': (e' ': r)) p m z a -> Reformulation' (e ': r) p m z a

Weaken a Reformulation by removing a derived effect under the topmost effect.

weakenReformUnderMany :: forall top new r p m z a. (KnownList top, KnownList new) => Reformulation' (Append top (Append new r)) p m z a -> Reformulation' (Append top r) p m z a

Weaken a Reformulation by removing a number of derived effects under a number of topmost effects.

This needs a type application to specify the top effects of the stack underneath which effects are removed, and another type application to specify what effects to remove.

For example:

weakenReformUnderMany @'[Catch e] @'[Optional ((->) e)]
  :: Reformulation (Catch e ': Optional ((->) e) ': r) p m
  -> Reformulation (Catch e ': r) p m