CODEWITHSUNDEEP
haskell
Disnesquick
Disnesquick

Reputation: 1

haskell generics documentation incorrect?

I've been going through the GHC Generics documentation here and it seems the example code is incorrect. The part I have trouble with is this:

type RepUserTree a =
  -- A UserTree is either a Leaf, which has no arguments
      U1
  -- ... or it is a Node, which has three arguments that we put in a product
  :+: a :*: UserTree a :*: UserTree a

given that the the (:*:) type operator is defined as data (:*:) f g p = f p :*: g p, as expected, the above bit of code gives the kind error:

 Blockquotetest.hs:26:13: error:
    • Expecting one fewer argument to ‘UserTree a’
      Expected kind ‘* -> *’, but ‘UserTree a’ has kind ‘*’
    • In the first argument of ‘:*:’, namely ‘UserTree a’
      In the second argument of ‘:*:’, namely ‘UserTree a :*: UserTree a’
      In the second argument of ‘:+:’, namely
        ‘a :*: (UserTree a :*: UserTree a)’

Is the documentation incorrect? Am I missing an extension that makes the above work? I'm not really sure how to go about changing the above to compile.

Upvotes: 0

Views: 55

Answers (1)

MCH
MCH

Reputation: 2214

It is just a dummy example to give you an idea of what it is doing because the details are a bit more complex. But it might be worth understanding why it doesn't compile because it is good to understand what is going wrong in these situations if you want to do any sort of type level programming in Haskell.

If you look at the type parameters of (:+:) and (:*:), you can see that they each take three types, f g p. They are both kind * -> * -> * -> *.

data (:+:) f g p = L1 (f p) | R1 (g p)
data (:*:) f g p = f p :*: g p

and p is given to f and g, so we know that f and g must be at least kind * -> *. The UserTree type's kind is * -> *.

data UserTree a = Node a (UserTree a) (UserTree a) | Leaf

but in the declaration we have UserTree a, which is of kind * whereas what (:*:) is expecting two things of at least kind * -> *.

type RepUserTree a = U1 :+: a :*: UserTree a :*: UserTree a

If you remove the a you get it to compile.

type RepUserTree a = U1 :+: a :*: UserTree :*: UserTree

Now look at U1, K1 and M1 they all end in the p parameter. Notice that in the RealRepUserTree example, U1, K1 and M1 all take one type less they than can. These meets the requirements of both (:+:) and (:*:).

Upvotes: 0

Related Questions