Clr.ListTuple

Documentation

type family ListToTuple (t :: [Type]) :: Type where ...

Equations

ListToTuple '[] = ()

ListToTuple (a ': '[]) = a

ListToTuple (a ': (b ': '[])) = (a, b)

ListToTuple (a ': (b ': (c ': '[]))) = (a, b, c)

ListToTuple (a ': (b ': (c ': (d ': '[])))) = (a, b, c, d)

ListToTuple (a ': (b ': (c ': (d ': (e ': '[]))))) = (a, b, c, d, e)

ListToTuple (a ': (b ': (c ': (d ': (e ': (f ': '[])))))) = (a, b, c, d, e, f)

ListToTuple (a ': (b ': (c ': (d ': (e ': (f ': (g ': '[]))))))) = (a, b, c, d, e, f, g)

ListToTuple (a ': (b ': (c ': (d ': (e ': (f ': (g ': (h ': '[])))))))) = (a, b, c, d, e, f, g, h)

ListToTuple (a ': (b ': (c ': (d ': (e ': (f ': (g ': (h ': (i ': '[]))))))))) = (a, b, c, d, e, f, g, h, i)

ListToTuple (a ': (b ': (c ': (d ': (e ': (f ': (g ': (h ': (i ': (j ': '[])))))))))) = (a, b, c, d, e, f, g, h, i, j)

ListToTuple (a ': (b ': (c ': (d ': (e ': (f ': (g ': (h ': (i ': (j ': (k ': '[]))))))))))) = (a, b, c, d, e, f, g, h, i, j, k)

type family TupleToList (t :: Type) :: [Type] where ...

Equations

TupleToList () = '[]

TupleToList (a, b) = '[a, b]

TupleToList (a, b, c) = '[a, b, c]

TupleToList (a, b, c, d) = '[a, b, c, d]

TupleToList (a, b, c, d, e) = '[a, b, c, d, e]

TupleToList (a, b, c, d, e, f) = '[a, b, c, d, e, f]

TupleToList (a, b, c, d, e, f, g) = '[a, b, c, d, e, f, g]

TupleToList (a, b, c, d, e, f, g, h) = '[a, b, c, d, e, f, g, h]

TupleToList (a, b, c, d, e, f, g, h, i) = '[a, b, c, d, e, f, g, h, i]

TupleToList (a, b, c, d, e, f, g, h, i, j) = '[a, b, c, d, e, f, g, h, i, j]

TupleToList (a, b, c, d, e, f, g, h, i, j, k) = '[a, b, c, d, e, f, g, h, i, j, k]

TupleToList a = '[a]

type family TupleSize (x :: tupleKind) :: Nat where ...

Equations

TupleSize a = ListSize (TupleToList a)

type family ArgCount (x :: tupleKind) :: Nat where ...

Equations

ArgCount () = 1

ArgCount a = TupleSize a

type family ListSize (x :: k) :: Nat where ...

Equations

ListSize '[] = 0

ListSize (x ': xs) = 1 + ListSize xs

type family Elem (a :: k) (xs :: [k]) :: Bool where ...

Equations

Elem a '[] = False

Elem a (x ': xs) = (a == x) || Elem a xs

type family Concat (a :: [[t]]) :: [t] where ...

Equations

Concat '[] = '[]

Concat (x ': xs) = x `Append` Concat xs

type family Append (a :: [t]) (b :: [t]) :: [t] where ...

Equations

Append '[] ys = ys

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

type family CatMaybes (l :: [Maybe k]) :: [k] where ...

Equations

CatMaybes '[] = '[]

CatMaybes (Just x ': xs) = x ': CatMaybes xs

CatMaybes (Nothing ': xs) = CatMaybes xs

type family PrependIf (b :: Bool) (x :: k) (xs :: [k]) :: [k] where ...

Equations

PrependIf True x xs = x ': xs

PrependIf False x xs = xs

type family Index (x :: [t]) (n :: Nat) :: t where ...

Equations

Index (x ': xs) 0 = x

Index (x ': xs) n = Index xs (n - 1)

Index xs n = TypeError (Text "Out of bounds")