Safe Haskell	Safe
Language	Haskell2010

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

Show (NP [Atom kon] (ConstructorInfo kon) code) #
Methods showsPrec :: Int -> NP [Atom kon] (ConstructorInfo kon) code -> ShowS # show :: NP [Atom kon] (ConstructorInfo kon) code -> String # showList :: [NP [Atom kon] (ConstructorInfo kon) code] -> ShowS #
Show (NP (Atom kon) (FieldInfo kon) code) #
Methods showsPrec :: Int -> NP (Atom kon) (FieldInfo kon) code -> ShowS # show :: NP (Atom kon) (FieldInfo kon) code -> String # showList :: [NP (Atom kon) (FieldInfo kon) code] -> ShowS #

Relation to IsList predicate

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

Append two values of type NP

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.

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.

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

Consumes a value of type NP.

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.