Data.Type.List

Operations on type-level lists and tuples, together with their curried versions - the more apostrophes, the more arguments are missing from the function. Curried type functions can be evaluated by the Apply type family from Data.Singletons.

Documentation

type family Map f xs

Maps a curried type function over a type list.

Equations

Map f `[]` = `[]`

Map f (x : xs) = Apply f x : xs

data Map'' :: TyFun (TyFun a b -> *) (TyFun [a] [b] -> *) -> * where

Constructors

Map'' :: Map'' f

Instances

type Apply (TyFun [k] [k1] -> *) (TyFun k k1 -> *) (Map'' k k1) f = Map' k k1 f

data Map' :: (TyFun a b -> *) -> TyFun [a] [b] -> * where

Constructors

Map' :: Map' f g

Instances

type Apply [k] [k] (Map' k k f) l = Map k f l

type family ZipWith f xs ys

Zip two list with a curried two-argument type function.

Equations

ZipWith f `[]` `[]` = `[]`

ZipWith f (x : xs) (y : ys) = Apply (Apply f x) y : ZipWith f xs ys

data ZipWith''' :: TyFun (TyFun a (TyFun b c -> *) -> *) (TyFun [a] (TyFun [b] [c] -> *) -> *) -> * where

Constructors

ZipWith''' :: ZipWith''' f

Instances

type Apply (TyFun [k] (TyFun [k1] [k2] -> *) -> *) (TyFun k (TyFun k1 k2 -> *) -> *) (ZipWith''' k k1 k2) f = ZipWith'' k k1 k2 f

data ZipWith'' :: (TyFun a (TyFun b c -> *) -> *) -> TyFun [a] (TyFun [b] [c] -> *) -> * where

Constructors

ZipWith'' :: ZipWith'' f xs

Instances

type Apply (TyFun [k1] [k2] -> *) [k] (ZipWith'' k k1 k2 f) xs = ZipWith' k k1 k2 f xs

data ZipWith' :: (TyFun a (TyFun b c -> *) -> *) -> [a] -> TyFun [b] [c] -> * where

Constructors

ZipWith' :: ZipWith' f xs ys

Instances

