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.

## Synopsis

- type family SListIN (h :: (k -> Type) -> l -> Type) :: l -> Constraint
- type family AllZipN (h :: (k -> Type) -> l -> Type) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint
- type family AllN (h :: (k -> Type) -> l -> Type) (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])
- type All2 c = All (All c)
- type SListI = All Top
- type SListI2 = All SListI
- type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where ...
- class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where
- cpara_SList :: proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r ys -> r (y ': ys)) -> r xs

- ccase_SList :: All c xs => proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r (y ': ys)) -> r xs
- data Constraint

# Documentation

type family SListIN (h :: (k -> Type) -> l -> Type) :: 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 (POP :: (k -> Type) -> [[k]] -> Type) Source # | |

Defined in Data.SOP.NP | |

type SListIN (SOP :: (k -> Type) -> [[k]] -> Type) Source # | |

Defined in Data.SOP.NS | |

type SListIN (NP :: (k -> Type) -> [k] -> Type) Source # | |

Defined in Data.SOP.NP | |

type SListIN (NS :: (k -> Type) -> [k] -> Type) Source # | |

Defined in Data.SOP.NS |

type family AllZipN (h :: (k -> Type) -> l -> Type) (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 (POP :: (k -> Type) -> [[k]] -> Type) (c :: a -> b -> Constraint) Source # | |

Defined in Data.SOP.NP | |

type AllZipN (NP :: (k -> Type) -> [k] -> Type) (c :: a -> b -> Constraint) Source # | |

Defined in Data.SOP.NP |

type family AllN (h :: (k -> Type) -> l -> Type) (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 (POP :: (k -> Type) -> [[k]] -> Type) (c :: k -> Constraint) Source # | |

Defined in Data.SOP.NP | |

type AllN (SOP :: (k -> Type) -> [[k]] -> Type) (c :: k -> Constraint) Source # | |

Defined in Data.SOP.NS | |

type AllN (NP :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) Source # | |

Defined in Data.SOP.NP | |

type AllN (NS :: (k -> Type) -> [k] -> Type) (c :: k -> Constraint) Source # | |

Defined in Data.SOP.NS |

A constraint that can always be satisfied.

*Since: 0.2*

## Instances

Top (x :: k) Source # | |

Defined in Data.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 Data.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

, the kind of `Compose`

f g`f`

is `k -> `

.
The kind of `Constraint`

`g`

, however, is `l -> k`

and can thus be a 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`

(`Compose`

`Show`

f) xs

*Since: 0.2*

## Instances

f (g x) => Compose (f :: k2 -> Constraint) (g :: k1 -> k2) (x :: k1) Source # | |

Defined in Data.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 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 Data.SOP.Constraint |

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

The constraint

is equivalent
to `LiftedCoercible`

f g x y

.`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 Data.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*

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*

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.

Since 0.5.0.0, this only tests the top-level structure of
the list, and is intended to be used in conjunction with
a separate construct (such as the `AllZip`

, `AllZipF`

combination to tie the recursive knot). The reason is that
making `SameShapeAs`

directly recursive leads to quadratic
compile times.

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

*Since: 0.5.0.0*

SameShapeAs '[] ys = ys ~ '[] | |

SameShapeAs (x ': xs) ys = ys ~ (Head ys ': 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 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 Data.SOP.Constraint |

type All2 c = All (All c) 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 inner 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`

.

Since 0.4.0.0, this is merely a synonym for 'All (All c)'.

*Since: 0.4.0.0*

type SListI = All Top Source #

Implicit singleton list.

A singleton list can be used to reveal the structure of a type-level list argument that the function is quantified over.

Since 0.4.0.0, this is now defined in terms of `All`

.
A singleton list provides a witness for a type-level list
where the elements need not satisfy any additional
constraints.

*Since: 0.4.0.0*

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

Type family used to implement `All`

.

class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where 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`

.

Note on superclasses: ghc cannot deduce superclasses from `All`

constraints.
You might expect the following to compile

class (Eq a) => MyClass a foo :: (All Eq xs) => NP f xs -> z foo = [..] bar :: (All MyClass xs) => NP f xs -> x bar = foo

but it will fail with an error saying that it was unable to
deduce the class constraint

(or similar) in the
definition of `AllF`

`Eq`

xs`bar`

.
In cases like this you can use `Dict`

from Data.SOP.Dict
to prove conversions between constraints.
See this answer on SO for more details.

cpara_SList :: proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r ys -> r (y ': ys)) -> r xs Source #

Constrained paramorphism for a type-level list.

The advantage of writing functions in terms of `cpara_SList`

is that
they are then typically not recursive, and can be unfolded statically if
the type-level list is statically known.

*Since: 0.4.0.0*

## Instances

All (c :: k -> Constraint) ([] :: [k]) Source # | |

Defined in Data.SOP.Constraint cpara_SList :: proxy c -> r [] -> (forall (y :: k0) (ys :: [k0]). (c y, All c ys) => r ys -> r (y ': ys)) -> r [] Source # | |

(c x, All c xs) => All (c :: a -> Constraint) (x ': xs :: [a]) Source # | |

Defined in Data.SOP.Constraint cpara_SList :: proxy c -> r [] -> (forall (y :: k) (ys :: [k]). (c y, All c ys) => r ys -> r (y ': ys)) -> r (x ': xs) Source # |

ccase_SList :: All c xs => proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r (y ': ys)) -> r xs Source #

Constrained case distinction on a type-level list.

*Since: 0.4.0.0*

data Constraint #

The kind of constraints, like `Show a`