Safe Haskell	Safe
Language	Haskell2010

Data.Diverse.TypeLevel.Internal

Synopsis

Documentation

type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where ... Source #

Get the first position of a type (indexed by 1) Will return 0 if x doesn't exists in xs.

Equations

PositionOfImpl i x (x ': xs) = i + 1
PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs
PositionOfImpl i x '[] = 0

type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where ... Source #

Get the first index of a type from a list

Equations

IndexOfImpl ctx x (x ': xs) = 0
IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs
IndexOfImpl ctx y '[] = TypeError ((((((Text "IndexOf error: \8216" :<>: ShowType y) :<>: Text "\8217") :<>: Text " is not a member of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")

type family NubImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where ... Source #

Searches for y in ys if not found, than use y, and repeat search with next (y ': ys) in ctx else if found, then don't use y, then repeat search with next (y ': ys) in ctx

Equations

NubImpl '[] y '[] = y ': '[]
NubImpl '[] y (y ': xs) = '[]
NubImpl (x ': xs) y '[] = y ': NubImpl xs x xs
NubImpl (x ': xs) y (y ': ys) = NubImpl xs x xs
NubImpl ctx y (x ': xs) = NubImpl ctx y xs

type family IsUniqueImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where ... Source #

Errors if a type exists in a typelist

Equations

IsUniqueImpl ctx y '[] = ()
IsUniqueImpl ctx x (x ': xs) = TypeError ((((((Text "Not unique error: \8216" :<>: ShowType x) :<>: Text "\8217") :<>: Text " is a duplicate in ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")
IsUniqueImpl ctx y (x ': xs) = IsUniqueImpl ctx y xs

type family IsUniqueLabelImpl (ctx :: [k]) (l :: k2) (xs :: [k]) :: Constraint where ... Source #

Errors if a label exists in a typelist

Equations

IsUniqueLabelImpl ctx y '[] = ()
IsUniqueLabelImpl ctx l (tagged l x ': xs) = TypeError ((((((Text "Not unique label error: \8216" :<>: ShowType l) :<>: Text "\8217") :<>: Text " is a duplicate in ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")
IsUniqueLabelImpl ctx l (x ': xs) = IsUniqueLabelImpl ctx l xs

type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where ... Source #

Ensures that the type list contain unique types. Not implemented as (xs ~ Nub xs) for better type error messages.

Equations

IsDistinctImpl ctx '[] = ()
IsDistinctImpl ctx (x ': xs) = (IsUniqueImpl ctx x xs, IsDistinctImpl ctx xs)

type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where ... Source #

Ensures that x only ever appears once in xs

Equations

UniqueImpl ctx x '[] = ()
UniqueImpl ctx x (x ': xs) = IsUniqueImpl ctx x xs
UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs

type family UniqueLabelImpl (ctx :: [k]) (l :: k1) (xs :: [k]) :: Constraint where ... Source #

Ensures that the label in tagged label v only ever appears once in xs.

Equations

UniqueLabelImpl ctx l '[] = ()
UniqueLabelImpl ctx l (tagged l x ': xs) = IsUniqueLabelImpl ctx l xs
UniqueLabelImpl ctx l (y ': xs) = UniqueLabelImpl ctx l xs

type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where ... Source #

Indexed access into the list

Equations

KindAtIndexImpl i ctx 0 '[] = TypeError ((((((Text "KindAtIndex error: Index \8216" :<>: ShowType i) :<>: Text "\8217") :<>: Text " is out of bounds of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")
KindAtIndexImpl i ctx 0 (x ': xs) = x
KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs

type family KindAtLabelImpl (l :: k1) (ctx :: [k]) (xs :: [k]) :: k where ... Source #

Labelled access into the list

Equations

KindAtLabelImpl l ctx '[] = TypeError ((((((Text "KindAtLabel error: Label \8216" :<>: ShowType l) :<>: Text "\8217") :<>: Text " is not found in ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")
KindAtLabelImpl l ctx (tagged l x ': xs) = tagged l x
KindAtLabelImpl l ctx (x ': xs) = KindAtLabelImpl l ctx xs

type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where ... Source #

Ensures two typelists are the same length

Equations

SameLengthImpl as bs '[] '[] = ()
SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys
SameLengthImpl as bs xs ys = TypeError ((((((Text "SameLength error: \8216" :<>: ShowType as) :<>: Text "\8217") :<>: Text " is not the same length as ") :<>: Text "\8216") :<>: ShowType bs) :<>: Text "\8217")

type family RemoveIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where ... Source #

The typelist xs without the type at Nat n. n must be within bounds of xs

Equations

RemoveIndexImpl i ctx n '[] = TypeError ((((((Text "RemoveIndex error: Index \8216" :<>: ShowType i) :<>: Text "\8217") :<>: Text " is out of bounds of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")
RemoveIndexImpl i ctx 0 (x ': xs) = xs
RemoveIndexImpl i ctx n (x ': xs) = x ': RemoveIndexImpl i ctx (n - 1) xs

type family ReplaceIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (y :: k) (xs :: [k]) :: [k] where ... Source #

The typelist xs without the type at Nat n replaced by y. n must be within bounds of xs

Equations

ReplaceIndexImpl i ctx n y '[] = TypeError ((((((Text "ReplaceIndex error: Index \8216" :<>: ShowType i) :<>: Text "\8217") :<>: Text " is out of bounds of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")
ReplaceIndexImpl i ctx 0 y (x ': xs) = y ': xs
ReplaceIndexImpl i ctx n y (x ': xs) = x ': ReplaceIndexImpl i ctx (n - 1) y xs

type family ReplaceImpl (x :: k) (y :: k) (xs :: [k]) :: [k] where ... Source #

The typelist xs with the first x replaced by y. It is okay for x not to exist in xs

Equations

ReplaceImpl x y '[] = '[]
ReplaceImpl x y (x ': xs) = y ': xs
ReplaceImpl x y (z ': xs) = z ': ReplaceImpl x y xs

type family ReplacesImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) (zs :: [k]) :: [k] where ... Source #

The typelist zs with the first xs replaced by ys. xs must be the same size as ys

Equations

ReplacesImpl xs' ys' xs ys '[] = '[]
ReplacesImpl xs' ys' '[] '[] (z ': zs) = z ': ReplacesImpl xs' ys' xs' ys' zs
ReplacesImpl xs' ys' (x ': xs) (y ': ys) (x ': zs) = y ': ReplacesImpl xs' ys' xs' ys' zs
ReplacesImpl xs' ys' (x ': xs) (y ': ys) (z ': zs) = ReplacesImpl xs' ys' xs ys (z ': zs)
ReplacesImpl xs' ys' xs ys zs = TypeError ((((((Text "Replaces error: \8216" :<>: ShowType xs') :<>: Text "\8217") :<>: Text " must be the same size as ") :<>: Text "\8216") :<>: ShowType ys') :<>: Text "\8217")

type family ReplaceIfIndex (ns :: [Nat]) (ys :: [k]) (i :: Nat) (x :: k) :: k where ... Source #

The type x replaced by an y if an n matches i.

Equations

ReplaceIfIndex '[] ys i x = x
ReplaceIfIndex ns '[] i x = x
ReplaceIfIndex (n ': ns) (y ': ys) n x = y
ReplaceIfIndex (n ': ns) (y ': ys) i x = ReplaceIfIndex ns ys i x

type family ReplacesIndexImpl (i :: Nat) (ns :: [Nat]) (ys :: [k]) (xs :: [k]) :: [k] where ... Source #

The typelist xs replaced by ys at the indices ns. ns and ys must be the same length. ns must be within bounds of xs

Equations

ReplacesIndexImpl i ns ys '[] = '[]
ReplacesIndexImpl i '[] '[] xs = xs
ReplacesIndexImpl i ns ys (x ': xs) = ReplaceIfIndex ns ys i x ': ReplacesIndexImpl (i + 1) ns ys xs
ReplacesIndexImpl i ns ys xs = TypeError ((((((Text "ReplacesIndex error: \8216" :<>: ShowType ns) :<>: Text "\8217") :<>: Text " must be the same size as ") :<>: Text "\8216") :<>: ShowType ys) :<>: Text "\8217")

type family ZipImpl (xs' :: [k]) (ys' :: [k]) (xs :: [k]) (ys :: [k]) :: [k] where ... Source #

Zips up xs and ys, which must be the same length

Equations

ZipImpl xs' ys' '[] '[] = '[]
ZipImpl xs' ys' (x ': xs) (y ': ys) = (x, y) ': ZipImpl xs' ys' xs ys
ZipImpl xs' ys' xs ys = TypeError ((((((Text "Zip error: \8216" :<>: ShowType xs') :<>: Text "\8217") :<>: Text " must be the same size as ") :<>: Text "\8216") :<>: ShowType ys') :<>: Text "\8217")