module Data.HSet.TypeLevel
( Nat(..)
, Elem
, Index
, TEq
, Length
, Append
, Delete
, FirstEQ
, FirstContains
, And
, HSubset
) where
data Nat = Z | S Nat
type family Elem (typ :: k) (typs :: [k]) :: Bool where
Elem typ '[] = 'False
Elem typ (typ ': typs) = 'True
Elem typ1 (typ2 ': typs) = Elem typ1 typs
type family Index (typ :: k) (typs :: [k]) :: Nat where
Index t (t ': ts) = 'Z
Index t (tt ': ts) = 'S (Index t ts)
type family TEq (t1 :: k) (t2 :: k) :: Bool where
TEq a a = 'True
TEq a b = 'False
type family Length (list :: [*]) :: Nat where
Length '[] = 'Z
Length (x ': xs) = 'S (Length xs)
type family Append (l1 :: [*]) (l2 :: [*]) :: [*] where
Append '[] x = x
Append x '[] = x
Append (x ': xs) ys = x ': (Append xs ys)
type family Delete (typ :: *) (typs :: [*]) :: [*] where
Delete x '[] = '[]
Delete x (x ': ys) = Delete x ys
Delete x (y ': ys) = y ': (Delete x ys)
type family FirstEQ (list1 :: [*]) (list2 :: [*]) :: Bool where
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 where
FirstContains '[] x = 'False
FirstContains x '[] = 'False
FirstContains (x ': xs) els = Elem x els
type family And (a :: Bool) (b :: Bool) where
And 'False x = 'False
And x 'False = 'False
And x y = 'True
type family HSubset (h1 :: [k]) (h2 :: [k]) where
HSubset '[] x = 'True
HSubset x '[] = 'False
HSubset (h1 ': tl2) h2 = And (Elem h1 h2) (HSubset tl2 h2)