Data.Effect.OpenUnion.Internal

Documentation

newtype P (e :: k) (es :: [k])

Represents position of element e :: k in a type list es :: [k].

Constructors

P

Fields

• unP :: Word

type FindElem (e :: a) (es :: [a]) = KnownNat (ElemIndex e es)

elemNo :: forall {k} (e :: k) (es :: [k]). FindElem e es => P e es

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

Equations

ElemIndex (e :: a) (e ': es :: [a]) = 0

ElemIndex (e :: a) (_1 ': es :: [a]) = 1 + ElemIndex e 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 IfNotFound (e :: k) (r :: [k]) (w :: [k])

Instance resolution for this class fails with a custom type error if e :: k is not in the list w :: [k].

Instances

IfNotFound (e :: k) (r :: [k]) (w :: [k])

Pass if r is uninstantiated. The incoherence here is safe, since picking this instance doesn’t cause any variation in behavior, except possibly the production of an inferior error message. For more information, see lexi-lambda/freer-simple#3, which describes the motivation in more detail.

Defined in Data.Effect.OpenUnion.Internal

(TypeError ((('Text "\8216" ':<>: 'ShowType e) ':<>: 'Text "\8217 is not a member of the type-level list") ':$$: (('Text " \8216" ':<>: 'ShowType w) ':<>: 'Text "\8217")) :: Constraint) => IfNotFound (e :: k) ('[] :: [k]) (w :: [k])

If we reach an empty list, that’s a failure, since it means the type isn’t in the list.

Defined in Data.Effect.OpenUnion.Internal

IfNotFound (e :: a) (e ': r :: [a]) (w :: [a])

Defined in Data.Effect.OpenUnion.Internal

IfNotFound e r w => IfNotFound (e :: a) (e' ': r :: [a]) (w :: [a])

Defined in Data.Effect.OpenUnion.Internal

type LookupError (key :: kk) (w :: [ke]) = TypeError ((('Text "The key \8216" ':<>: 'ShowType key) ':<>: 'Text "\8217 does not exist in the type-level list") ':$$: (('Text " \8216" ':<>: 'ShowType w) ':<>: 'Text "\8217")) :: k

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

Equations

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

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

wordVal :: forall (n :: Nat). KnownNat n => Word

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

Methods

prefixLen :: Word

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 family Length (es :: [a]) :: Natural where ...

Equations

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

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

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

Instances

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

Defined in Data.Effect.OpenUnion.Internal

reifyLength :: forall {a} (es :: [a]). KnownLength es => Word

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

Equations

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

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

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

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

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

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 StrengthenUnder (offset :: Natural) (es :: [k]) (es' :: [k]) = StrengthenNUnder (PrefixLength es' es) offset es es'

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

type StrengthenMap (len :: Natural) (es :: [k]) (es' :: [k]) = StrengthenMap_ (len == 0) len es es'

class isLenZero ~ (len == 0) => StrengthenMap_ (isLenZero :: Bool) (len :: Natural) (es :: [k]) (es' :: [k]) where

Methods

strengthenMap :: Word -> Word

Instances

StrengthenMap_ 'True 0 (es :: [k]) (es :: [k])

Defined in Data.Effect.OpenUnion.Internal

Methods

strengthenMap :: Word -> Word

(StrengthenMap (len - 1) es es', FindElem e es, (len == 0) ~ 'False) => StrengthenMap_ 'False len (e ': es :: [k]) (es' :: [k])

Defined in Data.Effect.OpenUnion.Internal

Methods

strengthenMap :: Word -> Word

strengthenMapUnder :: forall {k} (len :: Natural) (offset :: Natural) (es :: [k]) (es' :: [k]). StrengthenNUnder len offset es es' => Word -> Word

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 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 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 family Drop (n :: Natural) (es :: [a]) :: [a] where ...

Equations

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

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

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

type family Reverse_ (acc :: [a]) (es :: [a]) :: [a] where ...

Equations

Reverse_ (acc :: [a]) ('[] :: [a]) = acc

Reverse_ (acc :: [a]) (e ': es :: [a]) = Reverse_ (e ': acc) es