| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
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
- type family SListIN (h :: (k -> *) -> l -> *) :: l -> Constraint
- type family AllZipN (h :: (k -> *) -> l -> *) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint
- type family AllN (h :: (k -> *) -> l -> *) (c :: k -> Constraint) :: l -> Constraint
- class Top x
- class (f x, g x) => And f g x
- class f (g x) => Compose f g x
- class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss
- class Coercible (f x) (g y) => LiftedCoercible f g x y
- type family Tail (xs :: [a]) :: [a] where ...
- type family Head (xs :: [a]) :: a where ...
- type family SameShapeAs (xs :: [a]) (ys :: [b]) :: Constraint where ...
- type family AllZipF (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b]) :: Constraint where ...
- class (SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])
- class (AllF (All f) xss, SListI xss) => All2 f xss
- type SListI2 = All SListI
- type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...
- class (AllF f xs, SListI xs) => All (f :: k -> Constraint) (xs :: [k])
- data Constraint
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 # | |
Defined in Generics.SOP.NP | |
| type SListIN (POP :: (k -> *) -> [[k]] -> *) Source # | |
Defined in Generics.SOP.NP | |
| type SListIN (NS :: (k -> *) -> [k] -> *) Source # | |
Defined in Generics.SOP.NS | |
| type SListIN (SOP :: (k -> *) -> [[k]] -> *) Source # | |
Defined in Generics.SOP.NS | |
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 # | |
Defined in Generics.SOP.NP | |
| type AllZipN (POP :: (k -> *) -> [[k]] -> *) (c :: a -> b -> Constraint) Source # | |
Defined in Generics.SOP.NP | |
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 # | |
Defined in Generics.SOP.NP | |
| type AllN (POP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) Source # | |
Defined in Generics.SOP.NP | |
| type AllN (NS :: (k -> *) -> [k] -> *) (c :: k -> Constraint) Source # | |
Defined in Generics.SOP.NS | |
| type AllN (SOP :: (k -> *) -> [[k]] -> *) (c :: k -> Constraint) Source # | |
Defined in Generics.SOP.NS | |
A constraint that can always be satisfied.
Since: 0.2
Instances
| Top (x :: k) Source # | |
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 # | |
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 , the kind of :. gf is k -> .
The kind of Constraintg, 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 xsShow, we can say All (Show :. f) xs
Since: 0.2
Instances
| f (g x) => Compose (f :: k2 -> Constraint) (g :: k1 -> k2) (x :: k1) Source # | |
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 # | |
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 # | |
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
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 # | |
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 # | |
Defined in Generics.SOP.Constraint | |
type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where ... Source #
Type family used to implement All.
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 # | |
Defined in Generics.SOP.Constraint | |
data Constraint #
The kind of constraints, like Show a