Data.Shapely.Normal.TypeIndexed

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.

class HasAny a l b | a l -> b

A type equality predicate class.

Instances

HasAny a () False

~ Bool false False => HasAny p (Only x) false

HasAny p (Only p) True

HasAny a (Tail (Either x l)) b => HasAny a (Either x l) b

HasAny p (Either p ps) True

HasAny a l b => HasAny a (x, l) b

HasAny a (a, l) True

viewType :: (HasAny a (Tail (NormalConstr l a l')) False, HavingType a l l') => l -> NormalConstr l a l'

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'

class HavingType a l l' | a l -> l' where

The non-empty, Product or Sum l, out of which we can pull the first occurrence of type a, leaving as the Tail l'.

Methods

viewFirstType :: l -> NormalConstr l a l'

Shift the first occurrence of type a to the Head of l.

viewFirstTypeOf :: l -> a -> NormalConstr l a l'

viewFirstType of the same type as its second argument.

 viewFirstTypeOf = const . viewFirstType

Instances

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 Products

class DeleteAllType a l l' | a l -> l' where

Methods

deleteAllTypeOf :: l -> a -> l'

Drop any occurrences of type a from the list l, leaving l'.

Instances

~ * 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'

class NubType l l' | l -> l' where

Methods

nubType :: l -> l'

Remove all but the first occurrence of each type.

Instances

~ * () l' => NubType () l'

(DeleteAllType x xys ys, NubType ys ys', ~ * x_ys' (x, ys')) => NubType (x, xys) x_ys'