hlist.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
 
{-# OPTIONS_GHC -Wall #-}
 
data HList f l where
  HNil :: HList f '[]
  HCons :: f a -> HList f l -> HList f (a ': l)
 
--how can I write reverse and (++)?
 
lengthH :: HList f l -> Int
lengthH HNil = 0
lengthH (HCons _ xs) = lengthH xs + 1
 
headH :: HList f (a ': as) -> f a
headH (HCons x _) = x
 
tailH :: HList f (a ': as) -> HList f as
tailH (HCons _ xs) = xs

rev_app :: [a] -> [a] -> [a]
rev_app [] acc = acc
rev_app (x:xs) acc = rev_app xs (x:acc)

reverse' :: [a] -> [a]
reverse' xs = rev_app xs []

type family App (xs :: [k]) (ys :: [k]) :: [k] where
  App '[] ys = ys
  App (x ': xs) ys = x ': App xs ys

happ :: HList f xs -> HList f ys -> HList f (App xs ys)
happ HNil ys = ys
happ (HCons x xs) ys = HCons x (happ xs ys)