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 `:.`

g`f`

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 xs`Show`

, 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`