Safe Haskell	Safe
Language	Haskell2010

Data.Diverse.TypeLevel

Synopsis

Documentation

type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs)) Source #

Ensures that x is a unique member of xs, and that natVal can be used.

type family UniqueMembers (xs :: [k]) (ys :: [k]) :: Constraint where ... Source #

Every x in xs is a `UniqueMember x ys`

Equations

UniqueMembers '[] ys = ()
UniqueMembers (x ': xs) ys = (UniqueMember x ys, UniqueMembers xs ys)

type UniqueLabelMember l xs = (UniqueLabel l xs, KnownNat (IndexOf (KindAtLabel l xs) xs)) Source #

Ensures that x is a unique member of xs, and that natVal can be used.

type MaybeUniqueMember x xs = (Unique x xs, KnownNat (PositionOf x xs)) Source #

Ensures that x is a unique member of xs if it exists, and that natVal can be used.

type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs) Source #

Ensures that x is a member of xs at n, and that natVal can be used.

type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs) Source #

Ensures that x is a member of xs at n if it exists, and that natVal can be used.

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

Snoc x to end of xs if x doesn't already exist in xs

Equations

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

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

For each y in ys, snocs them to end of xs if y doesn't already exist in xs

Equations

AppendUnique '[] xs = xs
AppendUnique xs '[] = xs
AppendUnique xs xs = xs
AppendUnique xs (y ': ys) = AppendUnique (SnocUnique xs y) ys

type family UniqueIfExists ys x xs :: Constraint where ... Source #

Ensures x is a unique member in xs iff it exists in ys

Equations

UniqueIfExists '[] x xs = ()
UniqueIfExists (y ': ys) y xs = Unique y xs
UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs

type IsDistinct xs = IsDistinctImpl xs xs Source #

Ensures that the type list contain unique types

type family Nub (xs :: [k]) :: [k] where ... Source #

Return the list of distinct types in a typelist

Equations

Nub '[] = '[]
Nub (x ': xs) = NubImpl xs x xs

type Unique x xs = UniqueImpl xs x xs Source #

Ensures that x only ever appears once in xs

type UniqueLabel l xs = UniqueLabelImpl xs l xs Source #

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

type family UniqueLabels (ls :: [k1]) (xs :: [k]) :: Constraint where ... Source #

Ensures that the label list all UniqueLabels

Equations

UniqueLabels '[] xs = ()
UniqueLabels (l ': ls) xs = (UniqueLabel l xs, UniqueLabels ls xs)

type IndexOf x xs = IndexOfImpl xs x xs Source #

Get the first index of a type (Indexed by 0) Will result in type error if x doesn't exist in xs.

type PositionOf x xs = PositionOfImpl 0 x xs Source #

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

type KindAtIndex n xs = KindAtIndexImpl n xs n xs Source #

Get the type at an index

type KindAtLabel l xs = KindAtLabelImpl l xs xs Source #

Get the type at a label

type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where ... Source #

It's actually ok for the position to be zero, but if it's not zero then the types must match

Equations

KindAtPositionIs 0 x xs = ()
KindAtPositionIs n x xs = x ~ KindAtIndexImpl (n - 1) xs (n - 1) xs

type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where ... Source #

Get the types at an list of index

Equations

KindsAtIndices '[] xs = '[]
KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs

type family KindsAtLabels (ls :: [k1]) (xs :: [k]) :: [k] where ... Source #

Get the types with labels ls from xs

Equations

KindsAtLabels '[] xs = '[]
KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs

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

The typelist xs without first x. It is okay for x not to exist in xs

Equations

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

type Replace x y xs = ReplaceImpl x y xs Source #

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

type Replaces xs ys zs = ReplacesImpl xs ys xs ys zs Source #

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

type RemoveIndex n xs = RemoveIndexImpl n xs n xs Source #

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

type ReplaceIndex n y xs = ReplaceIndexImpl n xs n y xs Source #

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

type ReplacesIndex ns ys xs = ReplacesIndexImpl 0 ns ys xs 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

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

Returns the typelist up to and excluding x. If x doesn't exist, then the original xs is returned.

Equations

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

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

Returns the typelist up to and including x. If x doesn't exist, then the original xs is returned.

Equations

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

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

Returns the typelist after and excluding x. If x doesn't exist, then an empty '[] is returned.

Equations

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

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

Returns the typelist after and including x. If x doesn't exist, then an empty '[] is returned.

Equations

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

type family BeforeIndex (n :: Nat) (xs :: [k]) :: [k] where ... Source #

Returns the typelist before (and exluding) index n. If n is larger then the xs size, then the original xs is returned.

Equations

BeforeIndex n '[] = '[]
BeforeIndex 0 xs = '[]
BeforeIndex n (x ': xs) = x ': BeforeIndex (n - 1) xs

type family ToIndex (n :: Nat) (xs :: [k]) :: [k] where ... Source #

Returns the typelist up to (and including) index n. If n is larger then the xs size, then the original xs is returned.

Equations

ToIndex n '[] = '[]
ToIndex 0 (x ': xs) = '[x]
ToIndex n (x ': xs) = x ': ToIndex (n - 1) xs

type family AfterIndex (n :: Nat) (xs :: [k]) :: [k] where ... Source #

Returns the typelist after (and exluding) index n. If n is larger then the xs size, then an empty '[] is returned.

Equations

AfterIndex n '[] = '[]
AfterIndex 0 (_ ': xs) = xs
AfterIndex n (x ': xs) = AfterIndex (n - 1) xs

type family FromIndex (n :: Nat) (xs :: [k]) :: [k] where ... Source #

Returns the typelist from (and including) index n. If n is larger then the xs size, then an empty '[] is returned.

Equations

FromIndex n '[] = '[]
FromIndex 0 xs = xs
FromIndex n (x ': xs) = FromIndex (n - 1) xs

type family Tail (xs :: [k]) :: [k] where ... Source #

Get the typelist without the Head type

Equations

Tail '[] = TypeError (Text "Tail error: empty type list")
Tail (x ': xs) = xs

type family Head (xs :: [k]) :: k where ... Source #

Get the first type in a typelist

Equations

Head '[] = TypeError (Text "Head error: empty type list")
Head (x ': xs) = x

type family Last (xs :: [k]) :: k where ... Source #

Equations

Last '[] = TypeError (Text "Last error: empty type list")
Last (x ': (x' ': xs)) = Last (x' ': xs)
Last '[x] = x

type family Length (xs :: [k]) :: Nat where ... Source #

Equations

Length '[] = 0
Length (x ': xs) = 1 + Length xs

type SameLength xs ys = SameLengthImpl xs ys xs ys Source #

Ensures two typelists are the same length

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

Set complement. Returns the set of things in xs that are not in ys.

Equations

Complement xs '[] = xs
Complement xs (y ': ys) = Complement (Remove y xs) ys

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

Returns a xs appended with ys

Equations

Append xs '[] = xs
Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys

type family Init (xs :: [k]) :: [k] where ... Source #

Returns the typelist without the Last type

Equations

Init '[] = TypeError (Text "Init error: empty type list")
Init '[x] = '[]
Init (x ': xs) = x ': Init xs

type Zip xs ys = ZipImpl xs ys xs ys Source #

Takes two lists which must be the same length and returns a list of corresponding pairs.

type family CaseResult (c :: [k1] -> k2) (x :: k1) :: k2 Source #

The result from evaluating a Case with a type from a typelist.

Instances

type CaseResult * Type (CaseFunc' k) x Source #
type CaseResult * Type (CaseFunc' k) x = x
type CaseResult * Type (CaseFunc k r) x Source #
type CaseResult * Type (CaseFunc k r) x = r
type CaseResult * Type (Cases fs r) x Source #
type CaseResult * Type (Cases fs r) x = r
type CaseResult * Type (CasesN fs r n) x Source #
type CaseResult * Type (CasesN fs r n) x = r

type family CaseResults (c :: [k1] -> k2) (xs :: [k1]) :: [k2] where ... Source #

Return a list of results from applying CaseResult to every type in the xs typelist.

Equations

CaseResults c '[] = '[]
CaseResults c (x ': xs) = CaseResult c x ': CaseResults c xs

type family AllConstrained (c :: k -> Constraint) (xs :: [k]) :: Constraint where ... Source #

Tests if all the types in a typelist satisfy a constraint

Equations

AllConstrained c '[] = ()
AllConstrained c (x ': xs) = (c x, AllConstrained c xs)