haskell - Understanding this definition of HList

Question

I'm relatively new to Haskell, and I'm trying to understand one of the definitions of HList.

data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x xs = HCons1 (x, xs)

I have a couple specific questions:

• What is the '[] and (x ': xs) syntax I'm seeing? It almost looks like it's pattern matching on variadic type parameters, but I have never seen this syntax before, nor am I familiar with variadic type parameters in Haskell. I would guess this is part of GHC's Type Families, but I don't see anything about this on the linked page, and it's rather hard to search syntax in Google.

• Is there any point in using a newtype declaration with a tuple (instead of a data declaration with two fields) besides avoiding boxing of HCons1?

Answer 1

First, you are missing part of the definition: the data family declaration itself.

data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)

This is called a data family (available under the TypeFamilies extension).

pattern HCons x xs = HCons1 (x, xs)

This is a bidirectional pattern (available under the PatternSynonyms extension).

What is the '[] and (x ': xs) syntax I'm seeing?

When you see ' marks in front of constructors, it is to denote their promoted type-level counterparts. As a syntactic convenience, promoted lists and tuples also just need the extra tick (and we still get to write '[] for the empty type-level list and ': for the type level cons. All of this is available through the DataKinds extension.

Is there any point in using a newtype declaration with a tuple (instead of a data declaration with two fields) besides avoiding boxing of HCons1?

Yes, it is to make sure that HList has a representational role, which means you can coerce between HLists¹. This is a bit too involved to explain in just an answer, but here is an example of where things don't go as we want when we have

 data instance HList (x ': xs) = HCons x (HList xs)

instead of the newtype instance (and no pattern). Consider the following newtypes which are representationally equivalent to Int, Bool, and () respectively

newtype MyInt = MyInt Int
newtype MyBool = MyBool Bool
newtype MyUnit = MyUnit ()

Recall we can use coerce to wrap or unwrap these types automatically. Well, we'd like to be able to do the same thing, but for a whole HList:

ghci> l  = (HCons 3 (HCons True (HCons () HNil))) :: HList '[Int,   Bool,   ()]
ghci> l' = coerce l                               :: HList '[MyInt, MyBool, MyUnit]

This works with the newtype instance variant, but not the data instance one because of the roles. (More on that here.)

---

¹ technically, there is no role for a data family as a whole: the roles can be different for each instance/newtype - here we only really need the HCons case to be representational, since that's the one that gets coerced. Check out this Trac ticket.