Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Understanding this definition of HList

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?

like image 739
lcmylin Avatar asked Dec 14 '16 05:12

lcmylin


1 Answers

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 HLists1. 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.)


1 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.

like image 166
Alec Avatar answered Sep 23 '22 13:09

Alec