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

'[] and (x ': xs) are syntax for type-level lists in the sense that the DataKinds language extension allows promoting types to kinds and constructors to types; i.e. if k is some kind, then '[k] is also a kind, and '[] is a type of kind '[k], and if t :: k and ts :: '[k], then t ': ts :: '[k]. Everything gets shifted by one.

So in HList (x ': xs), x and xs match two types: x matches a "normal" type of kind * (e.g. Int) and xs matches another type-level list of kind '[*]. The right-hand side defines a (newtype) datatype that has a constructor HCons1 with a parameter of type (x, HList xs).

As an example, we can have

HCons1 (1, HCons1 (True, HNil)) :: HList '[Int, Bool]

Or, using the pattern synonym:

1 `HCons` True `HCons` HNil :: HList '[Int, Bool]

I don't have a good answer to your second question regarding why it's represented as a newtype with a tuple.

Answer 2

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.