generics-mrsop-1.2.2: Generic Programming with Mutually Recursive Sums of Products.

Safe HaskellSafe
LanguageHaskell2010

Generics.MRSOP.Base.NP

Contents

Description

Standard representation of n-ary products.

Synopsis

Documentation

data NP :: (k -> *) -> [k] -> * where #

Indexed n-ary products. This is analogous to the All datatype in Agda.

Constructors

NP0 :: NP p '[] 
(:*) :: p x -> NP p xs -> NP p (x ': xs) infixr 5 
Instances
Eq1 ki => Eq1 (NP ki :: [k] -> Type) # 
Instance details

Defined in Generics.MRSOP.Base.NP

Methods

eq1 :: NP ki k0 -> NP ki k0 -> Bool #

Show (NP (ConstructorInfo :: [Atom kon] -> Type) code) # 
Instance details

Defined in Generics.MRSOP.Base.Metadata

Methods

showsPrec :: Int -> NP ConstructorInfo code -> ShowS #

show :: NP ConstructorInfo code -> String #

showList :: [NP ConstructorInfo code] -> ShowS #

Show (NP (FieldInfo :: Atom kon -> Type) code) # 
Instance details

Defined in Generics.MRSOP.Base.Metadata

Methods

showsPrec :: Int -> NP FieldInfo code -> ShowS #

show :: NP FieldInfo code -> String #

showList :: [NP FieldInfo code] -> ShowS #

(Show1 phi, Show1 ki) => Show (PoA ki (AnnFix ki codes phi) xs) # 
Instance details

Defined in Generics.MRSOP.Base.Show

Methods

showsPrec :: Int -> PoA ki (AnnFix ki codes phi) xs -> ShowS #

show :: PoA ki (AnnFix ki codes phi) xs -> String #

showList :: [PoA ki (AnnFix ki codes phi) xs] -> ShowS #

Relation to IsList predicate

appendNP :: NP p xs -> NP p ys -> NP p (xs :++: ys) #

Append two values of type NP

listPrfNP :: NP p xs -> ListPrf xs #

Proves that the index of a value of type NP is a list. This is useful for pattern matching on said list without having to carry the product around.

Map, Elim and Zip

mapNP :: (f :-> g) -> NP f ks -> NP g ks #

Maps a natural transformation over a n-ary product

mapNPM :: Monad m => (forall x. f x -> m (g x)) -> NP f ks -> m (NP g ks) #

Maps a monadic natural transformation over a n-ary product

elimNP :: (forall x. f x -> a) -> NP f ks -> [a] #

Eliminates the product using a provided function.

elimNPM :: Monad m => (forall x. f x -> m a) -> NP f ks -> m [a] #

Monadic eliminator

zipNP :: NP f xs -> NP g xs -> NP (f :*: g) xs #

Combines two products into one.

unzipNP :: NP (f :*: g) xs -> (NP f xs, NP g xs) #

Unzips a combined product into two separate products

Catamorphism

cataNP :: (forall x xs. f x -> r xs -> r (x ': xs)) -> r '[] -> NP f xs -> r xs #

Consumes a value of type NP.

cataNPM :: Monad m => (forall x xs. f x -> r xs -> m (r (x ': xs))) -> m (r '[]) -> NP f xs -> m (r xs) #

Consumes a value of type NP.

Equality

eqNP :: (forall x. p x -> p x -> Bool) -> NP p xs -> NP p xs -> Bool #

Compares two NPs pairwise with the provided function and return the conjunction of the results.