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

Language | Haskell2010 |

- type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs))
- 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 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 Without (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 WithoutIndex n xs = WithoutIndexImpl 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 Tail (xs :: [k]) :: [k] where ...
- type family Head (xs :: [k]) :: k where ...
- type family Last (xs :: [k]) :: k 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

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

KindsAtLabels '[] xs = '[] | |

KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs |

type family Without (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 WithoutIndex n xs = WithoutIndexImpl 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 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 (Without y xs) ys |