data Maybe a = Nothing | Just a
data Either a b = Left a | Right b

Given this, is Maybe -> Int correct? No, since Maybe needs a type. So just as type-checking terms, we need to kind-check types. Mind-boggling!

* is the kind of types

Then we can give the kind of Maybe and Either like this:

Maybe :: * -> * and
Either:: * -> * -> *

This is why Maybe -> Int is not “well-kinded” since Maybe’s kind (* -> *) and ->(having kind *->(*->*)) expects something of kind *.

We can abstract out common bits and write both sum and product as a fold and abstract a function. This is not possible in first order languages. “Sad” according to Simon 🙂 We can do a similar thing for types!

Suppose we have two trees: RoseTree and BinTree (definitions to follow) We can abstract over the common parts, using kinds:

data Tree f a = Leaf a
| Node (f Tree f a))

where:
a :: *
f :: * -> *
Tree:: (*->*) -> * -> *

Should we go further?

Suppose we have this:

We would like T to have the kind forall k.(k->*) -> k -> *

This is similar to a function Append that can have type [int] -> [int] -> [int] or [bool] -> [bool] -> [bool] but not both.

This is called Kind Polymorphism.

A nice addition finally are datakind, for instance Nat, that are more specific than the *.

In summary: Take lessons from term :: type and apply them to type :: kind, leading to the ideas in this talk.

I am sure I missed a lot of details, since Simon’s presenting style is super energetic and fast, which makes it less ‘bloggable’, but still we got to see a lot of cool Haskell constructions that I hadn’t seen before (when I had a Haskell course in university)

Want to know more?