I remember when I was first learning Haskell, one of the terms being thrown around all the time was higher-kinded types. Coming from OCaml, it was commonly referenced as one of the major differences between the two languages. But as much as I tried to understand, I couldn't grasp what I now see as a simple concept. Every StackOverflow answer, blog post, or article I read about HKTs failed to explain the idea in a way that makes sense to me. It wasn't until I read a blog post on the repercussions of having HKTs available in C# that I really started to understand the idea. Here's my attempt at explaining the idea in a way that wouldn't confuse me more.

Anyone learning Haskell, Scala, ML, or another typed functional language can probably assign a type to a short term without much thought. In our hypothetical syntax, it would be trivial to say `1 : Int`

and `add 1 : Int -> Int`

. If we go a little further and start giving types their own types, we enter the realm of Kinds.

For example, it's pretty obvious that the type of `Int`

is going to be `Type`

. Somewhat confusingly at first, `Int -> Int`

is not `Type -> Type`

, but rather `Type`

(since the type is not a function in and of itself, but rather a single term). It may make sense to assign a type to `(->)`

at this point, which we could make `Type -> Type -> Type`

. Notice how the standard types we talk about (`Int`

, `Float -> Int`

, `(Int, String)`

) all fall under the simple `Type`

. This is probably weird at first... if we put all types into the same category, what's the use of categorizing them? Even seeing a kind given for `(->)`

doesn't help us out much, as it's just some magical operator that's guaranteed to make sense.

The reason we have for categorizing existing types is in fact due to HKTs. While `List Int : Type`

isn't a very useful statement, `List : Type -> Type`

is a bit more interesting. Of course, it's not useful to think of `List`

here in terms of its values... we aren't planning on writing a function of `(Type -> Type) -> Int`

or anything of the sort. Where it gets interesting is when you write generic code. Let's start with a simple example:

```
f : forall (c : Type -> Type), (a : Type), (b : Type).
c a -> c b
```

Let's not get caught up over the details of defining such a function, but as an exercise it's useful to analyze this type. First of all, you'll notice the rather drawn out `forall`

clause. In particular, it's worth noticing the fact that we give the type variables their own types. This is important, because it allows us to make `c`

a higher-kinded type here (alternatively, something with more complexity than `Type`

alone). Also, try to think of some examples for `c`

here: some good ones include `List`

and `Option`

(or `Maybe`

); an invalid example might be `Map`

(which is `Type -> Type -> Type`

, since we would normally write `Map Int String`

).

Now that we've got this basic example in mind, let's think of somewhere we can actually use this concept. We all know parametric polymorphism allows us to write things like functions that can operate on any kind of list (`List a -> (a -> b) -> List b`

being the type of `map`

). But it's quite hard to relate higher-kinded types as we've seen them so far to any sort of real-world code. In fact, HKTs alone are of little use. It's not until we enter a language with some kind of ad-hoc polymorphism that we can even really use them. To be language-agnostic, I'll define my own system for ad-hoc polymorphism below:

`a -> b | a, b < Number`

means "a function from `a`

to `b`

, where `a`

and `b`

inherit from the interface `Number`

." Less general types would include `Int -> Int`

and `Float -> Int`

in this case.

For our own use, we will create an interface called `MapFn`

. This interface can be inherited by any type with a corresponding `map`

function. Let's write a few of these:

```
inherit MapFn for List
with map f [] = []
map f (x::xs) = f::(map f xs)
inherit MapFn for Option
with map f None = None
map f (Some x) = Some (f x)
```

With both `List`

and `Option`

available, it's useful to see some places where it might be helpful to have both within reach without forcing us to rewrite a function each time. For example, `mapTwice`

might perform `map`

with 2 different functions in a row. Rather than writing a whole interface and its implementations for `MapTwiceFn`

, let's try to write this using HKTs.

First of all, we know our function `mapTwice`

is going to have a few type variables: `x`

, the original type contained by the List/Option; `y`

, the result of the first `map`

and input to the second `map`

; `z`

, the result of the second `map`

; and `c`

, the container to be mapped over (which must either be List or Option). It's also quite easy to write the function itself:

```
let mapTwice f g xs =
let ys = map f xs
map g ys
```

Next, we can start to assign types to the individual variables. Let's refine this function:

```
let mapTwice (f : x -> y) (g : y -> z) (xs : c x) =
let ys : c y = map f xs
map g ys : c z
```

Finally, let's put together everything we know and give the whole function its type:

`mapTwice : (x -> y) -> (y -> z) -> c x -> c z`

And how do we know what `c`

is?

```
mapTwice : forall (x : Type), (y : Type), (z : Type), (c : Type -> Type).
(x -> y) -> (y -> z) -> c x -> c z
| c < MapFn
```