Data.HSet.TypeLevel

Documentation

data Nat

Constructors

Z

S Nat

type family Elem typ typs :: Bool

Calculates to 'True if first type argument contained in second list element

Equations

Elem typ [] = False

Elem typ (typ : typs) = True

Elem typ1 (typ2 : typs) = Elem typ1 typs

type family Index typ typs :: Nat

Calculates to Nat kinded type describing the index of first argument in second argument

Equations

Index t (t : ts) = Z

Index t (tt : ts) = S (Index t ts)

type family TEq t1 t2 :: Bool

Equations

TEq a a = True

TEq a b = False

type family Length list :: Nat

Type level list length

Equations

Length [] = Z

Length (x : xs) = S (Length xs)

type family Append l1 l2 :: [*]

Equations

Append [] x = x

Append x [] = x

Append (x : xs) ys = x : Append xs ys

type family Delete typ typs :: [*]

Delete element from type list

Equations

Delete x [] = []

Delete x (x : ys) = Delete x ys

Delete x (y : ys) = y : Delete x ys

type family FirstEQ list1 list2 :: Bool

First elements of two lists are equal?

Equations

FirstEQ [] [] = False

FirstEQ [] x = False

FirstEQ x [] = False

FirstEQ (x : xs) (x : ys) = True

FirstEQ (x : xs) (y : ys) = False

type family FirstContains list1 list2 :: Bool

Equations

FirstContains [] x = False

FirstContains x [] = False

FirstContains (x : xs) els = Elem x els

type family And a b

Equations

And False x = False

And x False = False

And x y = True

type family HSubset h1 h2

Checks if the former subset included in the latter one.

Equations

HSubset [] x = True

HSubset x [] = False

HSubset (h1 : tl2) h2 = And (Elem h1 h2) (HSubset tl2 h2)