Data.Hefty.Union

A type class representing a general open union for higher-order effects, independent of the internal implementation.

Documentation

class Union (u :: [SigClass] -> SigClass) where

A type class representing a general open union for higher-order effects, independent of the internal implementation.

Minimal complete definition

inject, project, exhaust, (comp | inject0, weaken, decomp | (|+:))

Associated Types

type HasMembership u (e :: SigClass) (es :: [SigClass]) :: Constraint

Methods

inject :: HasMembership u e es => e f ~> u es f

project :: HasMembership u e es => u es f a -> Maybe (e f a)

exhaust :: u '[] f a -> x

comp :: Either (e f a) (u es f a) -> u (e ': es) f a

decomp :: u (e ': es) f a -> (e :+: u es) f a

(|+:) :: (e f a -> r) -> (u es f a -> r) -> u (e ': es) f a -> r infixr 5

inject0 :: e f ~> u (e ': es) f

injectUnder :: h2 f ~> u (h1 ': (h2 ': es)) f

injectUnder2 :: h3 f ~> u (h1 ': (h2 ': (h3 ': es))) f

injectUnder3 :: h4 f ~> u (h1 ': (h2 ': (h3 ': (h4 ': es)))) f

weaken :: u es f ~> u (e ': es) f

weaken2 :: u es f ~> u (e1 ': (e2 ': es)) f

weaken3 :: u es f ~> u (e1 ': (e2 ': (e3 ': es))) f

weaken4 :: u es f ~> u (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

weakenUnder :: u (e1 ': es) f ~> u (e1 ': (e2 ': es)) f

weakenUnder2 :: u (e1 ': (e2 ': es)) f ~> u (e1 ': (e2 ': (e3 ': es))) f

weakenUnder3 :: u (e1 ': (e2 ': (e3 ': es))) f ~> u (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

weaken2Under :: u (e1 ': es) f ~> u (e1 ': (e2 ': (e3 ': es))) f

weaken2Under2 :: u (e1 ': (e2 ': es)) f ~> u (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

weaken3Under :: u (e1 ': es) f ~> u (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

flipUnion :: u (e1 ': (e2 ': es)) f ~> u (e2 ': (e1 ': es)) f

flipUnion3 :: u (e1 ': (e2 ': (e3 ': es))) f ~> u (e3 ': (e2 ': (e1 ': es))) f

flipUnionUnder :: u (e1 ': (e2 ': (e3 ': es))) f ~> u (e1 ': (e3 ': (e2 ': es))) f

rot3 :: u (e1 ': (e2 ': (e3 ': es))) f ~> u (e2 ': (e3 ': (e1 ': es))) f

rot3' :: u (e1 ': (e2 ': (e3 ': es))) f ~> u (e3 ': (e1 ': (e2 ': es))) f

bundleUnion2 :: u (e1 ': (e2 ': es)) f ~> u (u '[e1, e2] ': es) f

bundleUnion3 :: u (e1 ': (e2 ': (e3 ': es))) f ~> u (u '[e1, e2, e3] ': es) f

bundleUnion4 :: u (e1 ': (e2 ': (e3 ': (e4 ': es)))) f ~> u (u '[e1, e2, e3, e4] ': es) f

unbundleUnion2 :: u (u '[e1, e2] ': es) f ~> u (e1 ': (e2 ': es)) f

unbundleUnion3 :: u (u '[e1, e2, e3] ': es) f ~> u (e1 ': (e2 ': (e3 ': es))) f

unbundleUnion4 :: u (u '[e1, e2, e3, e4] ': es) f ~> u (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

Instances

Union ExtensibleUnion

Defined in Data.Hefty.Extensible

Associated Types

type HasMembership ExtensibleUnion e es

Methods

inject :: forall (e :: SigClass) (es :: [SigClass]) (f :: Type -> Type). HasMembership ExtensibleUnion e es => e f ~> ExtensibleUnion es f

project :: forall e (es :: [SigClass]) (f :: Type -> Type) a. HasMembership ExtensibleUnion e es => ExtensibleUnion es f a -> Maybe (e f a)

exhaust :: forall (f :: Type -> Type) a x. ExtensibleUnion '[] f a -> x

comp :: forall e (f :: Type -> Type) a (es :: [SigClass]). Either (e f a) (ExtensibleUnion es f a) -> ExtensibleUnion (e ': es) f a

decomp :: forall (e :: SigClass) (es :: [SigClass]) (f :: Type -> Type) a. ExtensibleUnion (e ': es) f a -> (e :+: ExtensibleUnion es) f a

(|+:) :: forall e (f :: Type -> Type) a r (es :: [SigClass]). (e f a -> r) -> (ExtensibleUnion es f a -> r) -> ExtensibleUnion (e ': es) f a -> r

inject0 :: forall (e :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) (es :: [(Type -> Type) -> Type -> Type]). e f ~> ExtensibleUnion (e ': es) f

injectUnder :: forall (h2 :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) (h1 :: (Type -> Type) -> Type -> Type) (es :: [(Type -> Type) -> Type -> Type]). h2 f ~> ExtensibleUnion (h1 ': (h2 ': es)) f

injectUnder2 :: forall (h3 :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) (h1 :: (Type -> Type) -> Type -> Type) (h2 :: (Type -> Type) -> Type -> Type) (es :: [(Type -> Type) -> Type -> Type]). h3 f ~> ExtensibleUnion (h1 ': (h2 ': (h3 ': es))) f

injectUnder3 :: forall (h4 :: (Type -> Type) -> Type -> Type) (f :: Type -> Type) (h1 :: (Type -> Type) -> Type -> Type) (h2 :: (Type -> Type) -> Type -> Type) (h3 :: (Type -> Type) -> Type -> Type) (es :: [(Type -> Type) -> Type -> Type]). h4 f ~> ExtensibleUnion (h1 ': (h2 ': (h3 ': (h4 ': es)))) f

weaken :: forall (es :: [SigClass]) (f :: Type -> Type) (e :: SigClass). ExtensibleUnion es f ~> ExtensibleUnion (e ': es) f

weaken2 :: forall (es :: [SigClass]) (f :: Type -> Type) (e1 :: SigClass) (e2 :: SigClass). ExtensibleUnion es f ~> ExtensibleUnion (e1 ': (e2 ': es)) f

weaken3 :: forall (es :: [SigClass]) (f :: Type -> Type) (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass). ExtensibleUnion es f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f

weaken4 :: forall (es :: [SigClass]) (f :: Type -> Type) (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (e4 :: SigClass). ExtensibleUnion es f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

weakenUnder :: forall (e1 :: SigClass) (es :: [SigClass]) (f :: Type -> Type) (e2 :: SigClass). ExtensibleUnion (e1 ': es) f ~> ExtensibleUnion (e1 ': (e2 ': es)) f

weakenUnder2 :: forall (e1 :: SigClass) (e2 :: SigClass) (es :: [SigClass]) (f :: Type -> Type) (e3 :: SigClass). ExtensibleUnion (e1 ': (e2 ': es)) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f

weakenUnder3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type) (e4 :: SigClass). ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

weaken2Under :: forall (e1 :: SigClass) (es :: [SigClass]) (f :: Type -> Type) (e2 :: SigClass) (e3 :: SigClass). ExtensibleUnion (e1 ': es) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f

weaken2Under2 :: forall (e1 :: SigClass) (e2 :: SigClass) (es :: [SigClass]) (f :: Type -> Type) (e3 :: SigClass) (e4 :: SigClass). ExtensibleUnion (e1 ': (e2 ': es)) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

weaken3Under :: forall (e1 :: SigClass) (es :: [SigClass]) (f :: Type -> Type) (e2 :: SigClass) (e3 :: SigClass) (e4 :: SigClass). ExtensibleUnion (e1 ': es) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

flipUnion :: forall (e1 :: SigClass) (e2 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': es)) f ~> ExtensibleUnion (e2 ': (e1 ': es)) f

flipUnion3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f ~> ExtensibleUnion (e3 ': (e2 ': (e1 ': es))) f

flipUnionUnder :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f ~> ExtensibleUnion (e1 ': (e3 ': (e2 ': es))) f

rot3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f ~> ExtensibleUnion (e2 ': (e3 ': (e1 ': es))) f

rot3' :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f ~> ExtensibleUnion (e3 ': (e1 ': (e2 ': es))) f

bundleUnion2 :: forall (e1 :: SigClass) (e2 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': es)) f ~> ExtensibleUnion (ExtensibleUnion '[e1, e2] ': es) f

bundleUnion3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f ~> ExtensibleUnion (ExtensibleUnion '[e1, e2, e3] ': es) f

bundleUnion4 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (e4 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (e1 ': (e2 ': (e3 ': (e4 ': es)))) f ~> ExtensibleUnion (ExtensibleUnion '[e1, e2, e3, e4] ': es) f

unbundleUnion2 :: forall (e1 :: SigClass) (e2 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (ExtensibleUnion '[e1, e2] ': es) f ~> ExtensibleUnion (e1 ': (e2 ': es)) f

unbundleUnion3 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (ExtensibleUnion '[e1, e2, e3] ': es) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': es))) f

unbundleUnion4 :: forall (e1 :: SigClass) (e2 :: SigClass) (e3 :: SigClass) (e4 :: SigClass) (es :: [SigClass]) (f :: Type -> Type). ExtensibleUnion (ExtensibleUnion '[e1, e2, e3, e4] ': es) f ~> ExtensibleUnion (e1 ': (e2 ': (e3 ': (e4 ': es)))) f

type HFunctorUnion u = HFunctorUnion_ (ForallHFunctor u) u

class (Union u, forall e es. (HFunctor e, forallHFunctor es) => forallHFunctor (e ': es), forall es. forallHFunctor es => HFunctor (u es), forallHFunctor ~ ForallHFunctor u, forallHFunctor '[]) => HFunctorUnion_ forallHFunctor u | u -> forallHFunctor

Associated Types

type ForallHFunctor u :: [SigClass] -> Constraint

Instances

HFunctorUnion_ (Forall HFunctor) ExtensibleUnion

Defined in Data.Hefty.Extensible

Associated Types

type ForallHFunctor ExtensibleUnion :: [SigClass] -> Constraint

data FoundLevel

Constructors

CurrentLevel

LowerLevel

Instances

SingKind FoundLevel

Defined in Data.Hefty.Union

Associated Types

type Demote FoundLevel = (r :: Type)

Methods

fromSing :: forall (a :: FoundLevel). Sing a -> Demote FoundLevel

toSing :: Demote FoundLevel -> SomeSing FoundLevel

SingI 'CurrentLevel

Defined in Data.Hefty.Union

Methods

sing :: Sing 'CurrentLevel

SingI 'LowerLevel

Defined in Data.Hefty.Union

Methods

sing :: Sing 'LowerLevel

SingI1 'FoundIn

Defined in Data.Hefty.Union

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('FoundIn x)

SingI FoundInSym0

Defined in Data.Hefty.Union

Methods

sing :: Sing FoundInSym0

SuppressUnusedWarnings FoundInSym0

Defined in Data.Hefty.Union

Methods

suppressUnusedWarnings :: ()

type Demote FoundLevel

Defined in Data.Hefty.Union

type Demote FoundLevel = FoundLevel

type Sing

Defined in Data.Hefty.Union

type Sing = SFoundLevel

type Apply FoundInSym0 (a6989586621679104905 :: FoundLevel)

Defined in Data.Hefty.Union

type Apply FoundInSym0 (a6989586621679104905 :: FoundLevel) = 'FoundIn a6989586621679104905

data SearchResult

Constructors

FoundIn FoundLevel

NotFound

Instances

SingKind SearchResult

Defined in Data.Hefty.Union

Associated Types

type Demote SearchResult = (r :: Type)

Methods

fromSing :: forall (a :: SearchResult). Sing a -> Demote SearchResult

toSing :: Demote SearchResult -> SomeSing SearchResult

SingI 'NotFound

Defined in Data.Hefty.Union

Methods

sing :: Sing 'NotFound

SingI1 'FoundIn

Defined in Data.Hefty.Union

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('FoundIn x)

SingI n => SingI ('FoundIn n :: SearchResult)

Defined in Data.Hefty.Union

Methods

sing :: Sing ('FoundIn n)

SingI FoundInSym0

Defined in Data.Hefty.Union

Methods

sing :: Sing FoundInSym0

SuppressUnusedWarnings FoundInSym0

Defined in Data.Hefty.Union

Methods

suppressUnusedWarnings :: ()

type Demote SearchResult

Defined in Data.Hefty.Union

type Demote SearchResult = SearchResult

type Sing

Defined in Data.Hefty.Union

type Sing = SSearchResult

type Apply FoundInSym0 (a6989586621679104905 :: FoundLevel)

Defined in Data.Hefty.Union

type Apply FoundInSym0 (a6989586621679104905 :: FoundLevel) = 'FoundIn a6989586621679104905

type family FoundInSym1 (a6989586621679104905 :: FoundLevel) :: SearchResult where ...

Equations

FoundInSym1 a6989586621679104905 = FoundIn a6989586621679104905

data FoundInSym0 :: (~>) FoundLevel SearchResult where

Constructors

FoundInSym0KindInference :: SameKind (Apply FoundInSym0 arg) (FoundInSym1 arg) => FoundInSym0 a6989586621679104905

Instances

SingI FoundInSym0

Defined in Data.Hefty.Union

Methods

sing :: Sing FoundInSym0

SuppressUnusedWarnings FoundInSym0

Defined in Data.Hefty.Union

Methods

suppressUnusedWarnings :: ()

type Apply FoundInSym0 (a6989586621679104905 :: FoundLevel)

Defined in Data.Hefty.Union

type Apply FoundInSym0 (a6989586621679104905 :: FoundLevel) = 'FoundIn a6989586621679104905

type family NotFoundSym0 :: SearchResult where ...

Equations

NotFoundSym0 = NotFound

type family CurrentLevelSym0 :: FoundLevel where ...

Equations

CurrentLevelSym0 = CurrentLevel

type family LowerLevelSym0 :: FoundLevel where ...

Equations

LowerLevelSym0 = LowerLevel

data SSearchResult :: SearchResult -> Type where

Constructors

SFoundIn :: forall (n :: FoundLevel). (Sing n) -> SSearchResult (FoundIn n :: SearchResult)

SNotFound :: SSearchResult (NotFound :: SearchResult)

data SFoundLevel :: FoundLevel -> Type where

Constructors

SCurrentLevel :: SFoundLevel (CurrentLevel :: FoundLevel)

SLowerLevel :: SFoundLevel (LowerLevel :: FoundLevel)

type family FoundLevelOf found :: FoundLevel where ...

Equations

FoundLevelOf ('FoundIn l) = l

type MemberH u e ehs = HasMembershipRec u e ehs

type Member u e efs = MemberH u (LiftIns e) efs

class MemberRec (u :: [SigClass] -> SigClass) e es where

Methods

injectRec :: e f ~> u es f

projectRec :: u es f a -> Maybe (e f a)

Instances

(SearchMemberRec es u e es, MemberFound e es (CurrentLevelSearchResult searchResult), searchResult ~ Search u es e, SingI (HeadLowerSearchResult searchResult), found ~ CurrentLevelSearchResult searchResult) => MemberRec u e es

Defined in Data.Hefty.Union

Methods

injectRec :: forall (f :: Type -> Type). e f ~> u es f

projectRec :: forall (f :: Type -> Type) a. u es f a -> Maybe (e f a)

type HasMembershipRec u e es = (SearchMemberRec es u e es, HasMembershipRec1_ u e es (Search u es e))

type HasMembershipRec1_ u e es searchResult = (HasMembershipRec2_ u e es (CurrentLevelSearchResult searchResult), SingI (HeadLowerSearchResult searchResult))

type HasMembershipRec2_ u e es found = HasMembershipRec3_ u e es found (FoundLevelOf found)

type HasMembershipRec3_ u e es found lvl = (found ~ 'FoundIn lvl, SingI lvl, HasMembershipWhenCurrentLevel lvl u e es, SearchMemberRecWhenLowerLevel lvl es u e)

class MemberFound e es found where

Methods

withFound :: (forall lvl. (found ~ 'FoundIn lvl, SingI lvl) => a) -> a

Instances

(TypeError ((('Text "The effect class: " :<>: 'ShowType e) :$$: 'Text " was not found in the union:") :$$: ('Text " " :<>: 'ShowType es)) :: Constraint) => MemberFound (e :: k1) (es :: k2) 'NotFound

Defined in Data.Hefty.Union

Methods

withFound :: (forall (lvl :: FoundLevel). ('NotFound ~ 'FoundIn lvl, SingI lvl) => a) -> a

SingI lvl => MemberFound (e :: k1) (es :: k2) ('FoundIn lvl)

Defined in Data.Hefty.Union

Methods

withFound :: (forall (lvl0 :: FoundLevel). ('FoundIn lvl ~ 'FoundIn lvl0, SingI lvl0) => a) -> a

type SearchMemberRec rest u e = SearchMemberRec_ (NextSearchMemberRecAction rest u e) rest u e

class SearchMemberRec_ (act :: SearchMemberRecAction) (rest :: [SigClass]) (u :: [SigClass] -> SigClass) (e :: SigClass) (es :: [SigClass]) where

Associated Types

type Search_ act u rest e :: SearchResults

Methods

injectSMR_ :: searchResult ~ Search_ act u rest e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> e f ~> u es f

projectSMR_ :: searchResult ~ Search_ act u rest e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> u es f a -> Maybe (e f a)

Instances

SearchMemberRec_ act ('[] :: [SigClass]) u e es

Defined in Data.Hefty.Union

Associated Types

type Search_ act u '[] e :: SearchResults

Methods

injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type). searchResult ~ Search_ act u '[] e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> e f ~> u es f

projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type) a. searchResult ~ Search_ act u '[] e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> u es f a -> Maybe (e f a)

(SearchMemberRec es' u e es', headSearchResults ~ Search u es' e, tailSearchResults ~ Search u tail e, isFoundInHead ~ IsFound (CurrentLevelSearchResult headSearchResults), If isFoundInHead (HasMembership u (u es') es) (), SearchMemberRec (If isFoundInHead ('[] :: [SigClass]) tail) u e es, Union u, SingI (HeadLowerSearchResult headSearchResults), SingI (HeadLowerSearchResult tailSearchResults)) => SearchMemberRec_ 'SmrDown (u es' ': tail) u e es

Defined in Data.Hefty.Union

Associated Types

type Search_ 'SmrDown u (u es' ': tail) e :: SearchResults

Methods

injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type). searchResult ~ Search_ 'SmrDown u (u es' ': tail) e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> e f ~> u es f

projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type) a. searchResult ~ Search_ 'SmrDown u (u es' ': tail) e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> u es f a -> Maybe (e f a)

(HasMembership u e es, Union u) => SearchMemberRec_ 'SmrStop (e ': _tail) u e es

Defined in Data.Hefty.Union

Associated Types

type Search_ 'SmrStop u (e ': _tail) e :: SearchResults

Methods

injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type). searchResult ~ Search_ 'SmrStop u (e ': _tail) e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> e f ~> u es f

projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type) a. searchResult ~ Search_ 'SmrStop u (e ': _tail) e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> u es f a -> Maybe (e f a)

(HasMembershipWhenCurrentLevel lvl u e (_e ': rest), SearchMemberRecWhenLowerLevel lvl rest u e, SingI (HeadLowerSearchResult searchResult), Union u, searchResult ~ Search u rest e, lvl ~ FoundLevelOf (CurrentLevelSearchResult searchResult)) => SearchMemberRec_ 'SmrRight (_e ': rest) u e (_e ': rest)

Defined in Data.Hefty.Union

Associated Types

type Search_ 'SmrRight u (_e ': rest) e :: SearchResults

Methods

injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type). searchResult ~ Search_ 'SmrRight u (_e ': rest) e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> e f ~> u (_e ': rest) f

projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: Type -> Type) a. searchResult ~ Search_ 'SmrRight u (_e ': rest) e => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> u (_e ': rest) f a -> Maybe (e f a)

type Search u rest e = Search_ (NextSearchMemberRecAction rest u e) u rest e

injectSMR :: forall rest u e es searchResult lvl f. (SearchMemberRec rest u e es, searchResult ~ Search u rest e) => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> e f ~> u es f

projectSMR :: forall rest u e es searchResult lvl f a. (SearchMemberRec rest u e es, searchResult ~ Search u rest e) => (CurrentLevelSearchResult searchResult :~: 'FoundIn lvl) -> SSearchResult ('FoundIn lvl) -> SSearchResult (HeadLowerSearchResult searchResult) -> u es f a -> Maybe (e f a)

data SearchResults

Constructors

SearchResults SearchResult SearchResult

type family CurrentLevelSearchResult a where ...

Equations

CurrentLevelSearchResult ('SearchResults a _) = a

type family HeadLowerSearchResult a where ...

Equations

HeadLowerSearchResult ('SearchResults _ a) = a

data SearchMemberRecAction

Constructors

SmrStop

SmrRight

SmrDown

type family NextSearchMemberRecAction rest (u :: [SigClass] -> SigClass) e where ...

Equations

NextSearchMemberRecAction (e ': _) u e = 'SmrStop

NextSearchMemberRecAction (u _ ': _) u e = 'SmrDown

NextSearchMemberRecAction _ _ _ = 'SmrRight

type family IsFound found where ...

Equations

IsFound ('FoundIn _) = 'True

IsFound 'NotFound = 'False

type SearchResultsOnSmrDown u es' tail e foundInHead foundInTail = 'SearchResults (If (IsFound foundInHead) ('FoundIn 'LowerLevel) foundInTail) foundInHead

type HasMembershipWhenCurrentLevel lvl u e es = HasMembershipWhenCurrentLevel_ (HasMembership u e es) lvl u e es

class (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) => HasMembershipWhenCurrentLevel_ c lvl u e es | u e es -> c

Instances

(lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) => HasMembershipWhenCurrentLevel_ c lvl u e es

Defined in Data.Hefty.Union

type SearchMemberRecWhenLowerLevel lvl rest u e = SearchMemberRecWhenLowerLevel_ (SearchMemberRec rest u e rest) lvl rest u e

class (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) => SearchMemberRecWhenLowerLevel_ c lvl rest u e | rest u e -> c

Instances

(lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) => SearchMemberRecWhenLowerLevel_ c lvl rest u e

Defined in Data.Hefty.Union

(|+) :: Union u => (e a -> r) -> (u es f a -> r) -> u (LiftIns e ': es) f a -> r infixr 5

type U u ef = UH u (LiftIns ef)

Recursively decompose the sum of first-order effects into a list, following the direction of right association, with normalization.

type UH u eh = SumToUnionList u (NormalizeSig eh)

Recursively decompose the sum of higher-order effects into a list, following the direction of right association, with normalization.

type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where ...

Recursively decompose the sum of higher-order effects into a list, following the direction of right association.

Equations

SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2

SumToUnionList u LNop = '[]

SumToUnionList u (SingleSig e) = '[e]

type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where ...

Convert a given list of higher-order effect classes into a suitable representation type for each case of being empty, single, or multiple.

Equations

MultiListToUnion u '[] = LNop

MultiListToUnion u '[e] = e

MultiListToUnion u es = u es

type family NormalizeSig e where ...

Normalization in preparation for decomposing the sum of effect classes into a list.

In particular, mark an indivisible, single effect class by applying the SingleSig wrapper to it.

Equations

NormalizeSig LNop = LNop

NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2)

NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2

NormalizeSig e = SingleSig e

newtype SingleSig (e :: SigClass) f a

A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as a sum.

Constructors

SingleSig

Fields

• unSingleSig :: e f a

Instances

HFunctor e => HFunctor (SingleSig e)

Defined in Data.Hefty.Union

Methods

hfmap :: forall (f :: Type -> Type) (g :: Type -> Type). (f :-> g) -> SingleSig e f :-> SingleSig e g

type family UnionListToSum (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where ...

Equations

UnionListToSum u '[e] = UnionToSum u e

UnionListToSum u '[] = LNop

UnionListToSum u (e ': r) = UnionToSum u e :+: UnionListToSum u r

type family UnionToSum (u :: [SigClass] -> SigClass) (e :: SigClass) :: SigClass where ...

Equations

UnionToSum u (u es) = UnionListToSum u es

UnionToSum u e = e

type S u es = UnionListToSum u es Nop

type SH u es = UnionListToSum u es

type NormalFormUnionList u es = U u (S u es) ~ es

type NormalFormUnionListH u es = UH u (SH u es) ~ es

type NFU u es = NormalFormUnionList u es

type NFUH u es = NormalFormUnionListH u es

type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le

type family UnliftIfSingle e where ...

Equations

UnliftIfSingle (LiftIns e) = e

UnliftIfSingle e = e Nop

class LiftInsIfSingle e le where

Methods

liftInsIfSingle :: e ~> le Nop

unliftInsIfSingle :: le Nop ~> e

Instances

LiftInsIfSingle e (LiftIns e)

Defined in Data.Hefty.Union

Methods

liftInsIfSingle :: e ~> LiftIns e Nop

unliftInsIfSingle :: LiftIns e Nop ~> e

LiftInsIfSingle (e Nop) e

Defined in Data.Hefty.Union

Methods

liftInsIfSingle :: e Nop ~> e Nop

unliftInsIfSingle :: e Nop ~> e Nop

type family ClassIndex (es :: [SigClass]) (e :: SigClass) :: Nat where ...

Equations

ClassIndex (e ': es) e = 0

ClassIndex (_ ': es) e = 1 + ClassIndex es e

ClassIndex '[] e = TypeError (('Text "The effect class \8216" :<>: 'ShowType e) :<>: 'Text "\8217 was not found in the list.")

type MemberBy u key e efs = (Member u (key #> e) efs, Lookup key efs ~ 'Just (LiftIns (key #> e)))

type MemberHBy u key e ehs = (MemberH u (key ##> e) ehs, Lookup key ehs ~ 'Just (key ##> e))

type family Lookup (key :: k) es :: Maybe SigClass where ...

Equations

Lookup key ((key ##> e) ': _) = 'Just (key ##> e)

Lookup key (LiftIns (key #> e) ': _) = 'Just (LiftIns (key #> e))

Lookup key (u es ': es') = Lookup key es `OrElse` Lookup key es'

Lookup key (_ ': es) = Lookup key es

Lookup key '[] = 'Nothing

type family OrElse (a :: Maybe k) (b :: Maybe k) :: Maybe k where ...

Equations

OrElse ('Just a) _ = 'Just a

OrElse 'Nothing a = a