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))
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?
Read the paper.