Higher Kinded Types: Intro (part: 1 / 2)

If you've been touching haskell for a while, you've probably gone across this operator when talking about types:

. This

is what we call a kind. There are many different uses of kinds, but see them as categories for different types (or as some people who have no regard for saying confusing things call them, types for types).

If you've ever really thought about types that have parametric types, like for example the option type

Maybe

and the type of a basic type,

Int

, you'd notice that two types are different.

Maybe

takes in type parameters,

Maybe

itself does not have values. there is nothing out there of type

Maybe

, there are things out there of type

Maybe a

Maybe

requires a type parameter before becoming a full 'instantiated' type. Therefore, instead of having kind

Int

it has kind

* -> *

Kinds can be even more complex than that however. What is more complex than kinds with one paramater? Why kinds with two parameters of course. Enter the famed either type:

data Either a b = Left a | Right b

It takes two type paramaters, therefore it has kind

* -> * -> *

For haskell, the kind of a type is important not only to differentiate types, but also to specify type classes. Ever notice how haskell only allows functors of kind

* -> *

? In the definition of functor:

class  Functor f where
    fmap        :: (a -> b) -> f a -> f b
    (<$)        :: a -> f b -> f a
    (<$)        =  fmap . const

Haskell's type system implicitly can derive that

here must be of kind

* -> *

and will subsequently require all instances be of that kind too. but that's not all that haskell can do. Haskell can also have higher order kinds like

(* -> *) -> *

-- this has kind (* -> *) -> *
type Intify a = a Int

-- this has kind (* -> *) -> * -> *
type Apply a b = a b

Both these types are valid and would typecheck with the latest version of ghc. Now you may ask, why would anyone ever need those types, and the answer to that question is most of the type you won't need higher kinded types, but on the occasions that you do you'll be glad that GHC can support it. I'm writing up a blog post of my favorite use-case of higher kinded types, recursion-schemes. I'll post a link to it soon! Stay tuned.

Shalom Yiblet

Higher Kinded Types: Intro (part: 1 / 2)

Shalom
Yiblet