data-diverse-2.0.0.0: Extensible records and polymorphic variants.

Safe HaskellSafe
LanguageHaskell2010

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")