generics-sop-0.2.5.0: Generic Programming using True Sums of Products

Generics.SOP.Constraint

Contents

Description

Constraints for indexed datatypes.

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

Synopsis

# Documentation

class (AllF f xs, SListI xs) => All f xs Source #

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

 (AllF k f xs, SListI k xs) => All k f xs Source #

type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint Source #

Type family used to implement All.

Instances

 type AllF k _c ([] k) Source # type AllF k _c ([] k) = () type AllF k c ((:) k x xs) Source # type AllF k c ((:) k x xs) = (c x, All k c xs)

Require a singleton for every inner list in a list of lists.

class (AllF (All f) xss, SListI xss) => All2 f xss Source #

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

 (AllF [k] (All k f) xss, SListI [k] xss) => All2 k f xss Source #

class f (g x) => Compose f g x infixr 9 Source #

Composition of constraints.

Note that the result of the composition must be a constraint, and therefore, in f :. g, the kind of f is k -> Constraint. The kind of g, however, is l -> k and can thus be an normal type constructor.

A typical use case is in connection with All on an NP or an NS. For example, in order to denote that all elements on an NP f xs satisfy Show, we can say All (Show :. f) xs.

Since: 0.2

Instances

 f (g x) => Compose k k1 f g x Source #

class (f x, g x) => And f g x infixl 7 Source #

Pairing of constraints.

Since: 0.2

Instances

 (f x, g x) => And k f g x Source #

class Top x Source #

A constraint that can always be satisfied.

Since: 0.2

Instances

 Top k x Source #

type family AllN (h :: (k -> *) -> l -> *) (c :: k -> Constraint) :: l -> Constraint Source #

A generalization of All and All2.

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

Instances

 type AllN [[k]] k (POP k) c Source # type AllN [[k]] k (POP k) c = All2 k c type AllN [k] k (NP k) c Source # type AllN [k] k (NP k) c = All k c

type family SListIN (h :: (k -> *) -> l -> *) :: l -> Constraint Source #

A generalization of SListI.

The family SListIN expands to SListI or SListI2 depending on whether the argument is indexed by a list or a list of lists.

Instances

 type SListIN [[k]] k (POP k) Source # type SListIN [[k]] k (POP k) = SListI2 k type SListIN [[k]] k (SOP k) Source # type SListIN [[k]] k (SOP k) = SListI2 k type SListIN [k] k (NP k) Source # type SListIN [k] k (NP k) = SListI k type SListIN [k] k (NS k) Source # type SListIN [k] k (NS k) = SListI k

data Constraint :: * #

The kind of constraints, like Show a

# Orphan instances

 SListI k xs => SingI k xs Source # Methodssing :: Sing xs xs Source # (All [k] (SListI k) xss, SListI [k] xss) => SingI [k] xss Source # Methodssing :: Sing xss xs Source #