HList.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module HList where

-- statically bounded recursion, see the bottom of the file for results

data HList :: [*] -> * where
  Nil :: HList '[]
  (:>) :: a -> HList as -> HList (a ': as)
infixr 5 :>

-- recursive length
length1 :: HList xs -> Int
length1 Nil = 0
length1 (_ :> xs) = 1 + length1 xs

-- statically recursive length
class Length2 (xs :: [*]) where
  length2 :: HList xs -> Int

instance Length2 '[] where
  length2 Nil = 0
  {-# INLINE length2 #-}

instance Length2 xs => Length2 (x ': xs) where
  length2 (_ :> xs) = 1 + length2 xs
  {-# INLINE length2 #-}


-- $ ghc -O -fforce-recomp -ddump-simpl -dsuppress-all -ddump-to-file HList.hs

testList = "hello" :> 2 :> False :> 'c' :> Nil

test1 = length1 testList
-- test1 = case $wlength1 testList of ww_s1kD { __DEFAULT -> I# ww_s1kD }

test2 = length2 testList
-- test2 = I# 4#