module Type.Family.List where
import Type.Family.Constraint
import Type.Family.Monoid
import Type.Family.Tuple hiding (type (<$>),type (<*>),type (<&>))
import Type.Class.Witness
type Ø = '[]
type (:<) = '(:)
infixr 5 :<
type Only a = '[a]
type family Null (as :: [k]) :: Bool where
Null Ø = True
Null (a :< as) = False
nullCong :: (a ~ b) :- (Null a ~ Null b)
nullCong = Sub Wit
nilNotCons :: (Ø ~ (a :< as)) :- Fail
nilNotCons = nullCong
type family (as :: [k]) ++ (bs :: [k]) :: [k] where
Ø ++ bs = bs
(a :< as) ++ bs = a :< (as ++ bs)
infixr 5 ++
appendCong :: (a ~ b,c ~ d) :- ((a ++ c) ~ (b ++ d))
appendCong = Sub Wit
type family Concat (ls :: [[k]]) :: [k] where
Concat Ø = Ø
Concat (l :< ls) = l ++ Concat ls
concatCong :: (as ~ bs) :- (Concat as ~ Concat bs)
concatCong = Sub Wit
type family (as :: [k]) >: (a :: k) :: [k] where
Ø >: a = a :< Ø
(b :< as) >: a = b :< (as >: a)
infixl 6 >:
snocCong :: (as ~ bs,a ~ b) :- ((as >: a) ~ (bs >: b))
snocCong = Sub Wit
type family Reverse (as :: [k]) :: [k] where
Reverse Ø = Ø
Reverse (a :< as) = Reverse as >: a
reverseCong :: (as ~ bs) :- (Reverse as ~ Reverse bs)
reverseCong = Sub Wit
type family HeadM (as :: [k]) :: Maybe k where
HeadM Ø = Nothing
HeadM (a :< as) = Just a
type family Head (as :: [k]) :: k where
Head (a :< as) = a
type family TailM (as :: [k]) :: Maybe [k] where
TailM Ø = Nothing
TailM (a :< as) = Just as
type family Tail (as :: [k]) :: [k] where
Tail (a :< as) = as
type family InitM (as :: [k]) :: Maybe [k] where
InitM Ø = Nothing
InitM (a :< as) = Just (Init' a as)
type family Init (as :: [k]) :: [k] where
Init (a :< as) = Init' a as
type family Init' (a :: k) (as :: [k]) :: [k] where
Init' a Ø = Ø
Init' a (b :< as) = a :< Init' b as
initCong :: (a ~ b,as ~ bs) :- (Init' a as ~ Init' b bs)
initCong = Sub Wit
type family LastM (as :: [k]) :: Maybe k where
LastM Ø = Nothing
LastM (a :< as) = Just (Last' a as)
type family Last (as :: [k]) :: k where
Last (a :< as) = Last' a as
type family Last' (a :: k) (as :: [k]) :: k where
Last' a Ø = a
Last' a (b :< as) = Last' b as
lastCong :: (a ~ b,as ~ bs) :- (Last' a as ~ Last' b bs)
lastCong = Sub Wit
type family ListC (cs :: [Constraint]) = (c :: Constraint) | c -> cs where
ListC Ø = ØC
ListC (c :< cs) = (c, ListC cs)
type family (f :: k -> l) <$> (a :: [k]) :: [l] where
f <$> Ø = Ø
f <$> (a :< as) = f a :< (f <$> as)
infixr 4 <$>
listMapCong :: (f ~ g,as ~ bs) :- ((f <$> as) ~ (g <$> bs))
listMapCong = Sub Wit
type family (f :: [k -> l]) <&> (a :: k) :: [l] where
Ø <&> a = Ø
(f :< fs) <&> a = f a :< (fs <&> a)
infixl 5 <&>
type family (f :: [k -> l]) <*> (a :: [k]) :: [l] where
fs <*> Ø = Ø
fs <*> (a :< as) = (fs <&> a) ++ (fs <*> as)
infixr 4 <*>
type family Fsts (ps :: [(k,l)]) :: [k] where
Fsts Ø = Ø
Fsts (p :< ps) = Fst p :< Fsts ps
type family Snds (ps :: [(k,l)]) :: [l] where
Snds Ø = Ø
Snds (p :< ps) = Snd p :< Snds ps
type family Zip (as :: [k]) (bs :: [l]) = (cs :: [(k,l)]) | cs -> as bs where
Zip Ø Ø = Ø
Zip (a :< as) (b :< bs) = a#b :< Zip as bs
type family Fsts3 (ps :: [(k,l,m)]) :: [k] where
Fsts3 Ø = Ø
Fsts3 (p :< ps) = Fst3 p :< Fsts3 ps
type family Snds3 (ps :: [(k,l,m)]) :: [l] where
Snds3 Ø = Ø
Snds3 (p :< ps) = Snd3 p :< Snds3 ps
type family Thds3 (ps :: [(k,l,m)]) :: [m] where
Thds3 Ø = Ø
Thds3 (p :< ps) = Thd3 p :< Thds3 ps
type instance Mempty = Ø
type instance a <> b = a ++ b