type-list-0.1.0.0: Operations on type-level lists and tuples.

Copyright(c) Marcin Mrotek, 2014
LicenseBSD3
Maintainermarcin.jan.mrotek@gmail.com
Safe HaskellNone
LanguageHaskell2010
Extensions
  • UndecidableInstances
  • MonoLocalBinds
  • ScopedTypeVariables
  • TypeFamilies
  • GADTs
  • GADTSyntax
  • PolyKinds
  • DataKinds
  • KindSignatures
  • TypeOperators
  • ExplicitNamespaces
  • ExplicitForAll

Data.Type.List

Description

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.

Synopsis

Documentation

type family Map f xs Source

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 Source

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 Source

Constructors

Map' :: Map' f g 

Instances

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

type family Length xs Source

Equations

Length [] = 0 
Length (x : xs) = 1 + Length xs 

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

Constructors

Length' :: Length' l 

Instances

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

type family Insert a xs Source

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 Source

Constructors

Insert'' :: Insert'' f 

Instances

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

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

Constructors

Insert' :: Insert' x f 

Instances

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

type family Union xs ys Source

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 Source

Constructors

Union'' :: Union'' f 

Instances

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

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

Constructors

Union' :: Union' xs f 

Instances

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

type family Remove x ys Source

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 Source

Constructors

Remove'' :: Remove'' f 

Instances

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

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

Constructors

Remove' :: Remove' x f 

Instances

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

type family Difference xs ys Source

Equations

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

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

Constructors

Difference'' :: Difference'' f 

Instances

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

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

Constructors

Difference' :: Difference' xs f 

Instances

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

type family ReverseAcc xs acc Source

Equations

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

type family Reverse xs Source

Equations

Reverse xs = ReverseAcc xs [] 

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

Constructors

Reverse' :: Reverse' f 

Instances

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

type family Find x ys Source

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 Source

Constructors

Find'' :: Find'' f 

Instances

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

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

Constructors

Find' :: Find' x f 

Instances

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

type family Intersection xs ys Source

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 Source

Constructors

Intersection'' :: Intersection'' f 

Instances

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

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

Constructors

Intersection' :: Intersection' xs f 

Instances

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

type family Distinct xs ys Source

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 Source

Constructors

Distinct'' :: Distinct'' f 

Instances

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

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

Constructors

Distinct' :: Distinct' xs f 

Instances

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

type family Lookup x l Source

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 Source

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 Source

Constructors

Lookup' :: Lookup' x f 

Instances

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

type family Fst k Source

First element of a type pair.

Equations

Fst `(a, b)` = a 

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

Constructors

Fst' :: Fst' f 

Instances

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

type family Snd k Source

Second element of a type pair.

Equations

Snd `(a, b)` = b 

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

Constructors

Snd' :: Snd' k 

Instances

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

type family AsFst a b Source

Cons a type pair with elements in order.

Equations

AsFst a b = `(a, b)` 

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

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 Source

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 Source

Cons a type pair in reverse order.

Equations

AsSnd a b = `(b, a)` 

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

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 Source

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 Source

Swap elements of a type pair.

Equations

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

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

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)