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