Safe Haskell	None
Language	Haskell2010

Data.SOP.Constraint

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

Instances details

type SListIN ( NP :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Data.SOP.NP type SListIN ( NP :: (k -> Type ) -> [k] -> Type ) = SListI :: [k] -> Constraint
type SListIN ( POP :: (k -> Type ) -> [[k]] -> Type ) Source #
Instance details Defined in Data.SOP.NP type SListIN ( POP :: (k -> Type ) -> [[k]] -> Type ) = SListI2 :: [[k]] -> Constraint
type SListIN ( NS :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Data.SOP.NS type SListIN ( NS :: (k -> Type ) -> [k] -> Type ) = SListI :: [k] -> Constraint
type SListIN ( SOP :: (k -> Type ) -> [[k]] -> Type ) Source #
Instance details Defined in Data.SOP.NS type SListIN ( SOP :: (k -> Type ) -> [[k]] -> Type ) = SListI2 :: [[k]] -> Constraint

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

Instances details

type AllZipN ( NP :: (k -> Type ) -> [k] -> Type ) (c :: a -> b -> Constraint ) Source #
Instance details Defined in Data.SOP.NP type AllZipN ( NP :: (k -> Type ) -> [k] -> Type ) (c :: a -> b -> Constraint ) = AllZip c
type AllZipN ( POP :: (k -> Type ) -> [[k]] -> Type ) (c :: a -> b -> Constraint ) Source #
Instance details Defined in Data.SOP.NP type AllZipN ( POP :: (k -> Type ) -> [[k]] -> Type ) (c :: a -> b -> Constraint ) = AllZip2 c

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

Instances details

type AllN ( NP :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Data.SOP.NP type AllN ( NP :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) = All c
type AllN ( POP :: (k -> Type ) -> [[k]] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Data.SOP.NP type AllN ( POP :: (k -> Type ) -> [[k]] -> Type ) (c :: k -> Constraint ) = All2 c
type AllN ( NS :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Data.SOP.NS type AllN ( NS :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) = All c
type AllN ( SOP :: (k -> Type ) -> [[k]] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Data.SOP.NS type AllN ( SOP :: (k -> Type ) -> [[k]] -> Type ) (c :: k -> Constraint ) = All2 c

class Top x Source #

A constraint that can always be satisfied.

Since: 0.2

Instances

Instances details

Top (x :: k) Source #
Instance details Defined in Data.SOP.Constraint

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

Pairing of constraints.

Since: 0.2

Instances

Instances details

(f x, g x) => And (f :: k -> Constraint ) (g :: k -> Constraint ) (x :: k) Source #
Instance details 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 Compose f g , the kind of f is k -> Constraint . The kind of 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 NP f xs satisfy Show , we can say All ( Compose Show f) xs .

Since: 0.2

Instances

Instances details

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

Instances details

( 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 Data.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

Instances details

Coercible (f x) (g y) => LiftedCoercible (f :: k1 -> k2) (g :: k3 -> k2) (x :: k1) (y :: k3) Source #
Instance details 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

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.

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

Equations

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

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 pointwise for every pair of elements from two lists.

Example: The constraint

AllZip (~) '[ Int, Bool, Char ] '[ a, b, c ]

is equivalent to the constraint

(Int ~ a, Bool ~ b, Char ~ c)

Since: 0.3.1.0

Instances

Instances details

( 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 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 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 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 AllF Eq xs (or similar) in the definition of 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 .

Methods

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

Instances details

All (c :: k -> Constraint ) ('[] :: [k]) Source #
Instance details Defined in Data.SOP.Constraint Methods 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 #
Instance details Defined in Data.SOP.Constraint Methods 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 Source #

The kind of constraints, like Show a