Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
- type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where ...
- type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where ...
- type family DistinctImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where ...
- type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where ...
- type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where ...
- type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where ...
- type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where ...
- type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where ...
- type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where ...
Documentation
type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where ... Source #
Get the first position of a type (indexed by 1)
Will return 0 if x
doesn't exists in xs
.
PositionOfImpl i x (x ': xs) = i + 1 | |
PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs | |
PositionOfImpl i x '[] = 0 |
type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where ... Source #
Get the first index of a type from a list
IndexOfImpl ctx x (x ': xs) = 0 | |
IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs | |
IndexOfImpl ctx y '[] = TypeError ((((((Text "\8216" :<>: ShowType y) :<>: Text "\8217") :<>: Text " is not a member of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217") |
type family DistinctImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where ... Source #
Searches for y in ys if not found, than use y, and repeat search with next (y ': ys) in ctx else if found, then don't use y, then repeat search with next (y ': ys) in ctx
DistinctImpl '[] y '[] = y ': '[] | |
DistinctImpl '[] y (y ': xs) = '[] | |
DistinctImpl (x ': xs) y '[] = y ': DistinctImpl xs x xs | |
DistinctImpl (x ': xs) y (y ': ys) = DistinctImpl xs x xs | |
DistinctImpl ctx y (x ': xs) = DistinctImpl ctx y xs |
type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where ... Source #
Errors if a type exists in a typelist
MissingImpl ctx y '[] = () | |
MissingImpl ctx x (x ': xs) = TypeError ((((((Text "\8216" :<>: ShowType x) :<>: Text "\8217") :<>: Text " is a duplicate in ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217") | |
MissingImpl ctx y (x ': xs) = MissingImpl ctx y xs |
type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where ... Source #
Ensures that the type list contain unique types
IsDistinctImpl ctx '[] = () | |
IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs) |
type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where ... Source #
Ensures that x
only ever appears once in xs
UniqueImpl ctx x '[] = () | |
UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs | |
UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs |
type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where ... Source #
Indexed access into the list
KindAtIndexImpl i ctx 0 '[] = TypeError ((((((Text "Index \8216" :<>: ShowType i) :<>: Text "\8217") :<>: Text " is out of bounds of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217") | |
KindAtIndexImpl i ctx 0 (x ': xs) = x | |
KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs |
type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where ... Source #
Ensures two typelists are the same length
SameLengthImpl as bs '[] '[] = () | |
SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys | |
SameLengthImpl as bs xs ys = TypeError ((((((Text "\8216" :<>: ShowType as) :<>: Text "\8217") :<>: Text " is not the same length as ") :<>: Text "\8216") :<>: ShowType bs) :<>: Text "\8217") |
type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where ... Source #
The typelist xs
without the type at Nat n
. n
must be within bounds of xs
WithoutIndexImpl i ctx n '[] = TypeError ((((((Text "Index \8216" :<>: ShowType i) :<>: Text "\8217") :<>: Text " is out of bounds of ") :<>: Text "\8216") :<>: ShowType ctx) :<>: Text "\8217") | |
WithoutIndexImpl i ctx 0 (x ': xs) = xs | |
WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs |