1{-# LANGUAGE DataKinds #-} 2{-# LANGUAGE GADTs #-} 3{-# LANGUAGE KindSignatures #-} 4{-# LANGUAGE TypeOperators #-} 5 6import Data.Kind 7 8data Nat = Z | S Nat 9 10data HList (ls :: [Type]) where 11 HNil :: HList '[] 12 HCons :: t -> HList ts -> HList (t ': ts) 13 14data ElemAt (n :: Nat) t (ts :: [Type]) where 15 AtZ :: ElemAt 'Z t (t ': ts) 16 AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) 17 18lookMeUp :: ElemAt i ty tys -> HList tys -> ty 19lookMeUp AtZ (HCons t hl') = _ 20lookMeUp (AtS ea') (HCons t hl') = _ 21 22