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?

Hardback

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.

Bridgehead

Does the (l :: [*]) mean a type parameter l constrained to kind [*]? – Hardback

@Textfield Exactly! A type parameter that has is a promoted list of types. Come to think of it, getting that to compile may need turning on KindSignatures too and possibly importing Data.Kind too... Just do whatever GHC advises you to. :) – Bridgehead

Answer 2

'[] 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.

Calefacient