haskelldependent-typeheterogeneous

Show instance for Heterogeneous List

I am having trouble defining a Show instances for the heterogeneous list defined below:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Kind

data HList xs where
     HNil :: HList TNil
     (::^) :: a -> HList as -> HList (a :^ as)

data TypeList = TNil | (:^) Type TypeList

instance Show (HList TNil) where
     show HNil = "[]"

I would like to give HList xs a show instance, if all types in the Typelist xs have a Show Instance. I guess one should be able to write something like

instance (Show a, _) => Show (HList a :^ as) where
     show (x ::^ xs) = show x ++ show xs

but I am unsure what to fill in the hole _.

PS: If you try this in ghci, don't forget to add the language extensions with

:set -XTypeInType -XTypeOperators
Solution 
  • {-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.Kind

infixr 5 ::^

data HList xs where
     HNil :: HList TNil
     (::^) :: a -> HList as -> HList (a :^ as)

data TypeList = TNil | (:^) Type TypeList

instance Show (HList TNil) where
     show HNil = "HNil"

instance (Show a, Show (HList as)) => Show (HList (a:^as)) where
     showsPrec p (x::^xs) = showParen (p>5)
       $ showsPrec 6 x . ("::^"++) . showsPrec 5 xs

main :: IO ()
main = print ((2 :: Int) ::^ "bla" ::^ HNil)

    2::^"bla"::^HNil