Shared constraint for items of an HList

Question

Suppose we have a following definition of HList:

data HL spec where
  HLNil :: HL ()
  HLCons :: h -> HL t -> HL (h, t)

Is it possible to somehow enforce a shared constraint on its items?

As an example, following is my attempt to constrain the items to have Show instances, which fails with Couldn't match type `Char' with `Int':

class HLSpecEach spec item
instance HLSpecEach () item
instance (HLSpecEach t item, h ~ item) => HLSpecEach (h, t) item

a :: (Show item, HLSpecEach spec item) => HL spec -> Int
a = undefined

b :: HL (Int, (Char, ()))
b = undefined

c = a b

Misbeliever

Answer 1

Easy to do if you have constraint kinds and type families. First, let me say I prefer using DataKinds for clarity

data HList ls where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

type family ConstrainAll (c :: * -> Constraint) (ls :: [*]) :: Constraint
type instance ConstrainAll c '[] = ()
type instance ConstrainAll c (x ': xs) = (c x, ConstrainAll c xs)

showAll :: ConstrainAll Show xs => HList xs -> [String]
showAll HNil = []
showAll (HCons x xs) = (show x) : showAll xs

if you don't use the new extensions it is possible, but much uglier. One option is to define custom classes for everything

class ShowAll ls where
  showAll :: HList ls -> [Show]
instance ShowAll () where
  showAll _ = []
instance (ShowAll xs, Show x) => ShowAll (x,xs)
  showAll (HCons x xs) = (show x) : (showAll xs)

which I find ugly. A more clever approach would be to fake constraint kinds

class Constrained tag aType where
  isConstained :: tag aType

data HListT tag ls where
  HNilT :: HListT tag ()
  HConsT :: x -> tag x -> HListT tag xs -> HListT tag (x,xs)

data Proxy (f :: * -> *) = Proxy 
class ConstainedAll tag ls  where
  tagThem :: Proxy tag -> HList ls -> HListT tag ls
instance ConstainedAll tag () where
  tagThem _ _ = HNilT
instance (ConstainedAll tag xs, Constrained tag x) => ConstainedAll tag (x,xs) where
  tagThem p (HCons x xs) = HConsT x isConstained (tagThem p xs)

which you can then use like

data Showable x where Showable :: Show x => Showable x
instance Show x => Constrained Showable x where isConstained = Showable

--inferred type showAll' :: HListT Showable xs -> [String]
showAll' HNilT = []
showAll' (HConsT x Showable xs) = (show x) : showAll' xs

--inferred type: showAll :: ConstainedAll Showable xs => HList xs -> [String]
showAll xs = showAll' (tagThem (Proxy :: Proxy Showable) xs)

example = showAll (HCons "hello" (HCons () HNil))

which should (havent tested) work with any GHC with GADTs, MPTC, Flexible Contexts/Instances, and Kind Signatures (you can get rid of the last one easily).

EDIT: In GHC 7.6+ you should use

type family ConstrainAll (c :: k -> Constraint) (ls :: [k]) :: Constraint

(k instead of the *) and turn on PolyKinds, but this won't work with the GHC 7.4 implementation of PolyKinds (hence the monomorphic code). In the same way, defining

data HList f ls where
  HNil :: HList f '[]
  HCons :: !(f x) -> !(HList f xs) -> HList f (x ': xs)

lets you avoid code duplication when you want things like a lazy vs strict HLists or when you want a list of dictionaries, or universal variants of higher kinded types, etc.

Decern

You might want to add that Constraint is partof the constraints package, and you have to import Data.Constraint for the DataKinds solution. You also need the ConstraintKinds extension. :-) – Quark

Easy... Yeah, it's not like it could be any harder than concatenating strings or something, right? It's easy. Easy is the name for it! Sure! I mean, you look at it and you totally see why. Piece of cake! ) Seriously though, thank you! – Misbeliever

To be fair, the Constraint solution is pretty easy (compared to the others. All owing to DataKinds being really useful.) You can see a more general approach in this SO answer: https://mcmap.net/q/1514686/-ghc-7-6-class-instances-for-dependent-types The entire thread is actually pretty interesting, and I think it might help you. – Quark

Easy compared to what this code looked like as of the original Hlist paper! – Decern