generics-mrsop-2.1.0: 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 Source #

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
ShowHO phi => ShowHO (NP phi :: [k] -> Type) Source # 
Instance details

Defined in Generics.MRSOP.Base.NP

Methods

showHO :: NP phi k0 -> String Source #

EqHO phi => EqHO (NP phi :: [k] -> Type) Source # 
Instance details

Defined in Generics.MRSOP.Base.NP

Methods

eqHO :: NP phi k0 -> NP phi k0 -> Bool Source #

EqHO phi => Eq (NP phi xs) Source # 
Instance details

Defined in Generics.MRSOP.Base.NP

Methods

(==) :: NP phi xs -> NP phi xs -> Bool #

(/=) :: NP phi xs -> NP phi xs -> Bool #

ShowHO phi => Show (NP phi xs) Source # 
Instance details

Defined in Generics.MRSOP.Base.NP

Methods

showsPrec :: Int -> NP phi xs -> ShowS #

show :: NP phi xs -> String #

showList :: [NP phi xs] -> ShowS #

Relation to IsList predicate

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

Append two values of type NP

listPrfNP :: NP p xs -> ListPrf xs Source #

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

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

Maps a monadic natural transformation over a n-ary product

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

Eliminates the product using a provided function.

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

Monadic eliminator

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

Combines two products into one.

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

Unzips a combined product into two separate products

Catamorphism

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

Consumes a value of type NP.

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

Consumes a value of type NP.

Equality

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

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