in-other-words-0.1.0.0: A higher-order effect system where the sky's the limit

Safe HaskellNone
LanguageHaskell2010

Control.Effect.Internal.KnownList

Synopsis

Documentation

type family StripPrefix xs r where ... Source #

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

Constructors

SEnd :: SList '[] 
SCons :: SList xs -> SList (x ': xs) 

class KnownList l where Source #

Methods

singList :: SList l Source #

Instances
KnownList ([] :: [a]) Source # 
Instance details

Defined in Control.Effect.Internal.KnownList

Methods

singList :: SList [] Source #

KnownList xs => KnownList (x ': xs :: [a]) Source # 
Instance details

Defined in Control.Effect.Internal.KnownList

Methods

singList :: SList (x ': xs) Source #

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

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

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

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

weakenN :: SList l -> Union r m a -> Union (Append l r) m a Source #

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 #

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

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

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

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

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

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

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