Copyright  (c) Marcin Mrotek, 2014 

License  BSD3 
Maintainer  marcin.jan.mrotek@gmail.com 
Safe Haskell  None 
Language  Haskell2010 
Extensions 

Operations on typelevel 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.
 type family Map f xs
 data Map'' :: TyFun (TyFun a b > *) (TyFun [a] [b] > *) > * where
 data Map' :: (TyFun a b > *) > TyFun [a] [b] > * where
 type family ZipWith f xs ys
 data ZipWith''' :: TyFun (TyFun a (TyFun b c > *) > *) (TyFun [a] (TyFun [b] [c] > *) > *) > * where
 ZipWith''' :: ZipWith''' f
 data ZipWith'' :: (TyFun a (TyFun b c > *) > *) > TyFun [a] (TyFun [b] [c] > *) > * where
 data ZipWith' :: (TyFun a (TyFun b c > *) > *) > [a] > TyFun [b] [c] > * where
 type family Length xs
 lengthVal :: forall sing xs. KnownNat (Length xs) => sing xs > Integer
 data Length' :: TyFun [a] Nat > * where
 type family Insert a xs
 data Insert'' :: TyFun k (TyFun [k] [k] > *) > * where
 data Insert' :: k > TyFun [k] [k] > * where
 type family Union xs ys
 data Union'' :: TyFun [k] (TyFun [k] [k] > *) > * where
 data Union' :: [k] > TyFun [k] [k] > * where
 type family Remove x ys
 data Remove'' :: TyFun k (TyFun [k] [k] > *) > * where
 data Remove' :: k > TyFun [k] [k] > * where
 type family Difference xs ys
 data Difference'' :: TyFun [k] (TyFun [k] [k] > *) > * where
 Difference'' :: Difference'' f
 data Difference' :: [k] > TyFun [k] [k] > * where
 Difference' :: Difference' xs f
 type family ReverseAcc xs acc
 type family Reverse xs
 data Reverse' :: TyFun [k] [k] > * where
 type family Find x ys
 data Find'' :: TyFun k (TyFun [k] Bool > *) > * where
 data Find' :: k > TyFun [k] Bool > * where
 type family Intersection xs ys
 data Intersection'' :: TyFun [k] (TyFun [k] [k] > *) > * where
 data Intersection' :: [k] > TyFun [k] [k] > * where
 Intersection' :: Intersection' xs f
 type family Distinct xs ys
 data Distinct'' :: TyFun [k] (TyFun [k] Bool > *) > * where
 Distinct'' :: Distinct'' f
 data Distinct' :: [k] > TyFun [k] Bool > * where
 type family Lookup x l
 data Lookup'' :: TyFun k (TyFun [(k, a)] a > *) > * where
 data Lookup' :: k > TyFun [(k, a)] a > * where
 type family Fst k
 data Fst' :: TyFun (a, b) a > * where
 type family Snd k
 data Snd' :: TyFun (a, b) b > * where
 type family AsFst a b
 data AsFst'' :: TyFun a (TyFun b (a, b) > *) > * where
 data AsFst' :: a > TyFun b (a, b) > * where
 type family AsSnd a b
 data AsSnd'' :: TyFun a (TyFun b (b, a) > *) > * where
 data AsSnd' :: a > TyFun b (b, a) > * where
 type family Swap k
 data Swap' :: TyFun (a, b) (b, a) > * where
Documentation
Maps a curried type function over a type list.
data ZipWith''' :: TyFun (TyFun a (TyFun b c > *) > *) (TyFun [a] (TyFun [b] [c] > *) > *) > * where Source
ZipWith''' :: ZipWith''' f 
data ZipWith'' :: (TyFun a (TyFun b c > *) > *) > TyFun [a] (TyFun [b] [c] > *) > * where Source
Length of a typelevel list, as a typelevel natural number.
lengthVal :: forall sing xs. KnownNat (Length xs) => sing xs > Integer Source
Length of a typelevel list, as an integer.
type family Difference xs ys Source
Set difference over type lists.
Difference `[]` ys = ys  
Difference (x : xs) ys = Remove x (Difference xs ys) 
data Difference'' :: TyFun [k] (TyFun [k] [k] > *) > * where Source
Difference'' :: Difference'' f 
type Apply (TyFun [k] [k] > *) [k] (Difference'' k) xs = Difference' k xs Source 
data Difference' :: [k] > TyFun [k] [k] > * where Source
Difference' :: Difference' xs f 
type Apply [k] [k] (Difference' k xs) ys = Difference k xs ys Source 
type family ReverseAcc xs acc Source
Helper type family for Reverse
.
ReverseAcc `[]` acc = acc  
ReverseAcc (x : xs) acc = ReverseAcc xs (x : acc) 
Type list membership test.
type family Intersection xs ys Source
Type list intersection.
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
type Apply (TyFun [k] [k] > *) [k] (Intersection'' k) xs = Intersection' k xs Source 
data Intersection' :: [k] > TyFun [k] [k] > * where Source
Intersection' :: Intersection' xs f 
type Apply [k] [k] (Intersection' k xs) ys = Intersection k xs ys Source 
data Distinct'' :: TyFun [k] (TyFun [k] Bool > *) > * where Source
Distinct'' :: Distinct'' f 
Lookup an association type list.