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 :: TyFun a b -> *) (xs :: [a]) where ...

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 a b -> *) (TyFun [a] [b] -> *) (Map'' a b) f

type Apply (TyFun a b -> *) (TyFun [a] [b] -> *) (Map'' a b) f = Map' a b f

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

Constructors

Map' :: Map' f g

Instances

type Apply [b] [b] (Map' b b f) l

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

type family ZipWith (f :: TyFun a (TyFun b c -> *) -> *) (xs :: [a]) (ys :: [b]) where ...

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 a (TyFun b c -> *) -> *) (TyFun [a] (TyFun [b] [c] -> *) -> *) (ZipWith''' a b c) f

type Apply (TyFun a (TyFun b c -> *) -> *) (TyFun [a] (TyFun [b] [c] -> *) -> *) (ZipWith''' a b c) f = ZipWith'' a b c f

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

Constructors

ZipWith'' :: ZipWith'' f xs

Instances

type Apply [a] (TyFun [b] [c] -> *) (ZipWith'' a b c f) xs

type Apply [a] (TyFun [b] [c] -> *) (ZipWith'' a b c f) xs = ZipWith' a b c f xs

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

Constructors

ZipWith' :: ZipWith' f xs ys

Instances

type Apply [b] [c] (ZipWith' a b c f xs) ys

type Apply [b] [c] (ZipWith' a b c f xs) ys = ZipWith a b c f xs ys

type family Length xs where ...

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 [k] Nat (Length' k) xs

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

type family Insert a xs where ...

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 k (TyFun [k] [k] -> *) (Insert'' k) x

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

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

Constructors

Insert' :: Insert' x f

Instances

type Apply [a] [a] (Insert' a x) xs

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

type family Union xs ys where ...

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 [k] (TyFun [k] [k] -> *) (Union'' k) xs

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

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

Constructors

Union' :: Union' xs f

Instances

type Apply [a] [a] (Union' a xs) ys

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

type family Remove x ys where ...

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 k (TyFun [k] [k] -> *) (Remove'' k) x

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

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

Constructors

Remove' :: Remove' x f

Instances

type Apply [a] [a] (Remove' a x) xs

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

type family Difference xs ys where ...

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 [k] (TyFun [k] [k] -> *) (Difference'' k) xs

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

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

Constructors

Difference' :: Difference' xs f

Instances

type Apply [a] [a] (Difference' a xs) ys

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

type family ReverseAcc xs acc where ...

Helper type family for Reverse.

Equations

ReverseAcc '[] acc = acc

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

type family Reverse xs where ...

Reverse a type-level list.

Equations

Reverse xs = ReverseAcc xs '[]

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

Constructors

Reverse' :: Reverse' f

Instances

type Apply [a] [a] (Reverse' a) xs

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

type family Find x ys where ...

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 k (TyFun [k] Bool -> *) (Find'' k) x

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

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

Constructors

Find' :: Find' x f

Instances

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

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

type family Intersection xs ys where ...

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 [k] (TyFun [k] [k] -> *) (Intersection'' k) xs

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

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

Constructors

Intersection' :: Intersection' xs f

Instances

type Apply [a] [a] (Intersection' a xs) ys

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

type family Distinct xs ys where ...

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 [k] (TyFun [k] Bool -> *) (Distinct'' k) xs

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

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

Constructors

Distinct' :: Distinct' xs f

Instances

type Apply [a] Bool (Distinct' a xs) ys

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

type family Lookup (x :: k) (l :: [(k, a)]) where ...

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 k (TyFun [(k, a)] a -> *) (Lookup'' k a) x

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

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

Constructors

Lookup' :: Lookup' x f

Instances

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

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

type family Fst k where ...

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 (k2, b) k2 (Fst' b k2) ((,) k2 b a b1)

type Apply (k2, b) k2 (Fst' b k2) ((,) k2 b a b1) = a

type family Snd k where ...

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 (a, k2) k2 (Snd' a k2) ((,) a k2 a1 b)

type Apply (a, k2) k2 (Snd' a k2) ((,) a k2 a1 b) = b

type family AsFst a b where ...

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 a (TyFun b (a, b) -> *) (AsFst'' a b) a1

type Apply a (TyFun b (a, b) -> *) (AsFst'' a b) a1 = AsFst' b a a1

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

Constructors

AsFst' :: AsFst' a f

Instances

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

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

type family AsSnd a b where ...

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 a (TyFun b (b, a) -> *) (AsSnd'' b a) a1

type Apply a (TyFun b (b, a) -> *) (AsSnd'' b a) a1 = AsSnd' b a a1

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

Constructors

AsSnd' :: AsSnd' k f

Instances

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

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

type family Swap k where ...

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) ((,) k1 k a b)

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