Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type family StripPrefix xs r where ...
- data SList l where
- class KnownList l where
- 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
- weakenReformUnder1 :: forall e' e r p m z a. Reformulation' (e ': (e' ': r)) p m z a -> Reformulation' (e ': r) p m z a
- 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
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)
StripPrefix '[] r = r | |
StripPrefix (x ': xs) (x ': r) = StripPrefix xs r |
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 #
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 #
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