Generics.SOP.Constraint

Constraints for indexed datatypes.

This module contains code that helps to specify that all elements of an indexed structure must satisfy a particular constraint.

Documentation

type family All c xs :: Constraint

Require a constraint for every element of a list.

If you have a datatype that is indexed over a type-level list, then you can use All to indicate that all elements of that type-level list must satisfy a given constraint.

Example: The constraint

All Eq '[ Int, Bool, Char ]

is equivalent to the constraint

(Eq Int, Eq Bool, Eq Char)

Example: A type signature such as

f :: All Eq xs => NP I xs -> ...

means that f can assume that all elements of the n-ary product satisfy Eq.

Instances

type All k c ([] k) = ()

type All k c ((:) k x xs) = (c x, All k c xs)

type family All2 c xs :: Constraint

Require a constraint for every element of a list of lists.

If you have a datatype that is indexed over a type-level list of lists, then you can use All2 to indicate that all elements of the innert lists must satisfy a given constraint.

Example: The constraint

All2 Eq '[ '[ Int ], '[ Bool, Char ] ]

is equivalent to the constraint

(Eq Int, Eq Bool, Eq Char)

Example: A type signature such as

f :: All2 Eq xss => SOP I xs -> ...

means that f can assume that all elements of the sum of product satisfy Eq.

Instances

type All2 k c ([] [k]) = ()

type All2 k c ((:) [k] x xs) = (All k c x, All2 k c xs)

type family Map f xs :: [l]

A type-level map.

Instances

type Map k k1 f ([] k1) = [] k

type Map k k1 f ((:) k1 x xs) = (:) k (f x) (Map k k1 f xs)

type family AllMap h c xs :: Constraint

A generalization of All and All2.

The family AllMap expands to All or All2 depending on whether the argument is indexed by a list or a list of lists.

Instances

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

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

data AllDict c xs where

Dictionary for a constraint for all elements of a type-level list.

A value of type AllDict c xs captures the constraint All c xs.

Constructors

AllDictC :: (SingI xs, All c xs) => AllDict c xs

Instances

Typeable ((k -> Constraint) -> [k] -> *) (AllDict k)

data Constraint :: BOX

Instances

Typeable ((* -> *) -> Constraint) Alternative

Typeable ((* -> *) -> Constraint) Applicative

Typeable (* -> Constraint) Monoid

Typeable (* -> Constraint) HasDatatypeInfo

Typeable (* -> Constraint) Generic

Typeable ((k -> Constraint) -> [k] -> *) (AllDict k)

Typeable (((k -> *) -> k -> *) -> Constraint) (HPure k k)

Typeable (((k -> *) -> k -> *) -> Constraint) (HAp k k)

Typeable (((k -> *) -> k -> *) -> Constraint) (HCollapse k k)

Typeable (((k -> *) -> k -> *) -> Constraint) (HSequence k k)