Understanding signature of data type, typeclass, and making a data type an instance of a typeclass

1
votes

Been reading Learn You A Haskell For a Great Good ! and have big trouble with understanding instance and kind.

Q1: So the type t in Tofu t acts as a function with the kind signature (* -> (* -> *)) -> * ? And the overall kind signature of tofu is * -> *, isnt it? since (* -> *) -> * results in * and so does (* -> (* -> *)) -> *

Q2: When we want to make Frank a b instance of the typeclass Tofu t, data type Frank a b must also have the same kind with t. That means kind of a is *, b is * -> *, and b a which will be (* -> *) -> * which results in *. Is that correct?

Q3: The x in tofu x represents j a since both have the kind of *. Frank with its kind (* -> (* -> *)) -> * is applied on x. But I'm not sure how presenting j a as x will distinguish the x in tofu x which is j a and the x in Frank x which is a j.

I'm kind of new to the idea of having a function inside data type or class (Ex: b in Frank a b or t in Tofu t) which is a bit confusing

I leave the link here since quoting would make the post look unnecessarily long. link

class Tofu t where
  tofu :: j a -> t a j

data Frank a b = Frank {frankField :: b a} 

instance Tofu Frank where
  tofu x = Frank x
2
haskelltypeclasstype-kinds
Is that valid code? Do I need some extensions switched on? All I'm getting is compile rejection messages. In particular, in the instance Tofu Frank equation, there's no LHS binding for t or b. Where are they coming from? – AntC
As well as :kind that LYAH shows, there's also :info, that tells you everything GHC knows about your names. For example :i Tofu tells you inferred kind for t; :i Frank tells you inferred kinds for a, b. – AntC
@AntC im so sorry the instance code was wrong. I have fixed it. – Jung
thanks. I found a learnable moment trying to get a result out of applying tofu. (Add deriving Show to the data decl for Frank.) Writing tofu (Just "hello") gives nasty type errors. – AntC

2 Answers

6
votes

Q1:

So the type t in Tofu t acts as a function with the kind signature (* -> (* -> *)) -> * ?

t's kind is * -> (* -> *) -> *, or more explicitly * -> ((* -> *) -> *), not (* -> (* -> *)) -> *.

And the overall kind signature of tofu is * -> *, isnt it?

tofu doesn't have a kind signature, only type constructors do; its type's kind is *. So are its argument's and result's types. And same for any function.

Q2: You start with a wrong supposition: instance Tofu Frank makes the Frank type constructor an instance of Tofu, not Frank a b. So it's Frank which must have the same kind as t, not Frank a b (which has kind *).

b a which will be (* -> *) -> *

No, b a is an application of b of kind * -> * to a of kind *, so the application has kind *. Exactly as if b was a function of type x -> y, and a was a value of type x, b a would have type y, not (x -> y) -> x: just replace x and y by *.

Q3:

The x in tofu x represents j a

"Has type", not "represents".

since both have the kind of *

x doesn't have a kind, because it isn't a type.

Frank with its kind (* -> (* -> *)) -> * is applied on x

No, in

tofu x = Frank x

it's the Frank data constructor which is applied to x, not the type constructor. It's a function with signature b a1 -> Frank a1 b (renaming a so you don't confuse it with tofu's). So b ~ j and a1 ~ a.

3
votes

Alexey already had a go at answering your questions. I'll instead expound on your example with whatever details seem relevant.

class Tofu t where
  tofu :: j a -> t a j
          ^^^    ^^^^^
          ^^^^^^^^^^^^

The highlighted bits must have kind *. Anything on either side of a (type level) arrow must have type *[1], and the arrow term itself (that is, the whole j a -> t a j term) also has kind *. Indeed, any "type"[2] that can be inhabited by a value has kind *. If it has any other kind, there can't be any values of it (it is just used as to construct proper types elsewhere).

So, within the signature of tofu, the following holds

j a :: *
t a j :: *

because they are used as "inhabited" types, since they are arguments to (->).

And these are the only things constraining the class. In particular, a can be any kind. With PolyKinds[3]

a :: k   -- for any kind k
j :: k -> *
t :: k     ->   (k -> *) -> *
     ^          ^^^^^^^^    ^
 kind of a      kind of j   required since is used as inhabited type by ->

So we found the required kind of t.

We can use a similar reasoning for Frank.

data Frank a b = Frank {frankField :: b a}
     ^^^^^^^^^                        ^^^

Again the highlighted bits have to have kind *, because they can have values. Otherwise there are no constraints. Generalizing, we have

a :: k
b :: k -> *
Frank a b :: *

And thus

Frank :: k -> (k -> *) -> *

We can see that Frank's kind matches the required kind for Tofu. But it also makes sense for a more specific kind, for example:

data KatyPerry a b = KatyPerry a (b Int)

Try to deduce her kind, and check that it is more specific than the kind required by Tofu.

[1] This is even true of arrows at the kind level if we assume TypeInType. Without TypeInType, the "kinds of kinds" are called sorts and nobody worries about them; there's usually nothing interesting happening at that level.

[2] I put "type" in quotes because technically only things with kind * are called types, everything else is called a type constructor. I tried to be precise about this but I couldn't find a non-awkward way to refer to both at once and the paragraph got very messy. So "type" it is.

[3] Without PolyKinds, anything with an unconstrained kind like k gets specialized to *. It also means that Tofu's kind could depend on what type you first happen to instantiate it at, or whether you instantiate it at a type in the same module or a different module. It's bad. PolyKinds is good.