{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}


-- -- Method 1
-- data family Hlist (l :: [*])
-- data instance Hlist '[] = HNil
-- data instance Hlist (t ': ts) = HCons t (Hlist ts)

-- hd :: Hlist (t ': ts) -> t  
-- hd (HCons x _) = x

-- tl :: Hlist (t ': ts) -> Hlist ts
-- tl (HCons _ xs) = xs

-- idx :: Hlist ts -> (n :: Int) -> (ts '!! n)

-- -- Can't make it work
-- -- app :: Hlist ts1 -> Hlist ts2 -> Hlist (ts1 '++ ts2)
-- -- app HNil hls2 = hls2

-- -- Can't make it work
-- -- len :: Hlist ts -> Int
-- -- len HNil = 0
-- -- len (HCons _ xs) = 1 + (len xs)


-- -- Method 2 ??
-- data HNil = HNil
-- data HCons a b = HCons a b 

-- a = HCons 3 HNil 
-- b = HCons 3 (HCons True HNil)
  


-- -- Method 3
-- data Hlist :: [*] -> * where
--   HNil :: Hlist '[]
--   HCons :: t -> Hlist ts -> Hlist (t : ts)

-- data Member x (l':ls) where
--   First :: Member x (l:ls)
--   Next :: Member x ls -> Member x (l:ls)

-- data Member x (l':ls) where
--   First :: Member x (l:ls)
--   Next :: Member x ls -> Member x (l:ls)

-- len :: Hlist ts -> Int
-- len HNil = 0
-- len (HCons _ xs) = 1 + (len xs)

-- a = HCons 3 HNil 
-- b = HCons 3 (HCons True HNil)