Type.Family.List

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

Documentation

type Ø = `[]`

type (:<) = (:) infixr 5

type Only a = `[a]`

Type-level singleton list.

type family Null as :: Bool

Equations

Null Ø = True

Null (a :< as) = False

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

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

type family as ++ bs :: [k] infixr 5

Appends two type-level lists.

Equations

Ø ++ bs = bs

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

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

type family as >: a :: [k] infixl 6

Type-level list snoc.

Equations

Ø >: a = Only a

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

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

type family Reverse as :: [k]

Equations

Reverse Ø = Ø

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

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

type family Head as :: k

Equations

Head (a :< as) = a

type family Tail as :: [k]

Equations

Tail (a :< as) = as

type family Init as :: [k]

Equations

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

type family Init' a as :: [k]

Equations

Init' a Ø = Ø

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

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

type family Last as :: k

Equations

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

type family Last' a as :: k

Equations

Last' a Ø = a

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

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

type family ListC cs :: Constraint

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 <$> a :: [l] infixr 4

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))

type family f <&> a :: [l] infixl 5

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 <*> a :: [l] infixr 4

Equations

fs <*> Ø = Ø

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

type family Fsts ps :: [k]

Equations

Fsts Ø = Ø

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

type family Snds ps :: [l]

Equations

Snds Ø = Ø

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

type family Zip as bs :: [(k, l)]

Equations

Zip Ø Ø = Ø

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

type family Fsts3 ps :: [k]

Equations

Fsts3 Ø = Ø

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

type family Snds3 ps :: [l]

Equations

Snds3 Ø = Ø

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

type family Thds3 ps :: [m]

Equations

Thds3 Ø = Ø

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