Safe Haskell	Safe
Language	Haskell2010

Generics.MRSOP.Base.NP

Contents

Description

Standard representation of n-ary products.

Synopsis

data NP :: (k -> *) -> [k] -> * where
- NP0 :: NP p '[]
- (:*) :: p x -> NP p xs -> NP p (x ': xs)
appendNP :: NP p xs -> NP p ys -> NP p (xs :++: ys)
listPrfNP :: NP p xs -> ListPrf xs
mapNP :: (f :-> g) -> NP f ks -> NP g ks
mapNPM :: Monad m => (forall x. f x -> m (g x)) -> NP f ks -> m (NP g ks)
elimNP :: (forall x. f x -> a) -> NP f ks -> [a]
elimNPM :: Monad m => (forall x. f x -> m a) -> NP f ks -> m [a]
zipNP :: NP f xs -> NP g xs -> NP (f :*: g) xs
unzipNP :: NP (f :*: g) xs -> (NP f xs, NP g xs)
cataNP :: (forall a as. f a -> r as -> r (a ': as)) -> r '[] -> NP f xs -> r xs
cataNPM :: Monad m => (forall a as. f a -> r as -> m (r (a ': as))) -> m (r '[]) -> NP f xs -> m (r xs)
eqNP :: (forall x. p x -> p x -> Bool) -> NP p xs -> NP p xs -> Bool

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

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.

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

Unzips a combined product into two separate products

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.

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.