Safe Haskell | None |
---|---|
Language | Haskell2010 |
Standard representation of n-ary products.
Synopsis
- data NP (a :: k -> Type) (b :: [k]) :: forall k. (k -> Type) -> [k] -> Type 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
- 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 (a :: k -> Type) (b :: [k]) :: forall k. (k -> Type) -> [k] -> Type where #
An n-ary product.
The product is parameterized by a type constructor f
and
indexed by a type-level list xs
. The length of the list
determines the number of elements in the product, and if the
i
-th element of the list is of type x
, then the i
-th
element of the product is of type f x
.
The constructor names are chosen to resemble the names of the list constructors.
Two common instantiations of f
are the identity functor I
and the constant functor K
. For I
, the product becomes a
heterogeneous list, where the type-level list describes the
types of its components. For
, the product becomes a
homogeneous list, where the contents of the type-level list are
ignored, but its length still specifies the number of elements.K
a
In the context of the SOP approach to generic programming, an n-ary product describes the structure of the arguments of a single data constructor.
Examples:
I 'x' :* I True :* Nil :: NP I '[ Char, Bool ] K 0 :* K 1 :* Nil :: NP (K Int) '[ Char, Bool ] Just 'x' :* Nothing :* Nil :: NP Maybe '[ Char, Bool ]
Nil :: forall k (a :: k -> Type) (b :: [k]). NP a ([] :: [k]) | |
(:*) :: forall k (a :: k -> Type) (b :: [k]) (x :: k) (xs :: [k]). a x -> NP a xs -> NP a (x ': xs) infixr 5 |
Instances
HTrans (NP :: (k1 -> Type) -> [k1] -> Type) (NP :: (k2 -> Type) -> [k2] -> Type) | |
HPure (NP :: (k -> Type) -> [k] -> Type) | |
HAp (NP :: (k -> Type) -> [k] -> Type) | |
HCollapse (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP | |
HTraverse_ (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP hctraverse_ :: (AllN NP c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g ()) -> NP f xs -> g () # htraverse_ :: (SListIN NP xs, Applicative g) => (forall (a :: k0). f a -> g ()) -> NP f xs -> g () # | |
HSequence (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP hsequence' :: (SListIN NP xs, Applicative f) => NP (f :.: g) xs -> f (NP g xs) # hctraverse' :: (AllN NP c xs, Applicative g) => proxy c -> (forall (a :: k0). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) # htraverse' :: (SListIN NP xs, Applicative g) => (forall (a :: k0). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) # | |
ShowHO f => ShowHO (NP f :: [k] -> Type) Source # | Since: 2.3.0 |
EqHO f => EqHO (NP f :: [k] -> Type) Source # | Since: 2.3.0 |
All (Compose Eq f) xs => Eq (NP f xs) | |
(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NP f xs) | |
All (Compose Show f) xs => Show (NP f xs) | |
All (Compose Semigroup f) xs => Semigroup (NP f xs) | Since: sop-core-0.4.0.0 |
(All (Compose Monoid f) xs, All (Compose Semigroup f) xs) => Monoid (NP f xs) | Since: sop-core-0.4.0.0 |
All (Compose NFData f) xs => NFData (NP f xs) | Since: sop-core-0.2.5.0 |
Defined in Data.SOP.NP | |
type Same (NP :: (k1 -> Type) -> [k1] -> Type) | |
type Prod (NP :: (k -> Type) -> [k] -> Type) | |
type UnProd (NP :: (k -> Type) -> [k] -> Type) | |
type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a | |
Defined in Data.SOP.NP | |
type SListIN (NP :: (k -> Type) -> [k] -> Type) | |
Defined in Data.SOP.NP | |
type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) | |
Defined in Data.SOP.NP | |
type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) | |
Defined in Data.SOP.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.
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.
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 NP
s pairwise with the provided function and
return the conjunction of the results.