Data.Effect.OpenUnion

Documentation

type family (xs :: [a]) ++ (ys :: [a]) :: [a] where ... infixr 5

Equations

('[] :: [a]) ++ (ys :: [a]) = ys

(x ': xs :: [a]) ++ (ys :: [a]) = x ': (xs ++ ys)

type Reverse (es :: [a]) = Reverse_ ('[] :: [a]) es

type family ElemAt (i :: Natural) (es :: [k]) :: k where ...

Equations

ElemAt 0 (e ': _1 :: [k]) = e

ElemAt n (_1 ': es :: [k]) = ElemAt (n - 1) es

class IsSuffixOf (es :: k) (es' :: k1)

Minimal complete definition

prefixLen

Instances

IsSuffixOf (es :: k) (es :: k)

Defined in Data.Effect.OpenUnion.Internal

Methods

prefixLen :: Word

IsSuffixOf es es' => IsSuffixOf (es :: k) (e ': es' :: [a])

Defined in Data.Effect.OpenUnion.Internal

Methods

prefixLen :: Word

type WeakenN (len :: Natural) (es :: [a]) (es' :: [a]) = (es ~ Drop len es', KnownNat len)

type BundleUnder (u :: [a] -> a) (offset :: Natural) (es :: [a]) (es' :: [a]) (bundle :: [a]) = (es' ~ (Take offset es ++ (u bundle ': Drop (Length bundle) (Drop offset es))), es ~ (Take offset es' ++ (bundle ++ Drop 1 (Drop offset es'))), bundle ~ Take (PrefixLength (Drop 1 (Drop offset es')) (Drop offset es)) (Drop offset es), KnownLength bundle, KnownNat offset, Length bundle ~ PrefixLength (Drop 1 (Drop offset es')) (Drop offset es))

type family Drop (n :: Natural) (es :: [a]) :: [a] where ...

Equations

Drop 0 (es :: [a]) = es

Drop n (e ': es :: [a]) = Drop (n - 1) es

type Split (es :: [a]) (init :: [a]) (tail :: [a]) = (es ~ (init ++ tail), init ~ Take (PrefixLength tail es) es, tail ~ Drop (Length init) es, KnownLength init, Length init ~ PrefixLength tail es)

type Strengthen (es :: [a]) (es' :: [a]) = (StrengthenMap (PrefixLength es' es) es es', KnownNat (PrefixLength es' es))

type StrengthenN (len :: Natural) (es :: [k]) (es' :: [k]) = (StrengthenMap len es es', KnownNat len)

type StrengthenNUnder (len :: Natural) (offset :: Natural) (es :: [k]) (es' :: [k]) = (StrengthenMap len (Drop offset es) (Drop offset es'), KnownNat len, KnownNat offset)

type StrengthenUnder (offset :: Natural) (es :: [k]) (es' :: [k]) = StrengthenNUnder (PrefixLength es' es) offset es es'

type family Take (n :: Natural) (es :: [a]) :: [a] where ...

Equations

Take 0 (es :: [a]) = '[] :: [a]

Take n (e ': es :: [a]) = e ': Take (n - 1) es

type WeakenNUnder (len :: Natural) (offset :: Natural) (es :: [a]) (es' :: [a]) = (WeakenN len (Drop offset es) (Drop offset es'), KnownNat offset)

type WeakenUnder (offset :: Natural) (es :: [a]) (es' :: [a]) = (WeakenNUnder (PrefixLength es es') offset es es', KnownNat (PrefixLength es es'))

class KnownNat (Length es) => KnownLength (es :: [a])

Instances

KnownNat (Length es) => KnownLength (es :: [a])

Defined in Data.Effect.OpenUnion.Internal

type family Length (es :: [a]) :: Natural where ...

Equations

Length ('[] :: [a]) = 0

Length (e ': es :: [a]) = 1 + Length es

type MemberHBy (key :: k) (e :: EffectH) (es :: [EffectH]) = ((key ##> e) <<| es, LookupH key es ~ (key ##> e), IfKeyNotFound key es es)

data UnionH (es :: [EffectH]) (f :: Type -> Type) a

Open union for higher-order effects.

Instances

HFunctor (UnionH es)

Defined in Data.Effect.OpenUnion.Internal.HO

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> UnionH es f :-> UnionH es g

inj0H :: forall e (es :: [(Type -> Type) -> Type -> Type]) (f :: Type -> Type) a. e f a -> UnionH (e ': es) f a

class FindElem e es => MemberH (e :: EffectH) (es :: [EffectH]) where

Methods

injH :: forall (f :: Type -> Type) a. e f a -> UnionH es f a

prjH :: forall (f :: Type -> Type) a. HFunctor e => UnionH es f a -> Maybe (e f a)

Instances

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

Defined in Data.Effect.OpenUnion.Internal.HO

Methods

injH :: forall (f :: Type -> Type) a. e f a -> UnionH es f a

prjH :: forall (f :: Type -> Type) a. HFunctor e => UnionH es f a -> Maybe (e f a)

injNH :: forall (i :: Nat) (es :: [(Type -> Type) -> Type -> Type]) (f :: Type -> Type) a. KnownNat i => ElemAt i es f a -> UnionH es f a

type (<<|) = MemberH infix 3

extractH :: forall e (f :: Type -> Type) a. HFunctor e => UnionH '[e] f a -> e f a

hfmapUnion :: forall (f :: Type -> Type) (g :: Type -> Type) (es :: [EffectH]) a. (f ~> g) -> UnionH es f a -> UnionH es g a

nilH :: forall (f :: Type -> Type) a r. UnionH ('[] :: [EffectH]) f a -> r

weakenNH :: forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. WeakenN len es es' => UnionH es f a -> UnionH es' f a

weakensH :: forall (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. IsSuffixOf es es' => UnionH es f a -> UnionH es' f a

(!!+) :: forall e (f :: Type -> Type) a r (es :: [EffectH]). HFunctor e => (e f a -> r) -> (UnionH es f a -> r) -> UnionH (e ': es) f a -> r infixr 5

bundleAllUnionH :: forall (es :: [EffectH]) (f :: Type -> Type) a. UnionH es f a -> UnionH '[UnionH es] f a

bundleUnionH :: forall (bundle :: [EffectH]) (es :: [EffectH]) (rest :: [EffectH]) (f :: Type -> Type) a. Split es bundle rest => UnionH es f a -> UnionH (UnionH bundle ': rest) f a

bundleUnionUnderH :: forall (offset :: Natural) (bundle :: [EffectH]) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. BundleUnder UnionH offset es es' bundle => UnionH es f a -> UnionH es' f a

decompH :: forall e (es :: [(Type -> Type) -> Type -> Type]) (f :: Type -> Type) a. HFunctor e => UnionH (e ': es) f a -> Either (UnionH es f a) (e f a)

strengthenNH :: forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. StrengthenN len es es' => UnionH es f a -> UnionH es' f a

strengthenNUnderH :: forall (len :: Natural) (offset :: Natural) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. StrengthenNUnder len offset es es' => UnionH es f a -> UnionH es' f a

unbundleAllUnionH :: forall (es :: [EffectH]) (f :: Type -> Type) a. UnionH '[UnionH es] f a -> UnionH es f a

unbundleUnionH :: forall (bundle :: [EffectH]) (es :: [EffectH]) (rest :: [EffectH]) (f :: Type -> Type) a. Split es bundle rest => UnionH (UnionH bundle ': rest) f a -> UnionH es f a

unbundleUnionUnderH :: forall (offset :: Natural) (bundle :: [EffectH]) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. BundleUnder UnionH offset es es' bundle => UnionH es' f a -> UnionH es f a

weakenH :: forall (any :: EffectH) (es :: [EffectH]) (f :: Type -> Type) a. UnionH es f a -> UnionH (any ': es) f a

weakenNUnderH :: forall (len :: Natural) (offset :: Natural) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. WeakenNUnder len offset es es' => UnionH es f a -> UnionH es' f a

weakenUnderH :: forall (any :: EffectH) (e :: EffectH) (es :: [EffectH]) (f :: Type -> Type) a. UnionH (e ': es) f a -> UnionH (e ': (any ': es)) f a

type family LookupH (key :: k) (r :: [(Type -> Type) -> Type -> Type]) :: EffectH where ...

Equations

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

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

decomp0H :: forall e (f :: Type -> Type) a. HFunctor e => UnionH '[e] f a -> Either (UnionH ('[] :: [EffectH]) f a) (e f a)

flipAllUnionH :: forall (es :: [EffectH]) (f :: Type -> Type) a. KnownLength es => UnionH es f a -> UnionH (Reverse es) f a

flipUnionH :: forall (len :: Nat) (es :: [EffectH]) (f :: Type -> Type) a. KnownNat len => UnionH es f a -> UnionH (Reverse (Take len es) ++ Drop len es) f a

flipUnionUnderH :: forall (len :: Nat) (offset :: Nat) (es :: [EffectH]) (f :: Type -> Type) a. (KnownNat len, KnownNat offset) => UnionH es f a -> UnionH (Take offset es ++ (Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es))) f a

prefixUnionH :: forall (any :: [EffectH]) (es :: [EffectH]) (f :: Type -> Type) a. KnownLength any => UnionH es f a -> UnionH (any ++ es) f a

prefixUnionUnderH :: forall (any :: [EffectH]) (offset :: Nat) (es :: [EffectH]) (f :: Type -> Type) a. (KnownLength any, KnownNat offset) => UnionH es f a -> UnionH (Take offset es ++ (any ++ Drop offset es)) f a

prjNH :: forall (i :: Nat) (es :: [(Type -> Type) -> Type -> Type]) (f :: Type -> Type) a. (KnownNat i, HFunctor (ElemAt i es)) => UnionH es f a -> Maybe (ElemAt i es f a)

suffixUnionH :: forall (any :: [EffectH]) (es :: [EffectH]) (f :: Type -> Type) a. UnionH es f a -> UnionH (es ++ any) f a

suffixUnionOverNH :: forall (any :: [EffectH]) (offset :: Nat) (es :: [EffectH]) (f :: Type -> Type) a. (KnownLength any, KnownNat offset, KnownLength es) => UnionH es f a -> UnionH (Take (Length es - offset) es ++ (any ++ Drop (Length es - offset) es)) f a

weakensUnderH :: forall (offset :: Natural) (es :: [EffectH]) (es' :: [EffectH]) (f :: Type -> Type) a. WeakenUnder offset es es' => UnionH es f a -> UnionH es' f a

type (<|) = Member infix 3

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)

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)

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)

data Union (es :: [EffectF]) a

Open union for first-order effects.

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

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

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

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

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

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

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

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

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

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

strengthenN :: forall (len :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. StrengthenN len 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

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

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

unbundleUnion :: forall (es :: [EffectF]) (bundle :: [EffectF]) (rest :: [EffectF]) a. Split es bundle rest => Union (Union bundle ': rest) a -> Union 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

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)

weakenNUnder :: forall (len :: Natural) (offset :: Natural) (es :: [EffectF]) (es' :: [EffectF]) a. WeakenNUnder len offset 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

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

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

Specialized version of decomp for efficiency.

O(1)

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

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

prjN :: forall (i :: Nat) (es :: [EffectF]) a. KnownNat i => Union es a -> Maybe (ElemAt i 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

type (+) = (:+:) :: (Type -> Type) -> (Type -> Type) -> Type -> Type infixr 5

Sum for first-order effects.

type family SumToRecUnionList (u :: [k] -> k) (e :: k) :: [k] where ...

Equations

SumToRecUnionList Union Nop = '[] :: [EffectF]

SumToRecUnionList Union (e + r :: EffectF) = e ': SumToRecUnionList Union r

SumToRecUnionList Union (e :: EffectF) = '[e]

SumToRecUnionList UnionH LNop = '[] :: [EffectH]

SumToRecUnionList UnionH (e :+: r :: EffectH) = e ': SumToRecUnionList UnionH r

SumToRecUnionList UnionH (e :: EffectH) = '[e]

type SumToRecUnion (u :: [k] -> k) (e :: k) = u (SumToRecUnionList u e)

type U (u :: [k] -> k) (e :: k) = SumToRecUnion u e

type UL (u :: [k] -> k) (e :: k) = SumToRecUnionList u e