Safe Haskell | None |
---|
- class HasAny a l b | a l -> b
- viewType :: (HasAny a (Tail (NormalConstr l a l')) False, HavingType a l l') => l -> NormalConstr l a l'
- viewTypeOf :: (HasAny a (Tail (NormalConstr l a l')) False, HavingType a l l') => l -> a -> NormalConstr l a l'
- class HavingType a l l' | a l -> l' where
- viewFirstType :: l -> NormalConstr l a l'
- viewFirstTypeOf :: l -> a -> NormalConstr l a l'
- class DeleteAllType a l l' | a l -> l' where
- deleteAllTypeOf :: l -> a -> l'
- class NubType l l' | l -> l' where
- nubType :: l -> l'
Documentation
Operations on Normal
form types which make use of type equality. The type
level boolean type we use is the lifted Bool
type, requiring DataKinds
.
Most of the functions here require all terms to be unambiguous, so you might find some type annotations are necessary.
This module will be getting more functionality going forward.
viewType :: (HasAny a (Tail (NormalConstr l a l')) False, HavingType a l l') => l -> NormalConstr l a l'Source
Shift the only occurrence of type a
to the Head
of l
.
viewType = viewFirstType
viewTypeOf :: (HasAny a (Tail (NormalConstr l a l')) False, HavingType a l l') => l -> a -> NormalConstr l a l'Source
class HavingType a l l' | a l -> l' whereSource
The non-empty, Product
or Sum
l
, out of which we can pull the
first occurrence of type a
, leaving as the Tail
l'
.
viewFirstType :: l -> NormalConstr l a l'Source
Shift the first occurrence of type a
to the Head
of l
.
viewFirstTypeOf :: l -> a -> NormalConstr l a l'Source
viewFirstType
of the same type as its second argument.
viewFirstTypeOf = const . viewFirstType
Sum (Either () ()) => HavingType () (Either () ()) () | |
Sum (Either () ps) => HavingType () (Either () ps) ps | |
(HavingType a y l', ~ * (Either x l') xl', Sum y) => HavingType a (Either x y) xl' | |
(~ * x' x, Product p) => HavingType p (Either x p) x' | |
(Product l, HavingType a l l', ~ * (x, l') xl') => HavingType a (x, l) xl' | |
Product l => HavingType a (a, l) l | |
Sum (Either (x, y) ps) => HavingType (x, y) (Either (x, y) ps) ps | |
Sum (Either (x, y) (x, y)) => HavingType (x, y) (Either (x, y) (x, y)) (x, y) |
On Product
s
class DeleteAllType a l l' | a l -> l' whereSource
deleteAllTypeOf :: l -> a -> l'Source
Drop any occurrences of type a
from the list l
, leaving l'
.
~ * u () => DeleteAllType a () u | |
(DeleteAllType a l l', ~ * (x, l') x_l') => DeleteAllType a (x, l) x_l' | |
DeleteAllType a l l' => DeleteAllType a (a, l) l' |