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

Defined in Generics.SOP.NP

type SListIN (NP :: (k -> *) -> [k] -> *) = (SListI :: [k] -> Constraint)

type SListIN (POP :: (k -> *) -> [[k]] -> *)

Defined in Generics.SOP.NP

type SListIN (POP :: (k -> *) -> [[k]] -> *) = (SListI2 :: [[k]] -> Constraint)

type SListIN (NS :: (k -> *) -> [k] -> *)

Defined in Generics.SOP.NS

type SListIN (NS :: (k -> *) -> [k] -> *) = (SListI :: [k] -> Constraint)

type SListIN (SOP :: (k -> *) -> [[k]] -> *)

Defined in Generics.SOP.NS

type SListIN (SOP :: (k -> *) -> [[k]] -> *) = (SListI2 :: [[k]] -> Constraint)

type family AllZipN (h :: (k -> *) -> l -> *) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint

A generalization of AllZip and AllZip2.

The family AllZipN expands to AllZip or AllZip2 depending on whther the argument is indexed by a list or a list of lists.

Instances

type AllZipN (NP :: (k -> *) -> [k] -> *) (c :: a -> b -> Constraint)

Defined in Generics.SOP.NP

type AllZipN (NP :: (k -> *) -> [k] -> *) (c :: a -> b -> Constraint) = AllZip c

type AllZipN (POP :: (k -> *) -> [[k]] -> *) (c :: a -> b -> Constraint)

Defined in Generics.SOP.NP

type AllZipN (POP :: (k -> *) -> [[k]] -> *) (c :: a -> b -> Constraint) = AllZip2 c

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

Defined in Generics.SOP.NP

type AllN (NP :: (k -> *) -> [k] -> *) (c :: k -> Constraint) = All c

type AllN (POP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint)

Defined in Generics.SOP.NP

type AllN (POP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) = All2 c

type AllN (NS :: (k -> *) -> [k] -> *) (c :: k -> Constraint)

Defined in Generics.SOP.NS

type AllN (NS :: (k -> *) -> [k] -> *) (c :: k -> Constraint) = All c

type AllN (SOP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint)

Defined in Generics.SOP.NS

type AllN (SOP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) = All2 c

class Top x

A constraint that can always be satisfied.

Since: 0.2

Instances

Top (x :: k)

Defined in Generics.SOP.Constraint

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

Pairing of constraints.

Since: 0.2

Instances

(f x, g x) => And (f :: k -> Constraint) (g :: k -> Constraint) (x :: k)

Defined in Generics.SOP.Constraint

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 (f :: k2 -> Constraint) (g :: k1 -> k2) (x :: k1)

Defined in Generics.SOP.Constraint

class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss

Require a constraint for pointwise for every pair of elements from two lists of lists.

Instances

(AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 (f :: a -> b -> Constraint) (xss :: [[a]]) (yss :: [[b]])

Defined in Generics.SOP.Constraint

class Coercible (f x) (g y) => LiftedCoercible f g x y

The constraint LiftedCoercible f g x y is equivalent to Coercible (f x) (g y).

Since: 0.3.1.0

Instances

Coercible (f x) (g y) => LiftedCoercible (f :: k2 -> k0) (g :: k1 -> k0) (x :: k2) (y :: k1)

Defined in Generics.SOP.Constraint

type family Tail (xs :: [a]) :: [a] where ...

Utility function to compute the tail of a type-level list.

Since: 0.3.1.0

Equations

Tail (x ': xs) = xs

type family Head (xs :: [a]) :: a where ...

Utility function to compute the head of a type-level list.

Since: 0.3.1.0

Equations

Head (x ': xs) = x

type family SameShapeAs (xs :: [a]) (ys :: [b]) :: Constraint where ...

Type family that forces a type-level list to be of the same shape as the given type-level list.

The main use of this constraint is to help type inference to learn something about otherwise unknown type-level lists.

Since: 0.3.1.0

Equations

SameShapeAs '[] ys = ys ~ '[]

SameShapeAs (x ': xs) ys = (ys ~ (Head ys ': Tail ys), SameShapeAs xs (Tail ys))

type family AllZipF (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b]) :: Constraint where ...

Type family used to implement AllZip.

Since: 0.3.1.0

Equations

AllZipF _c '[] '[] = ()

AllZipF c (x ': xs) (y ': ys) = (c x y, AllZip c xs ys)

class (SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])

Require a constraint for pointwise for every pair of elements from two lists.

Example: The constraint

All (~) '[ Int, Bool, Char ] '[ a, b, c ]

is equivalent to the constraint

(Int ~ a, Bool ~ b, Char ~ c)

Since: 0.3.1.0

Instances

(SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])

Defined in Generics.SOP.Constraint

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 (All f) xss, SListI xss) => All2 (f :: k -> Constraint) (xss :: [[k]])

Defined in Generics.SOP.Constraint

type SListI2 = All SListI

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

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

Type family used to implement All.

Equations

AllF _c '[] = ()

AllF c (x ': xs) = (c x, All c xs)

class (AllF f xs, SListI xs) => All (f :: k -> Constraint) (xs :: [k])

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 f xs, SListI xs) => All (f :: k -> Constraint) (xs :: [k])

Defined in Generics.SOP.Constraint

data Constraint

The kind of constraints, like Show a

Orphan instances

SListI xs => SingI (xs :: [k])

Methods

sing :: Sing xs

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

Methods

sing :: Sing xss