Data.Diverse.Type

Documentation

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

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

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)

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)

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

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

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

Ensures that the type list contain unique types

type family Distinct (xs :: [k]) :: [k] where ...

Return the list of distinct types in a typelist

Equations

Distinct '[] = '[]

Distinct (x ': xs) = DistinctImpl xs x xs

type Unique x xs = UniqueImpl xs x xs

Ensures that x only ever appears once in xs

type IndexOf x xs = IndexOfImpl xs x xs

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

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

Get the type at an index

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

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

Get the types at an list of index

Equations

KindsAtIndices '[] xs = '[]

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

type family Without (x :: k) (xs :: [k]) :: [k] where ...

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

Equations

Without x '[] = '[]

Without x (x ': xs) = Without x xs

Without x (y ': xs) = y ': Without x xs

type WithoutIndex n xs = WithoutIndexImpl n xs n xs

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

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

Gets the ength of a typelist

Equations

Length '[] = 0

Length (x ': xs) = 1 + Length xs

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

Get the typelist without the Head type

Equations

Tail '[] = TypeError (Text "Cannot Tail an empty type list")

Tail (x ': xs) = xs

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

Get the first type in a typelist

Equations

Head '[] = TypeError (Text "Cannot Head an empty type list")

Head (x ': xs) = x

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

Get the last type in a typelist

Equations

Last '[] = TypeError (Text "Cannot Last an empty type list")

Last (x ': (x' ': xs)) = Last (x' ': xs)

Last '[x] = x

type SameLength xs ys = SameLengthImpl xs ys xs ys

Ensures two typelists are the same length

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

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

Equations

Complement xs '[] = xs

Complement xs (y ': ys) = Complement (Without y xs) ys

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

Returns a xs appended with ys

Equations

Append '[] ys = ys

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

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

Returns the typelist without the Last type

Equations

Init '[] = TypeError (Text "Cannot Init an empty type list")

Init '[x] = '[]

Init (x ': xs) = x ': Init xs