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

Safe HaskellNone
LanguageHaskell2010

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

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

Defined in Generics.SOP.NP

type SListIN (NP :: (k -> *) -> [k] -> *) = (SListI :: [k] -> Constraint)
type SListIN (POP :: (k -> *) -> [[k]] -> *) Source # 
Instance details

Defined in Generics.SOP.NP

type SListIN (POP :: (k -> *) -> [[k]] -> *) = (SListI2 :: [[k]] -> Constraint)
type SListIN (NS :: (k -> *) -> [k] -> *) Source # 
Instance details

Defined in Generics.SOP.NS

type SListIN (NS :: (k -> *) -> [k] -> *) = (SListI :: [k] -> Constraint)
type SListIN (SOP :: (k -> *) -> [[k]] -> *) Source # 
Instance details

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 Source #

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) Source # 
Instance details

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) Source # 
Instance details

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

Defined in Generics.SOP.NP

type AllN (NP :: (k -> *) -> [k] -> *) (c :: k -> Constraint) = All c
type AllN (POP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) Source # 
Instance details

Defined in Generics.SOP.NP

type AllN (POP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) = All2 c
type AllN (NS :: (k -> *) -> [k] -> *) (c :: k -> Constraint) Source # 
Instance details

Defined in Generics.SOP.NS

type AllN (NS :: (k -> *) -> [k] -> *) (c :: k -> Constraint) = All c
type AllN (SOP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) Source # 
Instance details

Defined in Generics.SOP.NS

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

class Top x Source #

A constraint that can always be satisfied.

Since: 0.2

Instances
Top (x :: k) Source # 
Instance details

Defined in Generics.SOP.Constraint

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

Pairing of constraints.

Since: 0.2

Instances
(f x, g x) => And (f :: k -> Constraint) (g :: k -> Constraint) (x :: k) Source # 
Instance details

Defined in Generics.SOP.Constraint

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

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 Source #

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]]) Source # 
Instance details

Defined in Generics.SOP.Constraint

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

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) Source # 
Instance details

Defined in Generics.SOP.Constraint

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

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 ... Source #

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 ... Source #

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 ... Source #

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]) Source #

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]) Source # 
Instance details

Defined in Generics.SOP.Constraint

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

Defined in Generics.SOP.Constraint

type SListI2 = All SListI Source #

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

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

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

Defined in Generics.SOP.Constraint

data Constraint #

The kind of constraints, like Show a

Orphan instances

SListI xs => SingI (xs :: [k]) Source # 
Instance details

Methods

sing :: Sing xs Source #

(All (SListI :: [k] -> Constraint) xss, SListI xss) => SingI (xss :: [[k]]) Source # 
Instance details

Methods

sing :: Sing xss Source #