ghc-7.6 class instances for dependent types

Question

Heterogeneous lists are one of the examples given for the new dependent type facility of ghc 7.6:

data HList :: [*] -> * where
  HNil :: HList '[]
  HCons:: a -> HList t -> HList (a ': t)

The example list "li" compiles fine:

li  = HCons "Int: " (HCons 234 (HCons "Integer: " (HCons 129877645 HNil)))

Obviously we would like HList to be in the Show class, but I can only come up with the following working class instantiation that uses mutually recursive constraints (superclasses):

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

instance (Show a, Show' (HList t)) => Show (HList (a ': t)) where
  show l  = "[" ++ show' l ++ "]"

class Show' a where
  show' :: a -> String

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

instance (Show a, Show' (HList t)) => Show' (HList (a ': t)) where
  show' (HCons h l) = case l of
    HNil      -> show h
    HCons _ _ -> show h ++ ", " ++ (show' l)

The code compiles fine and li is shown properly. Compile flags needed are:

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

I tried many variants of the following far more direct definition, but it doesn't compile without me being able to understand the ghc error messages:

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

instance (Show a, Show (HList t)) => Show (HList (a ': t)) where
  show l  = "[" ++ (show' l) ++ "]" where  
    show' (HCons h s) = case s of
      HNil      -> show h
      HCons _ _ -> show h ++ ", " ++ (show' s)

Some Haskell / ghc specialist might understand why this can't work and I would be happy to hear the reason.

Thank you

Hans Peter

---

Thank you, hammar, for your two nice working examples, improving on my first example.

But I still don't understand why my second example doesn't work. You say that "... show' only knows how to show the current element type and not the remaining ones." But wouldn't that comment not also apply in the following (working) code:

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

instance (Show a, Show (HList t)) => Show (HList (a ': t)) where 
   show (HCons h t) = case t of
      HNil      -> show h 
      HCons _ _ -> show h ++ ", " ++ (show t) 

Draconic

Did you try show' (HCons h HNil) = show h, show' (HCons h s) = show h ++ ", " ++ show' s? – Premedical

show' :: forall a t. (Show a, Show (HList t)) => HList (a ': t) -> String doesn't provide any constraint that says that you can show the next element in the list. Defining it like HCons _ _ -> show h ++ ", " ++ show s would work but won't be formatted the same as your original example. – Superadd

To dbaupp: yes I tried, but Nathan's remark applies to both my original non-working solution as well as your proposal. But I don't really understand it. (See below why.) – Draconic

@Draconic I added your edit to Hammers answer to your question. If you want to ask for clarification the proper place in in the comments. – Coolth

@Draconic A Show a, Show (HList t)) constraint states that you can show the head and tail of the list. It doesn't say anything about the Nth element (where N > 0), just the head and tail. Type families with constraint kinds (Hammar's example) or a helper type class (your alternative solution) are two ways around this. – Superadd

Answer 1

As Nathan said in the comments, show' only knows how to show the current element type and not the remaining ones.

As in your first example, we can get around this by making a new type class for show', although you can get away with only one Show instance:

-- Specializing show' to HLists avoids needing a Show' (HList ts) constraint
-- here, which would require UndecidableInstances.
instance (Show' ts) => Show (HList ts) where
  show xs = "[" ++ show' xs ++ "]"

class Show' ts where
  show' :: HList ts -> String

instance Show' '[] where
  show' HNil = ""

instance (Show a, Show' ts) => Show' (a ': ts) where
  show' (HCons a s) = case s of
    HNil     -> show a
    HCons {} -> show a ++ ", " ++ show' s

Another more hackish way of getting all the necessary Show constraints into show' is to use ConstraintKinds to directly build a list of all the necessary constraints.

-- In addition to the extensions in the original code:
{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-}
import GHC.Exts

-- ShowTypes [a, b, c, ...] = (Show a, Show b, Show c, ...)
type family ShowTypes (a :: [*]) :: Constraint
type instance ShowTypes '[] = ()
type instance ShowTypes (a ': t) = (Show a, ShowTypes t) 

instance ShowTypes ts => Show (HList ts) where
  show xs = "[" ++ show' xs ++ "]"
    where
      show' :: ShowTypes ts => HList ts -> String
      show' HNil = ""
      show' (HCons h s) = case s of
        HNil     -> show h
        HCons {} -> show h ++ ", " ++ show' s

Sestos

Reexamining your second solution I actually don't only find it "nice", but exactly answering my question and by no means hackish. I had looked for a way to formulate the Constraint, which you express as a type family. I had hoped to be able to express the induction of the supertype with the instance definition. Thank you again for your good help. – Draconic

Answer 2

Thanks to hammar's second solution I can now offer an even more general approach, which works for a general class (but I suppose that he had this in mind anyway):

type family ConstrainedTypes (a :: [*]) (f :: * -> Constraint) :: Constraint
type instance ConstrainedTypes '[] b = ()
type instance ConstrainedTypes (a ': t) b = (b a, ConstrainedTypes t b) 

instance ConstrainedTypes ts Show => Show (HList ts) where
  show xs = "[" ++ show' xs ++ "]"
    where
      show' :: ConstrainedTypes ts Show => HList ts -> String
      show' HNil = ""
      show' (HCons h s) = case s of
        HNil     -> show h
        HCons {} -> show h ++ ", " ++ show' s

Thank you again for the great help.

Draconic