Data.Diverse.Type.Internal

Documentation

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

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 ...

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 "\8216" :<>: ShowType y) :<>: Text "\8217") :<>: Text " is not a member of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")

type family DistinctImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where ...

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

DistinctImpl '[] y '[] = y ': '[]

DistinctImpl '[] y (y ': xs) = '[]

DistinctImpl (x ': xs) y '[] = y ': DistinctImpl xs x xs

DistinctImpl (x ': xs) y (y ': ys) = DistinctImpl xs x xs

DistinctImpl ctx y (x ': xs) = DistinctImpl ctx y xs

type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where ...

Errors if a type exists in a typelist

Equations

MissingImpl ctx y '[] = ()

MissingImpl ctx x (x ': xs) = TypeError ((((((Text "\8216" :<>: ShowType x) :<>: Text "\8217") :<>: Text " is a duplicate in ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")

MissingImpl ctx y (x ': xs) = MissingImpl ctx y xs

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

Ensures that the type list contain unique types

Equations

IsDistinctImpl ctx '[] = ()

IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs)

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

Ensures that x only ever appears once in xs

Equations

UniqueImpl ctx x '[] = ()

UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs

UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs

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

Indexed access into the list

Equations

KindAtIndexImpl i ctx 0 '[] = TypeError ((((((Text "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 SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where ...

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 "\8216" :<>: ShowType as) :<>: Text "\8217") :<>: Text " is not the same length as ") :<>: Text "\8216") :<>: ShowType bs) :<>: Text "\8217")

type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where ...

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

Equations

WithoutIndexImpl i ctx n '[] = TypeError ((((((Text "Index \8216" :<>: ShowType i) :<>: Text "\8217") :<>: Text " is out of bounds of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217")

WithoutIndexImpl i ctx 0 (x ': xs) = xs

WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs