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

Data.Diverse.TypeLevel

Synopsis

# Documentation

class NatToInt (n :: Nat) where Source #

Produce a runtime Int value corresponding to a Nat type. Based on https://github.com/VinylRecords/Vinyl/blob/a5ffd10fbc747c5366ae9806e61bf45f78c3eb33/Data/Vinyl/TypeLevel.hs This is used instead of KnownNat because to avoid inefficient Integer https://github.com/louispan/data-diverse/issues/8 AllowsAmbiguousTypes! Uses TypeApplication instead of Proxy

Minimal complete definition

natToInt

Methods

Instances
 (NatToInt m, n ~ (m + 1)) => NatToInt n Source # Instance detailsDefined in Data.Diverse.TypeLevel Methods Source # Instance detailsDefined in Data.Diverse.TypeLevel Methods

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

Ensures that x is a unique member of xs, and that natToInt 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, NatToInt (IndexOf (KindAtLabel l xs) xs)) Source #

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

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

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

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

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

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

Ensures that x is a member of xs at n if it exists, and that natToInt 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 :: [k]) = 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 :: k) (xs :: [k]) = UniqueImpl xs x xs Source #

Ensures that x only ever appears once in xs

type UniqueLabel (l :: k1) (xs :: [k]) = 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 :: k) (xs :: [k]) = 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 :: k) (xs :: [k]) = 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 :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs Source #

Get the type at an index

type KindAtLabel (l :: k1) (xs :: [k]) = 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 :: k) (y :: k) (xs :: [k]) = 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 :: [k]) (ys :: [k]) (zs :: [k]) = 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 :: Nat) (xs :: [k]) = 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 :: Nat) (x :: k) (y :: k) (xs :: [k]) = ReplaceIndexImpl n xs n x 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 :: [Nat]) (ys :: [k]) (xs :: [k]) = 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 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

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 SameLength (xs :: [k1]) (ys :: [k2]) = 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 :: [k]) (ys :: [k]) = 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 (CaseFunc' k :: [Type] -> *) (x :: Type) Source # Instance detailsDefined in Data.Diverse.CaseFunc type CaseResult (CaseFunc' k :: [Type] -> *) (x :: Type) = x type CaseResult (CaseFunc k r :: [Type] -> *) (x :: Type) Source # Instance detailsDefined in Data.Diverse.CaseFunc type CaseResult (CaseFunc k r :: [Type] -> *) (x :: Type) = r type CaseResult (Cases fs r :: [Type] -> *) (x :: Type) Source # Instance detailsDefined in Data.Diverse.Cases type CaseResult (Cases fs r :: [Type] -> *) (x :: Type) = r type CaseResult (CasesN fs r n :: [Type] -> *) (x :: Type) Source # Instance detailsDefined in Data.Diverse.Cases type CaseResult (CasesN fs r n :: [Type] -> *) (x :: Type) = r type CaseResult (CaseFunc1' k k1 k0 :: [Type] -> *) (f x :: Type) Source # Instance detailsDefined in Data.Diverse.CaseFunc type CaseResult (CaseFunc1' k k1 k0 :: [Type] -> *) (f x :: Type) = f x type CaseResult (CaseFunc1 k k1 k0 r :: [Type] -> *) (f x :: Type) Source # Instance detailsDefined in Data.Diverse.CaseFunc type CaseResult (CaseFunc1 k k1 k0 r :: [Type] -> *) (f x :: Type) = f 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)

class C0 a Source #

This is useful as a level function for k in CaseFunc1

Instances
 C0 (a :: k) Source # Instance detailsDefined in Data.Diverse.TypeLevel

class (c1 a, c2 a) => C2 c1 c2 a Source #

Instances
 (c1 a, c2 a) => C2 (c1 :: k -> Constraint) (c2 :: k -> Constraint) (a :: k) Source # Instance detailsDefined in Data.Diverse.TypeLevel

class (c1 a, c2 a, c3 a) => C3 c1 c2 c3 a Source #

Instances
 (c1 a, c2 a, c3 a) => C3 (c1 :: k -> Constraint) (c2 :: k -> Constraint) (c3 :: k -> Constraint) (a :: k) Source # Instance detailsDefined in Data.Diverse.TypeLevel

class (c1 a, c2 a, c3 a, c4 a) => C4 c1 c2 c3 c4 a Source #

Instances
 (c1 a, c2 a, c3 a, c4 a) => C4 (c1 :: k -> Constraint) (c2 :: k -> Constraint) (c3 :: k -> Constraint) (c4 :: k -> Constraint) (a :: k) Source # Instance detailsDefined in Data.Diverse.TypeLevel

class (c1 a, c2 a, c3 a, c4 a, c5 a) => C5 c1 c2 c3 c4 c5 a Source #

Instances
 (c1 a, c2 a, c3 a, c4 a, c5 a) => C5 (c1 :: k -> Constraint) (c2 :: k -> Constraint) (c3 :: k -> Constraint) (c4 :: k -> Constraint) (c5 :: k -> Constraint) (a :: k) Source # Instance detailsDefined in Data.Diverse.TypeLevel

class (c1 a, c2 a, c3 a, c4 a, c5 a, c6 a) => C6 c1 c2 c3 c4 c5 c6 a Source #

Instances
 (c1 a, c2 a, c3 a, c4 a, c5 a, c6 a) => C6 (c1 :: k -> Constraint) (c2 :: k -> Constraint) (c3 :: k -> Constraint) (c4 :: k -> Constraint) (c5 :: k -> Constraint) (c6 :: k -> Constraint) (a :: k) Source # Instance detailsDefined in Data.Diverse.TypeLevel