Understanding Kind of Haskell Class

Question

Looking at a kind example from Learn You a Haskell:

data Frank a b = Frank {frankField :: b a} deriving (Show)

LYAH discusses:

we see that Frank has a kind of * -> (* -> *) -> * The first * represents a and the (* -> *) represents b.

This makes sense to me as I think of an example: Frank String Maybe = Frank {frankField :: Maybe String}.

But I'm confused as to how to think about the kind of the right-hand side

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

Since the return type is frankField :: b a, how can the kind of Frank be:

* -> (* -> *) -> * -- what does the right-most * represent?

Why is the right-hand side's kind equal to *?

Answer 1

Well, the Frank on the right-hand side is a value constructor and values don't have kinds, they have types. The kind refers to the Frank on the left-hand side, which is a type constructor. It might help to rename the value constructor to MkFrank:

data Frank a b = MkFrank {frankField :: b a} deriving (Show)

The type of the value constructor is

MkFrank :: b a -> Frank a b

and the kind of the type constructor is

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

This says that Frank takes one (concrete) type (*) and a type constructor that takes one type ((* -> *)) and gives you a type (the last *). This is analogous to a function with a type A -> (B -> C) -> D: it takes a "concrete" value and a function (a way to get a value given another value) and it gives you a "concrete" value, the difference is that we are dealing with types instead of values.

As a side note, kinds work a bit differently for type classes (classes are not involved in the question body though). There's a special kind called Constraint which represents things that can go on the left hand side of => in a signature.

Answer 2

First some important conceptual points:

1. Types exist to "qualify" a set of values that can be treated the same way (in some sense). Types exist "one level up" from the value level, at the type level.

2. Kinds exists to "qualify" a set of types¹ that can be treated the same way (in some sense). Kinds exist "one level up" from the type level, at the kind level.

In any definition of the form data ... = ..., you are doing two things:

1. Adding new possible entities to the value level. The right hand side of the definition gives the "shape" of your possible new values (and the constructors themselves are values, as functions). This uses type-level things to talk about the "shape" of your new values (since that's what types are for), but the declared things are values.

2. Adding new entities to the type level. The left hand side of the definition gives the "shape" of your possible new types (and the type constructor itself is a type-level thing).

So hopefully you can see that the concept of kinds cannot apply to the right-hand side of the equation as a whole, because it's talking about value-level things. It uses some type level things to talk about values, and those things have kinds. The left hand side as a whole does "have a kind", because it introduces a new type, but that kind is always * so it's not very interesting. The type constructor declared on the left hand side can have a more interesting kind.

Let's look at a simple example in more detail:

data Maybe a = Nothing | Just a

Here we've declared that there are new things of the form Nothing and of the form Just a that are values, and new things of the form Maybe a that are types (the equation "links up" the a on both sides, so that Just a is of the type Maybe a, where the a is the same variable).

Just on its own is a constructor, and can be viewed as a function that exists on the value level, and so has a type; it's type is a -> Maybe a. The a has a kind, because it's a type-level thing, but neither Nothing, Just, the whole Just a, nor the entire right hand side Nothing | Just a can be meaningfully said to have a kind.

On the left hand side, the whole Maybe a has kind * (because you're declaring new data types with a data declaration, which have are the types of values, the whole left hand side of a data declaration always has kind *). Maybe on its own is also being introduced as a type constructor; because it takes a single argument it must have a kind like ___ -> *, where we need to fill in the blank.

To know the kind that should fill in the blank, which is the kind of the type variable a in the definition, we need to know how a is used on the RHS. We can see it's only used in the pattern Just a. We know that Just a was the form of new things on the value level, so a must be the type of some set of values to which Just could be applied. The kind of types that have values is *, so a must be of this kind (this is how we avoid non-sensible things like Just Maybe). So that allows us to conclude that Maybe has kind * -> *.

Going back to your example, this is all pretty similar, except that the new type constructor being introduced has the same name as the new value constructor being introduced (both being Frank). This doesn't cause a problem, because they exist on different levels in different namespaces². But always remember that there are still two different things; the Frank from the right hand side is a value constructor, and therefore it doesn't make sense to talk about its kind. The Frank from the left hand side is a type constructor, which does have a kind.

Here, though, the new type constructor Frank has two arguments, so it must be of a kind like ___ -> ___ -> *. Again, we need to look at the right hand side to figure out how a and b are used to know their kinds.

The only use of these two variables is in the type of the single field of the value constructor Frank; this type is b a. b a overall is the type of values that are going to be stored in this field, so it must be of kind *. That means that b is of a kind like ___ -> *.

Now here we're theoretically stuck. a is used only as the argument of b, and we still have a blank to fill as the kind of the argument of b, so whatever kind we assign to a will work³, but this changes the kind of b and also the type constructor Frank. A notion of kind polymorphism would fit here, but by default Haskell just defaults such kinds to *. So a has kind *, b has kind * -> *, and therefore the type constructor Frank has kind * -> (* -> *) -> *.

Frank String Maybe (or indeed Frank a b when we're being polymorphic) is Frank applied to two (type level) arguments, so it has kind *; this is necessary for it to be a type of values. Frank (Just "foo") is a value in the type Frank String Maybe, Frank is a value in the type b a -> Frank a b, and frankField is a value in the type Frank a b -> b a; none of these have kinds (and all of their types have kind *).

TLDR: The type of Frank is b a -> Frank a b, the kind of Frank is * -> (* -> *) -> *, but these two facts can only both be true because they are talking about different entities named Frank; it is impossible to sensibly talk about the kind and the type of the same thing, because kinds and types qualify things on completely different levels.

---

¹ My first lie for the post; kinds qualify "things at the type level", but not all of the type-level things that can exist in Haskell are strictly speaking types (depending on your definitions, anyway). Things with kinds like * -> * are "type-level entities" but they are not things that can stand in a typing relationship to values.

² It's always possible to know purely from the position where a given name appears whether it should be looked up in the type namespace or the value namespace, so the compiler can never confuse type names and value names. Until you're experienced with Haskell this isn't always true for the reader, though!

³ I can prove that this would work with other kinds by declaring them explicitly with the KindSignatures extension:

{-# LANGUAGE KindSignatures #-}

data Frank (a :: * -> *) (b :: (* -> *) -> *)  = Frank {frankField :: b a} deriving Show

data Strange (a :: * -> *) = Strange (a Int)

Then in GHCI:

λ :t Frank
Frank :: b a -> Frank a b

λ :t Frank (Strange (Just 1))
Frank (Strange (Just 1)) :: Frank Maybe Strange

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