Data.Effect.OpenUnion.Internal.FO

Implementation of an open union for first-order effects.

Importing this module allows unsafe access to the data structure of the open union, so it should not usually be imported directly.

Based on the open union in freer-simple.

Documentation

data Union (es :: [EffectF]) a where

Open union for first-order effects.

Constructors

Union

Fields

• :: forall (e :: Type -> Type) a (es :: [EffectF]). !Word

  A natural number tag to identify the element of the union.

• -> e a

  The data of the higher-order effect that is an element of the union.

• -> Union es a

unsafeInj :: forall e a (es :: [EffectF]). Word -> e a -> Union es a

Takes a request of type e :: EffectF, and injects it into the Union.

Summand is assigning a specified Word value, which is a position in the type-list (e ': es) :: EffectF.

This function is unsafe.

O(1)

unsafePrj :: forall (es :: [EffectF]) a e. Word -> Union es a -> Maybe (e a)

Project a value of type Union (e ': es) :: EffectF into a possible summand of the type e :: EffectF. Nothing means that e :: EffectF is not the value stored in the Union (e ': es) :: EffectF.

It is assumed that summand is stored in the Union when the Word value is the same value as is stored in the Union.

This function is unsafe.

O(1)

class FindElem e es => Member (e :: EffectF) (es :: [EffectF]) where

A constraint that requires that a particular effect, e, is a member of the type-level list es. This is used to parameterize an Eff computation over an arbitrary list of first-order effects, so long as e is somewhere in the list.

For example, a computation that only needs access to a cell of mutable state containing an Integer would likely use the following type:

State Integer <| ef => Eff eh ef ()

Methods

inj :: e a -> Union es a

Takes a request of type e :: EffectF, and injects it into the Union.

O(1)

prj :: Union es a -> Maybe (e a)

Project a value of type Union (e ': es) :: EffectF into a possible summand of the type e :: EffectF. Nothing means that e :: EffectF is not the value stored in the Union (e ': es) :: EffectF.

O(1)

Instances

(FindElem e es, IfNotFound e es es) => Member e es

Defined in Data.Effect.OpenUnion.Internal.FO

Methods

inj :: e a -> Union es a

prj :: Union es a -> Maybe (e a)

type (<|) = Member infix 3

type MemberBy (key :: k) (e :: EffectF) (es :: [EffectF]) = ((key #> e) <| es, Lookup key es ~ (key #> e), IfKeyNotFound key es es)

type family Lookup (key :: k) (r :: [Type -> Type]) :: EffectF where ...

Equations

Lookup (key :: k) ((key #> e) ': _1) = key #> e

Lookup (key :: k) (_1 ': r) = Lookup key r

decomp :: forall e (es :: [EffectF]) a. Union (e ': es) a -> Either (Union es a) (e a)

Orthogonal decomposition of a Union (e ': es) :: EffectF. Right value is returned if the Union (e ': es) :: EffectF contains e :: EffectF, and Left when it doesn't. Notice that Left value contains Union es :: EffectF, i.e. it can not contain e :: EffectF.

O(1)

decomp0 :: Union '[e] a -> Either (Union ('[] :: [EffectF]) a) (e a)

Specialized version of decomp for efficiency.

O(1)

(!+) :: forall e a r (es :: [EffectF]). (e a -> r) -> (Union es a -> r) -> Union (e ': es) a -> r infixr 5

extract :: Union '[e] a -> e a

Specialised version of prj/decomp that works on an Union '[e] :: EffectF which contains only one specific summand. Hence the absence of Maybe, and Either.

O(1)

inj0 :: forall e (es :: [Type -> Type]) a. e a -> Union (e ': es) a

injN :: forall (i :: Nat) (es :: [Type -> Type]) a. KnownNat i => ElemAt i es a -> Union es a

prjN :: forall (i :: Nat) (es :: [EffectF]) a. KnownNat i => Union es a -> Maybe (ElemAt i es a)

weaken :: forall (any :: EffectF) (es :: [EffectF]) a. Union es a -> Union (any ': es) a

Inject whole Union es into a weaker Union (any ': es) that has one more summand.

O(1)

weakens :: forall (es :: [EffectF]) (es' :: [EffectF]) a. IsSuffixOf es es' => Union es a -> Union es' a

weakenN :: forall (len :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. WeakenN len es es' => Union es a -> Union es' a

weakenUnder :: forall (any :: EffectF) (e :: EffectF) (es :: [EffectF]) a. Union (e ': es) a -> Union (e ': (any ': es)) a

weakensUnder :: forall (offset :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. WeakenUnder offset es es' => Union es a -> Union es' a

weakenNUnder :: forall (len :: Natural) (offset :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. WeakenNUnder len offset es es' => Union es a -> Union es' a

strengthen :: forall (e :: EffectF) (es :: [EffectF]) a. e <| es => Union (e ': es) a -> Union es a

strengthens :: forall (es :: [EffectF]) (es' :: [EffectF]) a. Strengthen es es' => Union es a -> Union es' a

strengthenN :: forall (len :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. StrengthenN len es es' => Union es a -> Union es' a

strengthenUnder :: forall (e2 :: EffectF) (e1 :: EffectF) (es :: [EffectF]) a. e2 <| es => Union (e1 ': (e2 ': es)) a -> Union (e1 ': es) a

strengthensUnder :: forall (offset :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. StrengthenUnder offset es es' => Union es a -> Union es' a

strengthenNUnder :: forall (len :: Natural) (offset :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. StrengthenNUnder len offset es es' => Union es a -> Union es' a

bundleUnion :: forall (es :: [EffectF]) (bundle :: [EffectF]) (rest :: [EffectF]) a. Split es bundle rest => Union es a -> Union (Union bundle ': rest) a

bundleUnionN :: forall (len :: Nat) (es :: [EffectF]) a. KnownNat len => Union es a -> Union (Union (Take len es) ': Drop len es) a

unbundleUnion :: forall (es :: [EffectF]) (bundle :: [EffectF]) (rest :: [EffectF]) a. Split es bundle rest => Union (Union bundle ': rest) a -> Union es a

unbundleUnionN :: forall (len :: Nat) (es :: [EffectF]) a. KnownNat len => Union (Union (Take len es) ': Drop len es) a -> Union es a

bundleUnionUnder :: forall (offset :: Natural) (bundle :: [EffectF]) (es :: [EffectF]) (es' :: [EffectF]) a. BundleUnder Union offset es es' bundle => Union es a -> Union es' a

bundleUnionNUnder :: forall (len :: Nat) (offset :: Nat) (es :: [EffectF]) a. (KnownNat len, KnownNat offset) => Union es a -> Union (Take offset es ++ (Union (Take len (Drop offset es)) ': Drop len (Drop offset es))) a

unbundleUnionUnder :: forall (offset :: Natural) (bundle :: [EffectF]) (es :: [EffectF]) (es' :: [EffectF]) a. BundleUnder Union offset es es' bundle => Union es' a -> Union es a

unbundleUnionNUnder :: forall (len :: Nat) (offset :: Nat) (es :: [EffectF]) a. (KnownNat len, KnownNat offset) => Union (Take offset es ++ (Union (Take len (Drop offset es)) ': Drop len (Drop offset es))) a -> Union es a

bundleAllUnion :: forall (es :: [EffectF]) a. Union es a -> Union '[Union es] a

unbundleAllUnion :: forall (es :: [EffectF]) a. Union '[Union es] a -> Union es a

prefixUnion :: forall (any :: [EffectF]) (es :: [EffectF]) a. KnownLength any => Union es a -> Union (any ++ es) a

prefixUnionUnder :: forall (any :: [EffectF]) (offset :: Nat) (es :: [EffectF]) a. (KnownLength any, KnownNat offset) => Union es a -> Union (Take offset es ++ (any ++ Drop offset es)) a

suffixUnion :: forall (any :: [EffectF]) (es :: [EffectF]) a. Union es a -> Union (es ++ any) a

suffixUnionOverN :: forall (any :: [EffectF]) (offset :: Nat) (es :: [EffectF]) a. (KnownLength any, KnownNat offset, KnownLength es) => Union es a -> Union (Take (Length es - offset) es ++ (any ++ Drop (Length es - offset) es)) a

flipAllUnion :: forall (es :: [EffectF]) a. KnownLength es => Union es a -> Union (Reverse es) a

flipUnion :: forall (len :: Nat) (es :: [EffectF]) a. KnownNat len => Union es a -> Union (Reverse (Take len es) ++ Drop len es) a

flipUnionUnder :: forall (len :: Nat) (offset :: Nat) (es :: [EffectF]) a. (KnownNat len, KnownNat offset) => Union es a -> Union (Take offset es ++ (Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es))) a

nil :: Union ('[] :: [EffectF]) a -> r