HList

{-# LANGUAGE GADTs, DataKinds, TypeOperators, FlexibleContexts, FlexibleInstances #-}

data HList ty where
  Nil  :: HList '[]
  (:>) :: h -> HList t -> HList (h ': t)
infixr 5 :>

instance Show (HList '[]) where
  show _ = "[]"

instance (Show h, Show (HList t)) => Show (HList (h ': t)) where
  show (h :> t) = let '[':s = show t in 
    "[" ++ show h ++ (if s == "]" then s else " :> " ++ s)
    
data Elem tys ty where
  EZ :: Elem (x ': xs) x
  ES :: Elem xs x -> Elem (y ': xs) x

get :: Elem tys ty -> HList tys -> ty
get EZ (h :> _) = h
get (ES elems) (_ :> t) = get elems t

main = do
  let myList = True :> [1,2,3,4] :> () :> ('c' :> [1,2] :> Nil) :> 42 :> Nil
  print myList
  putStrLn "----"
  print $ get EZ myList
  print $ get (ES (ES (ES EZ))) myList