Safe Haskell | None |
---|---|
Language | Haskell2010 |
Constraints for indexed datatypes.
This module contains code that helps to specify that all elements of an indexed structure must satisfy a particular constraint.
- class (AllF f xs, SListI xs) => All f xs
- type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint
- type SListI2 = All SListI
- class (AllF (All f) xss, SListI xss) => All2 f xss
- class f (g x) => Compose f g x
- class (f x, g x) => And f g x
- class Top x
- type family AllN (h :: (k -> *) -> l -> *) (c :: k -> Constraint) :: l -> Constraint
- type family SListIN (h :: (k -> *) -> l -> *) :: l -> Constraint
- data Constraint :: *
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
.
type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint Source #
Type family used to implement All
.
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
.
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 Constraint
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
satisfy NP
f xsShow
, we can say
.All
(Show
:. f) xs
Since: 0.2
type family AllN (h :: (k -> *) -> l -> *) (c :: k -> Constraint) :: l -> Constraint Source #
type family SListIN (h :: (k -> *) -> l -> *) :: l -> Constraint Source #
data Constraint :: * #
The kind of constraints, like Show a