type-combinators-0.2.4.3: A collection of data types for type-level programming

CopyrightCopyright (C) 2015 Kyle Carter
LicenseBSD3
MaintainerKyle Carter <kylcarte@indiana.edu>
Stabilityexperimental
PortabilityRankNTypes
Safe HaskellNone
LanguageHaskell2010

Type.Family.List

Description

Convenient aliases and type families for working with type-level lists.

Synopsis

Documentation

type Ø = '[] Source #

type (:<) = (:) infixr 5 Source #

type Only a = '[a] Source #

Type-level singleton list.

type family Null (as :: [k]) :: Bool where ... Source #

Equations

Null Ø = True 
Null (a :< as) = False 

nullCong :: (a ~ b) :- (Null a ~ Null b) Source #

nilNotCons :: (Ø ~ (a :< as)) :- Fail Source #

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ... infixr 5 Source #

Appends two type-level lists.

Equations

Ø ++ bs = bs 
(a :< as) ++ bs = a :< (as ++ bs) 

appendCong :: (a ~ b, c ~ d) :- ((a ++ c) ~ (b ++ d)) Source #

type family Concat (ls :: [[k]]) :: [k] where ... Source #

Equations

Concat Ø = Ø 
Concat (l :< ls) = l ++ Concat ls 

concatCong :: (as ~ bs) :- (Concat as ~ Concat bs) Source #

type family (as :: [k]) >: (a :: k) :: [k] where ... infixl 6 Source #

Type-level list snoc.

Equations

Ø >: a = a :< Ø 
(b :< as) >: a = b :< (as >: a) 

snocCong :: (as ~ bs, a ~ b) :- ((as >: a) ~ (bs >: b)) Source #

type family Reverse (as :: [k]) :: [k] where ... Source #

Equations

Reverse Ø = Ø 
Reverse (a :< as) = Reverse as >: a 

reverseCong :: (as ~ bs) :- (Reverse as ~ Reverse bs) Source #

type family HeadM (as :: [k]) :: Maybe k where ... Source #

Equations

HeadM Ø = Nothing 
HeadM (a :< as) = Just a 

type family Head (as :: [k]) :: k where ... Source #

Equations

Head (a :< as) = a 

type family TailM (as :: [k]) :: Maybe [k] where ... Source #

Equations

TailM Ø = Nothing 
TailM (a :< as) = Just as 

type family Tail (as :: [k]) :: [k] where ... Source #

Equations

Tail (a :< as) = as 

type family InitM (as :: [k]) :: Maybe [k] where ... Source #

Equations

InitM Ø = Nothing 
InitM (a :< as) = Just (Init' a as) 

type family Init (as :: [k]) :: [k] where ... Source #

Equations

Init (a :< as) = Init' a as 

type family Init' (a :: k) (as :: [k]) :: [k] where ... Source #

Equations

Init' a Ø = Ø 
Init' a (b :< as) = a :< Init' b as 

initCong :: (a ~ b, as ~ bs) :- (Init' a as ~ Init' b bs) Source #

type family LastM (as :: [k]) :: Maybe k where ... Source #

Equations

LastM Ø = Nothing 
LastM (a :< as) = Just (Last' a as) 

type family Last (as :: [k]) :: k where ... Source #

Equations

Last (a :< as) = Last' a as 

type family Last' (a :: k) (as :: [k]) :: k where ... Source #

Equations

Last' a Ø = a 
Last' a (b :< as) = Last' b as 

lastCong :: (a ~ b, as ~ bs) :- (Last' a as ~ Last' b bs) Source #

type family ListC (cs :: [Constraint]) = (c :: Constraint) | c -> cs where ... Source #

Takes a type-level list of Constraints to a single Constraint, where ListC cs holds iff all elements of cs hold.

Equations

ListC Ø = ØC 
ListC (c :< cs) = (c, ListC cs) 

type family (f :: k -> l) <$> (a :: [k]) :: [l] where ... infixr 4 Source #

Map an (f :: k -> l) over a type-level list (as :: [k]), giving a list (bs :: [l]).

Equations

f <$> Ø = Ø 
f <$> (a :< as) = f a :< (f <$> as) 

listMapCong :: (f ~ g, as ~ bs) :- ((f <$> as) ~ (g <$> bs)) Source #

type family (f :: [k -> l]) <&> (a :: k) :: [l] where ... infixl 5 Source #

Map a list of (fs :: [k -> l]) over a single (a :: k), giving a list (bs :: [l]).

Equations

Ø <&> a = Ø 
(f :< fs) <&> a = f a :< (fs <&> a) 

type family (f :: [k -> l]) <*> (a :: [k]) :: [l] where ... infixr 4 Source #

Equations

fs <*> Ø = Ø 
fs <*> (a :< as) = (fs <&> a) ++ (fs <*> as) 

type family Fsts (ps :: [(k, l)]) :: [k] where ... Source #

Equations

Fsts Ø = Ø 
Fsts (p :< ps) = Fst p :< Fsts ps 

type family Snds (ps :: [(k, l)]) :: [l] where ... Source #

Equations

Snds Ø = Ø 
Snds (p :< ps) = Snd p :< Snds ps 

type family Zip (as :: [k]) (bs :: [l]) = (cs :: [(k, l)]) | cs -> as bs where ... Source #

Equations

Zip Ø Ø = Ø 
Zip (a :< as) (b :< bs) = (a # b) :< Zip as bs 

type family Fsts3 (ps :: [(k, l, m)]) :: [k] where ... Source #

Equations

Fsts3 Ø = Ø 
Fsts3 (p :< ps) = Fst3 p :< Fsts3 ps 

type family Snds3 (ps :: [(k, l, m)]) :: [l] where ... Source #

Equations

Snds3 Ø = Ø 
Snds3 (p :< ps) = Snd3 p :< Snds3 ps 

type family Thds3 (ps :: [(k, l, m)]) :: [m] where ... Source #

Equations

Thds3 Ø = Ø 
Thds3 (p :< ps) = Thd3 p :< Thds3 ps