Generics.SOP.NP

n-ary products (and products of products)

Datatypes

data NP :: (k -> *) -> [k] -> * 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 :: NP f []

(:*) :: f x -> NP f xs -> NP f (x : xs) infixr 5

Instances

HSequence k [k] (NP k)

HCollapse k [k] (NP k)

HAp k [k] (NP k)

HPure k [k] (NP k)

All * Eq (Map * k f xs) => Eq (NP k f xs)

(All * Eq (Map * k f xs), All * Ord (Map * k f xs)) => Ord (NP k f xs)

All * Show (Map * k f xs) => Show (NP k f xs)

type CollapseTo k [k] (NP k) = []

type Prod k [k] (NP k) = NP k

type AllMap k [k] (NP k) c xs = All k c xs

newtype POP f xss

A product of products.

This is a 'newtype' for an NP of an NP. The elements of the inner products are applications of the parameter f. The type POP is indexed by the list of lists that determines the lengths of both the outer and all the inner products, as well as the types of all the elements of the inner products.

A POP is reminiscent of a two-dimensional table (but the inner lists can all be of different length). In the context of the SOP approach to generic programming, a POP is useful to represent information that is available for all arguments of all constructors of a datatype.

Constructors

POP (NP (NP f) xss)

Instances

HSequence k [[k]] (POP k)

HCollapse k [[k]] (POP k)

HAp k [[k]] (POP k)

HPure k [[k]] (POP k)

All * Eq (Map * [k] (NP k f) xss) => Eq (POP k f xss)

(All * Eq (Map * [k] (NP k f) xss), All * Ord (Map * [k] (NP k f) xss)) => Ord (POP k f xss)

All * Show (Map * [k] (NP k f) xss) => Show (POP k f xss)

type CollapseTo k [[k]] (POP k) = (:.:) * * [] []

type Prod k [[k]] (POP k) = POP k

type AllMap k [[k]] (POP k) c xs = All2 k c xs

unPOP :: POP f xss -> NP (NP f) xss

Unwrap a product of products.

Constructing products

pure_NP :: forall f xs. SingI xs => (forall a. f a) -> NP f xs

Specialization of hpure.

The call pure_NP x generates a product that contains x in every element position.

Example:

>>> pure_NP [] :: NP [] '[Char, Bool]
> "" :* [] :* Nil
>>> pure_NP (K 0) :: NP (K Int) '[Double, Int, String]
> K 0 :* K 0 :* K 0 :* Nil

pure_POP :: forall f xss. SingI xss => (forall a. f a) -> POP f xss

Specialization of hpure.

The call pure_POP x generates a product of products that contains x in every element position.

cpure_NP :: forall c xs f. (All c xs, SingI xs) => Proxy c -> (forall a. c a => f a) -> NP f xs

Specialization of hcpure.

The call cpure_NP p x generates a product that contains x in every element position.

cpure_POP :: forall c f xss. (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a) -> POP f xss

Specialization of hcpure.

The call cpure_NP p x generates a product of products that contains x in every element position.

Construction from a list

fromList :: SingI xs => [a] -> Maybe (NP (K a) xs)

Construct a homogeneous n-ary product from a normal Haskell list.

Returns Nothing if the length of the list does not exactly match the expected size of the product.

Application

ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs

Specialization of hap.

Applies a product of (lifted) functions pointwise to a product of suitable arguments.

ap_POP :: POP (f -.-> g) xs -> POP f xs -> POP g xs

Specialization of hap.

Applies a product of (lifted) functions pointwise to a product of suitable arguments.

Lifting / mapping

liftA_NP :: SingI xs => (forall a. f a -> g a) -> NP f xs -> NP g xs

Specialization of hliftA.

liftA_POP :: SingI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss

Specialization of hliftA.

liftA2_NP :: SingI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

Specialization of hliftA2.

liftA2_POP :: SingI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

Specialization of hliftA2.

liftA3_NP :: SingI xs => (forall a. f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs

Specialization of hliftA3.

liftA3_POP :: SingI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

Specialization of hliftA3.

cliftA_NP :: (All c xs, SingI xs) => Proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs

Specialization of hcliftA.

cliftA_POP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a) -> POP f xss -> POP g xss

Specialization of hcliftA.

cliftA2_NP :: (All c xs, SingI xs) => Proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

Specialization of hcliftA2.

cliftA2_POP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

Specialization of hcliftA2.

Dealing with All c

allDict_NP :: forall c xss. (All2 c xss, SingI xss) => Proxy c -> NP (AllDict c) xss

Construct a product of dictionaries for a type-level list of lists.

The structure of the product matches the outer list, the dictionaries contained are AllDict-dictionaries for the inner list.

hcliftA' :: (All2 c xss, SingI xss, Prod h ~ NP, HAp h) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs) -> h f xss -> h f' xss

Lift a constrained function operating on a list-indexed structure to a function on a list-of-list-indexed structure.

This is a variant of hcliftA.

Specification:

hcliftA' p f xs = hpure (fn_2 $ \ AllDictC -> f) ` hap ` allDict_NP p ` hap ` xs

Instances:

hcliftA' :: (All2 c xss, SingI xss) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs) -> NP f xss -> NP f' xss
hcliftA' :: (All2 c xss, SingI xss) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs) -> NS f xss -> NS f' xss

hcliftA2' :: (All2 c xss, SingI xss, Prod h ~ NP, HAp h) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs -> f'' xs) -> Prod h f xss -> h f' xss -> h f'' xss

Like hcliftA', but for binary functions.

hcliftA3' :: (All2 c xss, SingI xss, Prod h ~ NP, HAp h) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss

Like hcliftA', but for ternay functions.

cliftA2'_NP :: (All2 c xss, SingI xss) => Proxy c -> (forall xs. (SingI xs, All c xs) => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss

Specialization of hcliftA2'.

Collapsing

collapse_NP :: NP (K a) xs -> [a]

Specialization of hcollapse.

Example:

>>> collapse_NP (K 1 :* K 2 :* K 3 :* Nil)
> [1,2,3]

collapse_POP :: SingI xss => POP (K a) xss -> [[a]]

Specialization of hcollapse.

Example:

>>> collapse_POP (POP ((K 'a' :* Nil) :* (K 'b' :* K 'c' :* Nil) :* Nil) :: POP (K Char) '[ '[(a :: *)], '[b, c] ])
> ["a", "bc"]

(The type signature is only necessary in this case to fix the kind of the type variables.)

Sequencing

sequence'_NP :: Applicative f => NP (f :.: g) xs -> f (NP g xs)

Specialization of hsequence'.

sequence'_POP :: (SingI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)

Specialization of hsequence'.

sequence_NP :: (SingI xs, Applicative f) => NP f xs -> f (NP I xs)

Specialization of hsequence.

Example:

>>> sequence_NP (Just 1 :* Just 2 :* Nil)
> Just (I 1 :* I 2 :* Nil)

sequence_POP :: (SingI xss, Applicative f) => POP f xss -> f (POP I xss)

Specialization of hsequence.

Example:

>>> sequence_POP (POP ((Just 1 :* Nil) :* (Just 2 :* Just 3 :* Nil) :* Nil))
> Just (POP ((I 1 :* Nil) :* ((I 2 :* (I 3 :* Nil)) :* Nil)))