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

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

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

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

Type family used to implement All.

Instances

type AllF k _c ([] k)

type AllF k _c ([] k) = ()

type AllF k c ((:) k x xs)

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

type SListI2 = All SListI

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

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

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

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

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

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

Pairing of constraints.

Since: 0.2

Instances

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

class Top x

A constraint that can always be satisfied.

Since: 0.2

Instances

Top k x

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

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

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

type AllN [k] k (NP k) c

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

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

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)

type SListIN [[k]] k (POP k) = SListI2 k

type SListIN [[k]] k (SOP k)

type SListIN [[k]] k (SOP k) = SListI2 k

type SListIN [k] k (NP k)

type SListIN [k] k (NP k) = SListI k

type SListIN [k] k (NS k)

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

Methods

sing :: Sing xs xs

(All [k] (SListI k) xss, SListI [k] xss) => SingI [k] xss

Methods

sing :: Sing xss xs