Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

ghc-7.6 class instances for dependent types

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) 
like image 625
wurmli Avatar asked Oct 20 '12 14:10

wurmli


1 Answers

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
like image 72
hammar Avatar answered Oct 05 '22 03:10

hammar