type Apply [k2] [k1] (ZipWith' k k1 k2 f xs) ys = ZipWith k k1 k2 f xs ys

type family Length xs

Length of a type-level list, as a type-level natural number.

Equations

Length `[]` = 0

Length (x : xs) = 1 + Length xs

lengthVal :: forall sing xs. KnownNat (Length xs) => sing xs -> Integer

Length of a type-level list, as an integer.

data Length' :: TyFun [a] Nat -> * where

Constructors

Length' :: Length' l

Instances

type Apply Nat [k] (Length' k) xs = Length k xs

type family Insert a xs

Insert a type into a type list.

Equations

Insert a `[]` = a : `[]`

Insert a (a : xs) = a : xs

Insert a (x : xs) = x : Insert a xs

data Insert'' :: TyFun k (TyFun [k] [k] -> *) -> * where

Constructors

Insert'' :: Insert'' f

Instances

type Apply (TyFun [k] [k] -> *) k (Insert'' k) x = Insert' k x

data Insert' :: k -> TyFun [k] [k] -> * where

Constructors

Insert' :: Insert' x f

Instances

type Apply [k] [k] (Insert' k x) xs = Insert k x xs

type family Union xs ys

Set union over type lists.

Equations

Union `[]` ys = ys

Union (x : xs) ys = Insert x (Union xs ys)

data Union'' :: TyFun [k] (TyFun [k] [k] -> *) -> * where

Constructors

Union'' :: Union'' f

Instances

type Apply (TyFun [k] [k] -> *) [k] (Union'' k) xs = Union' k xs

data Union' :: [k] -> TyFun [k] [k] -> * where

Constructors

Union' :: Union' xs f

Instances

type Apply [k] [k] (Union' k xs) ys = Union k xs ys

type family Remove x ys

Remove a type from type list.

Equations

Remove a `[]` = `[]`

Remove a (a : ys) = ys

Remove a (y : ys) = y : Remove a ys

data Remove'' :: TyFun k (TyFun [k] [k] -> *) -> * where

Constructors

Remove'' :: Remove'' f

Instances

type Apply (TyFun [k] [k] -> *) k (Remove'' k) x = Remove' k x

data Remove' :: k -> TyFun [k] [k] -> * where

Constructors

Remove' :: Remove' x f

Instances

type Apply [k] [k] (Remove' k x) xs = Remove k x xs

type family Difference xs ys

Set difference over type lists.

Equations

Difference `[]` ys = ys

Difference (x : xs) ys = Remove x (Difference xs ys)

data Difference'' :: TyFun [k] (TyFun [k] [k] -> *) -> * where

Constructors

Difference'' :: Difference'' f

Instances

type Apply (TyFun [k] [k] -> *) [k] (Difference'' k) xs = Difference' k xs

data Difference' :: [k] -> TyFun [k] [k] -> * where

Constructors

Difference' :: Difference' xs f

Instances

type Apply [k] [k] (Difference' k xs) ys = Difference k xs ys

type family ReverseAcc xs acc

Helper type family for Reverse.

Equations

ReverseAcc `[]` acc = acc

ReverseAcc (x : xs) acc = ReverseAcc xs (x : acc)

type family Reverse xs

Reverse a type-level list.

Equations

Reverse xs = ReverseAcc xs `[]`

data Reverse' :: TyFun [k] [k] -> * where

Constructors

Reverse' :: Reverse' f

Instances

type Apply [k] [k] (Reverse' k) xs = Reverse k xs

type family Find x ys

Type list membership test.

Equations

Find x `[]` = False

Find x (x : ys) = True

Find x (y : ys) = Find x ys

data Find'' :: TyFun k (TyFun [k] Bool -> *) -> * where

Constructors

Find'' :: Find'' f

Instances

type Apply (TyFun [k] Bool -> *) k (Find'' k) x = Find' k x

data Find' :: k -> TyFun [k] Bool -> * where

Constructors

Find' :: Find' x f

Instances

type Apply Bool [k] (Find' k x) xs = Find k x xs

type family Intersection xs ys

Type list intersection.

Equations

Intersection `[]` ys = `[]`

Intersection (x : xs) (x : ys) = x : Intersection xs ys

Intersection (x : xs) (y : ys) = If (Find x ys) (x : Intersection xs (y : ys)) (Intersection xs (y : ys))

data Intersection'' :: TyFun [k] (TyFun [k] [k] -> *) -> * where

Constructors

Intersection'' :: Intersection'' f

Instances

type Apply (TyFun [k] [k] -> *) [k] (Intersection'' k) xs = Intersection' k xs

data Intersection' :: [k] -> TyFun [k] [k] -> * where

Constructors

Intersection' :: Intersection' xs f

Instances

type Apply [k] [k] (Intersection' k xs) ys = Intersection k xs ys

type family Distinct xs ys

Test if two list do not contain any equal elements.

Equations

Distinct `[]` `[]` = False

Distinct (x : xs) (x : ys) = Distinct xs ys

Distinct (x : xs) (y : ys) = Not (Find x (y : ys)) && Distinct xs ys

data Distinct'' :: TyFun [k] (TyFun [k] Bool -> *) -> * where

Constructors

Distinct'' :: Distinct'' f

Instances

type Apply (TyFun [k] Bool -> *) [k] (Distinct'' k) xs = Distinct' k xs

data Distinct' :: [k] -> TyFun [k] Bool -> * where

Constructors

Distinct' :: Distinct' xs f

Instances

type Apply Bool [k] (Distinct' k xs) ys = Distinct k xs ys

type family Lookup x l

Lookup an association type list.

Equations

Lookup k (`(k, a)` : ls) = a

Lookup k (`(x, a)` : ls) = Lookup k ls

data Lookup'' :: TyFun k (TyFun [(k, a)] a -> *) -> * where

Constructors

Lookup'' :: Lookup'' f

Instances

type Apply (TyFun [(,) k k1] k1 -> *) k (Lookup'' k k1) x = Lookup' k k1 x

data Lookup' :: k -> TyFun [(k, a)] a -> * where

Constructors

Lookup' :: Lookup' x f

Instances

type Apply k [(,) k1 k] (Lookup' k1 k x) xs = Lookup k1 k x xs

type family Fst k

First element of a type pair.

Equations

Fst `(a, b)` = a

data Fst' :: TyFun (a, b) a -> * where

Constructors

Fst' :: Fst' f

Instances

type Apply k1 ((,) k1 k) (Fst' k1 k) ((,) k1 k a b) = a

type family Snd k

Second element of a type pair.

Equations

Snd `(a, b)` = b

data Snd' :: TyFun (a, b) b -> * where

Constructors

Snd' :: Snd' k

Instances

type Apply k1 ((,) k k1) (Snd' k k1) ((,) k k1 a b) = b

type family AsFst a b

Cons a type pair with elements in order.

Equations

AsFst a b = `(a, b)`

data AsFst'' :: TyFun a (TyFun b (a, b) -> *) -> * where

Constructors

AsFst'' :: AsFst'' f

Instances

type Apply (TyFun k1 ((,) k k1) -> *) k (AsFst'' k k1) a = AsFst' k k1 a

data AsFst' :: a -> TyFun b (a, b) -> * where

Constructors

AsFst' :: AsFst' a f

Instances

type Apply ((,) k1 k) k (AsFst' k1 k a) b = AsFst k1 k a b

type family AsSnd a b

Cons a type pair in reverse order.

Equations

AsSnd a b = `(b, a)`

data AsSnd'' :: TyFun a (TyFun b (b, a) -> *) -> * where

Constructors

AsSnd'' :: AsSnd'' f

Instances

type Apply (TyFun k1 ((,) k1 k) -> *) k (AsSnd'' k k1) a = AsSnd' k k1 a

data AsSnd' :: a -> TyFun b (b, a) -> * where

Constructors

AsSnd' :: AsSnd' k f

Instances

type Apply ((,) k k1) k (AsSnd' k1 k a) b = AsSnd k1 k a b

type family Swap k

Swap elements of a type pair.

Equations

Swap `(a, b)` = `(b, a)`

data Swap' :: TyFun (a, b) (b, a) -> * where

Constructors

Swap' :: Swap' f

Instances

type Apply ((,) k1 k) ((,) k k1) (Swap' k k1) ((,) k k1 a b) = Swap k k1 ((,) k k1 a b)