Safe Haskell	None
Language	Haskell2010

Generics.MRSOP.Base.NP

Description

Standard representation of n-ary products.

Synopsis

data NP (a :: k -> Type) (b :: [k]) :: forall k. (k -> Type) -> [k] -> Type where
- 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)
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 K a, 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.

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 ]

Constructors

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)
Instance details Defined in Data.SOP.NP Methods htrans :: AllZipN (Prod NP) c xs ys => proxy c -> (forall (x :: k10) (y :: k20). c x y => f x -> g y) -> NP f xs -> NP g ys # hcoerce :: (AllZipN (Prod NP) (LiftedCoercible f g) xs ys, HTrans NP NP) => NP f xs -> NP g ys #
HPure (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NP Methods hpure :: SListIN NP xs => (forall (a :: k0). f a) -> NP f xs # hcpure :: AllN NP c xs => proxy c -> (forall (a :: k0). c a => f a) -> NP f xs #
HAp (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NP Methods hap :: Prod NP (f -.-> g) xs -> NP f xs -> NP g xs #
HCollapse (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NP Methods hcollapse :: SListIN NP xs => NP (K a) xs -> CollapseTo NP a #
HTraverse_ (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NP Methods 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)
Instance details Defined in Data.SOP.NP Methods 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) #
All (Compose Eq f) xs => Eq (NP f xs)
Instance details Defined in Data.SOP.NP Methods (==) :: NP f xs -> NP f xs -> Bool # (/=) :: NP f xs -> NP f xs -> Bool #
(All (Compose Eq f) xs, All (Compose Ord f) xs) => Ord (NP f xs)
Instance details Defined in Data.SOP.NP Methods compare :: NP f xs -> NP f xs -> Ordering # (<) :: NP f xs -> NP f xs -> Bool # (<=) :: NP f xs -> NP f xs -> Bool # (>) :: NP f xs -> NP f xs -> Bool # (>=) :: NP f xs -> NP f xs -> Bool # max :: NP f xs -> NP f xs -> NP f xs # min :: NP f xs -> NP f xs -> NP f xs #
All (Compose Show f) xs => Show (NP f xs)
Instance details Defined in Data.SOP.NP Methods showsPrec :: Int -> NP f xs -> ShowS # show :: NP f xs -> String # showList :: [NP f xs] -> ShowS #
All (Compose Semigroup f) xs => Semigroup (NP f xs)	Since: sop-core-0.4.0.0
Instance details Defined in Data.SOP.NP Methods (<>) :: NP f xs -> NP f xs -> NP f xs # sconcat :: NonEmpty (NP f xs) -> NP f xs # stimes :: Integral b => b -> NP f xs -> NP f xs #
(All (Compose Monoid f) xs, All (Compose Semigroup f) xs) => Monoid (NP f xs)	Since: sop-core-0.4.0.0
Instance details Defined in Data.SOP.NP Methods mempty :: NP f xs # mappend :: NP f xs -> NP f xs -> NP f xs # mconcat :: [NP f xs] -> NP f xs #
All (Compose NFData f) xs => NFData (NP f xs)	Since: sop-core-0.2.5.0
Instance details Defined in Data.SOP.NP Methods rnf :: NP f xs -> () #
type Same (NP :: (k1 -> Type) -> [k1] -> Type)
Instance details Defined in Data.SOP.NP type Same (NP :: (k1 -> Type) -> [k1] -> Type) = (NP :: (k2 -> Type) -> [k2] -> Type)
type Prod (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NP type Prod (NP :: (k -> Type) -> [k] -> Type) = (NP :: (k -> Type) -> [k] -> Type)
type UnProd (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NS type UnProd (NP :: (k -> Type) -> [k] -> Type) = (NS :: (k -> Type) -> [k] -> Type)
type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a
Instance details Defined in Data.SOP.NP type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a = [a]
type SListIN (NP :: (k -> Type) -> [k] -> Type)
Instance details Defined in Data.SOP.NP type SListIN (NP :: (k -> Type) -> [k] -> Type) = (SListI :: [k] -> Constraint)
type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint)
Instance details Defined in Data.SOP.NP type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) = All c
type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint)
Instance details Defined in Data.SOP.NP type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) = AllZip c

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.

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.