Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

- type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs))
- type family UniqueMembers (xs :: [k]) (ys :: [k]) :: Constraint where ...
- type UniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ IndexOf x xs)
- type UniqueLabelMember l xs = (UniqueLabel l xs, KnownNat (IndexOf (KindAtLabel l xs) xs))
- type MaybeUniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ PositionOf x xs)
- type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs)
- type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs)
- type family SnocUnique (xs :: [k]) (x :: k) :: [k] where ...
- type family AppendUnique (xs :: [k]) (ys :: [k]) :: [k] where ...
- type family UniqueIfExists ys x xs :: Constraint where ...
- type IsDistinct xs = IsDistinctImpl xs xs
- type family Nub (xs :: [k]) :: [k] where ...
- type Unique x xs = UniqueImpl xs x xs
- type UniqueLabel l xs = UniqueLabelImpl xs l xs
- type family UniqueLabels (ls :: [k1]) (xs :: [k]) :: Constraint where ...
- type IndexOf x xs = IndexOfImpl xs x xs
- type PositionOf x xs = PositionOfImpl 0 x xs
- type KindAtIndex n xs = KindAtIndexImpl n xs n xs
- type KindAtLabel l xs = KindAtLabelImpl l xs xs
- type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where ...
- type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where ...
- type family KindsAtLabels (ls :: [k1]) (xs :: [k]) :: [k] where ...
- type family Remove (x :: k) (xs :: [k]) :: [k] where ...
- type Replace x y xs = ReplaceImpl x y xs
- type Replaces xs ys zs = ReplacesImpl xs ys xs ys zs
- type RemoveIndex n xs = RemoveIndexImpl n xs n xs
- type ReplaceIndex n y xs = ReplaceIndexImpl n xs n y xs
- type ReplacesIndex ns ys xs = ReplacesIndexImpl 0 ns ys xs
- type family Before (x :: k) (xs :: [k]) :: [k] where ...
- type family To (x :: k) (xs :: [k]) :: [k] where ...
- type family After (x :: k) (xs :: [k]) :: [k] where ...
- type family From (x :: k) (xs :: [k]) :: [k] where ...
- type family BeforeIndex (n :: Nat) (xs :: [k]) :: [k] where ...
- type family ToIndex (n :: Nat) (xs :: [k]) :: [k] where ...
- type family AfterIndex (n :: Nat) (xs :: [k]) :: [k] where ...
- type family FromIndex (n :: Nat) (xs :: [k]) :: [k] where ...
- type family Tail (xs :: [k]) :: [k] where ...
- type family Head (xs :: [k]) :: k where ...
- type family Last (xs :: [k]) :: k where ...
- type family Length (xs :: [k]) :: Nat where ...
- type SameLength xs ys = SameLengthImpl xs ys xs ys
- type family Complement (xs :: [k]) (ys :: [k]) :: [k] where ...
- type family Append (xs :: [k]) (ys :: [k]) :: [k] where ...
- type family Init (xs :: [k]) :: [k] where ...
- type Zip xs ys = ZipImpl xs ys xs ys
- type family CaseResult (c :: [k1] -> k2) (x :: k1) :: k2
- type family CaseResults (c :: [k1] -> k2) (xs :: [k1]) :: [k2] where ...
- type family AllConstrained (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...

# 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`

UniqueMembers '[] ys = () | |

UniqueMembers (x ': xs) ys = (UniqueMember x ys, UniqueMembers xs ys) |

type UniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ IndexOf x xs) Source #

Ensures that `x`

is a unique member of `xs`

, and that `natVal`

can be used.

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 MaybeUniqueMemberAt n x xs = (Unique x xs, KnownNat n, n ~ 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`

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`

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`

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

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 `UniqueLabel`

s

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

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

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`

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`

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.

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.

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.

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.

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.

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.

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.

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.

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`

.

Complement xs '[] = xs | |

Complement xs (y ': ys) = Complement (Remove y xs) ys |

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.

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.

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

AllConstrained c '[] = () | |

AllConstrained c (x ': xs) = (c x, AllConstrained c xs) |