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

Safe Haskell Safe 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) (x :: k) (y :: k) (xs :: [k]) :: [k] where ... Source #

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

Equations

 ReplaceIndexImpl i ctx n x x xs = xs ReplaceIndexImpl i ctx n x 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 x y (z ': xs) = y ': xs ReplaceIndexImpl i ctx n x y (z ': xs) = z ': ReplaceIndexImpl i ctx (n - 1) x 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 x xs = xs 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")