Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

Standard representation of n-ary products.

- data NP :: (k -> *) -> [k] -> * where
- 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
- cataNP :: (forall x xs. f x -> r xs -> r (x ': xs)) -> r '[] -> NP f xs -> 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.

# Relation to IsList predicate

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

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.

# Catamorphism

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

Consumes a value of type `NP`

.