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

Language | Haskell2010 |

n-ary products (and products of products)

- data NP :: (k -> *) -> [k] -> * where
- newtype POP f xss = POP (NP (NP f) xss)
- unPOP :: POP f xss -> NP (NP f) xss
- pure_NP :: forall f xs. SingI xs => (forall a. f a) -> NP f xs
- pure_POP :: forall f xss. SingI xss => (forall a. f a) -> POP f xss
- cpure_NP :: forall c xs f. (All c xs, SingI xs) => Proxy c -> (forall a. c a => f a) -> NP f xs
- cpure_POP :: forall c f xss. (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a) -> POP f xss
- fromList :: SingI xs => [a] -> Maybe (NP (K a) xs)
- ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
- ap_POP :: POP (f -.-> g) xs -> POP f xs -> POP g xs
- liftA_NP :: SingI xs => (forall a. f a -> g a) -> NP f xs -> NP g xs
- liftA_POP :: SingI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss
- liftA2_NP :: SingI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs
- liftA2_POP :: SingI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss
- 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
- 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
- cliftA_NP :: (All c xs, SingI xs) => Proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs
- cliftA_POP :: (All2 c xss, SingI xss) => Proxy c -> (forall a. c a => f a -> g a) -> POP f xss -> POP g xss
- 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
- 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
- allDict_NP :: forall c xss. (All2 c xss, SingI xss) => Proxy c -> NP (AllDict c) xss
- 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
- 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
- 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
- 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
- collapse_NP :: NP (K a) xs -> [a]
- collapse_POP :: SingI xss => POP (K a) xss -> [[a]]
- sequence'_NP :: Applicative f => NP (f :.: g) xs -> f (NP g xs)
- sequence'_POP :: (SingI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)
- sequence_NP :: (SingI xs, Applicative f) => NP f xs -> f (NP I xs)
- sequence_POP :: (SingI xss, Applicative f) => POP f xss -> f (POP I xss)

# Datatypes

data NP :: (k -> *) -> [k] -> * where Source

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 ]

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 |

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.

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 |

# Constructing products

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

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

## Construction from a list

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

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 Source

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 Source

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 Source

Specialization of `hliftA`

.

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

Specialization of `hliftA`

.

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

Specialization of `hliftA2`

.

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

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 Source

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 Source

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 Source

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 Source

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 Source

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 Source

Specialization of `hcliftA2`

.

# Dealing with `All`

c

`All`

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

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 Source

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 Source

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 Source

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 Source

Specialization of `hcliftA2'`

.

# Collapsing

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

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

Specialization of `hcollapse`

.

*Example:*

`>>>`

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

(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) Source

Specialization of `hsequence'`

.

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

Specialization of `hsequence'`

.

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

Specialization of `hsequence`

.

*Example:*

`>>>`

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

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

Specialization of `hsequence`

.

*Example:*

`>>>`

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