module Data.TypeList where
import Data.Cardinal
import Prelude hiding (drop, head, reverse, tail, (!!))
class TypeList l where
type Length l
length :: l -> Length l
length _ = undefined
class TypeList l => HeadTail l where
type Head l
type Tail l
head :: l -> Head l
tail :: l -> Tail l
(.|.) :: Head l -> Tail l -> l
class Component l n where
type l :!!: n
(!!) :: l -> n -> l :!!: n
partialMap :: n -> (l :!!: n -> l :!!: n) -> l -> l
instance HeadTail l => Component l Zero where
type l :!!: Zero = Head l
(!!) l _ = head l
partialMap _ f l = f (head l) .|. tail l
instance (HeadTail l, Component (Tail l) n) => Component l (Succ n) where
type l :!!: Succ n = Tail l :!!: n
(!!) l n = tail l !! p n
where p :: Succ n -> n
p _ = undefined
partialMap n f l = head l .|. partialMap (p n) f (tail l)
where p :: Succ n -> n
p _ = undefined
class (TypeList l, TypeList l') => AppendList l l' where
type l :++: l'
(<++>) :: l -> l' -> l :++: l'
class (Cardinal n, TypeList l) => TakeList n l where
type Take n l
take :: n -> l -> Take n l
class (Cardinal n, TypeList l) => DropList n l where
type Drop n l
drop :: n -> l -> Drop n l
class (TypeList l, TypeList l') => TailRevList l l' where
type TailRev l l'
rev :: l -> l' -> TailRev l l'
class TypeList l => ReverseList l where
type Reverse l
reverse :: l -> Reverse l
class JoinList n l l' where
type Join n l l'
join :: n -> l -> l' -> Join n l l'
instance (ReverseList (Drop n (Reverse l)),
DropList n (Reverse l),
ReverseList l,
AppendList (Reverse (Drop n (Reverse l))) (Drop n l'),
DropList n l',
Reverse (Take n (Reverse l)) ~ Take n l')
=> JoinList n l l' where
type Join n l l' = Reverse (Drop n (Reverse l)) :++: Drop n l'
join n l l' = reverse (drop n (reverse l)) <++> drop n l'
class Extend l l' where
type Ext l l'
extend :: l -> Ext l l' -> l'