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
?
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 ofHCons1
?
Yes, it is to make sure that HList
has a representational role, which means you can coerce between HList
s1. 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 newtype
s 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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With