Data.HTree.Families

generic types and type families used in some of the modules

Documentation

type family All (c :: k -> Constraint) (xs :: [k]) where ...

for all elements of a list, a contraint holds

Equations

All (c :: k -> Constraint) ('[] :: [k]) = ()

All (c :: k -> Constraint) (x ': xs :: [k]) = (c x, All c xs)

class All c xs => AllC (c :: k -> Constraint) (xs :: [k])

like All but can be partially applied

Instances

All c xs => AllC (c :: k -> Constraint) (xs :: [k])

Defined in Data.HTree.Families

class AllInv (l :: [k -> Constraint]) (k1 :: k)

All but inversed: holds if all constraints in the list hold

Instances

AllInv ('[] :: [k1 -> Constraint]) (k2 :: k1)

Defined in Data.HTree.Families

(c k2, AllInv cs k2) => AllInv (c ': cs :: [k1 -> Constraint]) (k2 :: k1)

Defined in Data.HTree.Families

class (c1 a, c2 a) => Both (c1 :: k -> Constraint) (c2 :: k -> Constraint) (a :: k)

product of two classes

Instances

(c1 a, c2 a) => Both (c1 :: k -> Constraint) (c2 :: k -> Constraint) (a :: k)

Defined in Data.HTree.Families

type family Not (a :: Bool) :: Bool where ...

like not but on the type level

Equations

Not 'True = 'False

Not 'False = 'True

class Top (k1 :: k)

the class that every type has an instance for

Instances

Top (k2 :: k1)

Defined in Data.HTree.Families

type family (xs :: [k]) ++ (ys :: [k]) :: [k] where ... infixr 5

like 'Prelude.(++)' on the value level but on the type level

Equations

('[] :: [k]) ++ (ys :: [k]) = ys

(x ': xs :: [k]) ++ (ys :: [k]) = x ': (xs ++ ys)

type family (a :: Bool) || (b :: Bool) :: Bool where ...

typelevel Or

Equations

'True || b = 'True

'False || b = b