Yeah. Built up really well, made sure everybody was on the same place, and then just stopped right when it was getting to the thing I thought it was going to explain.

A (Rust) example of why HKTs would be useful is if you have a user-defined container that want's to abstract between having an Rc or an Arc, so that people can pay or not the cost of thread safety.

A more immediate example of where these are useful are in async Rust: being able to represent HKTs is necessary to allow a trait to hold an async fn, which gets desugared to a function returning an associated type that implements Future<Output = T>. This is being worked on.

The most common case you'll see higher-kinded types show up is if you're trying to allow for abstraction over operations without resorting to inheritance.

For example, let's say you have several different types that all have a notion of add:

  type Int

  incrementInt : Int -> Int

  incrementByTwoInt : Int -> Int
  # You'll probably implement this as incrementByTwoInt(x) = incrementInt(incrementInt(x))

  type Float

  incrementFloat : Float -> Float

  incrementByTwoFloat : Float -> Float
  # You'll probably implement this again as incrementByTwoFloat(x) = incrementFloat(incrementFloat(x)), notice the duplication

If you had inheritance, you could remove the duplicate definitions of `incrementByTwo` by making an `Incrementable` parent and have `Float` and `Int` both inherit from `Incrementable` and then make `incrementByTwo` just take an `Incrementable`. But this has several annoying problems that come from inheritance. Since I don't want to get dragged into a long discussion about the pros and cons about inheritance, I'll just mention one reason to motivate why you'd want to use something other than inheritance: by using `Incrementable` via inheritance, it must have existed when `Float` and `Int` were themselves written. This is very annoying if you want to abstract over behavior of `Float` and `Int` after the fact (e.g. maybe `Float` and `Int` exist in separate libraries, or maybe they never provided `Incrementable` to begin with and you want to make a third-party library to add this functionality).

So instead we could use store the function directly in data to abstract the behavior instead.

  type Incrementable<a> =
    {  increment : a -> a
    }

  intIsIncrementable : Incrementable<a>
  intIsIncrementable =
    { increment = incrementInt
    }

  floatIsIncrementable : Incrementable<Float>
  floatIsIncrementable =
    { increment = incrementFloat
    }

  incrementByTwo : (Incrementable<a>, a) -> a
  incrementByTwo(incrementable, x) = incrementable.increment(incrementable.increment(x))

Then we can recover our individual `Float` and `Int` versions by just passing in the respective `intIsIncrementable` and `floatIsIncrementable` values, instead of writing duplicate `incrementByTwo` functions that share the exact same function bodies.

So far so good, but what happens with collections?

  type Array<a>

  head : Array<a> -> a
  # Get the first element, for simplicity we'll just crash on an empty collection

  compareTwoHeads : (Array<a>, Array<a>) -> Boolean
  # Assume all values are always comparable with ==
  compareTwoHeads(collection0, collection1) = head(collection0) == head(collection1)

  type List<a>

  head : List<a> -> a
  # Again get the first element

  compareTwoHeads : (List<a>, List<a>) -> Boolean
  # Assume all values are always comparable with ==
  compareTwoHeads(collection0, collection1) = head(collection0) == head(collection1)

If we want to do the same trick so that we don't duplicate our definition of `compareTwoHeads` we'd write something like

  # c is for collection
  type Headable<c> =
    { head : c<a> -> a
    }

But that requires `Headable` to be a higher-kinded type, because now `c` is not a concrete type such as `Int` or `Float`, but is itself a type constructor, that takes another type as an argument, which is why `head` has `c<a>` appear in it. That's the only way we could write something like

  Headable<Array>

or

  Headable<List>

Without the ability to write something like `c<a>` where both `c` and `a` are generics, i.e. higher-kinded types, we can't create `Headable` so we're forced to duplicate `compareTwoHeads` and can't abstract out a common function body, or our language must support inheritance (but even doing this through inheritance has its own set of problems).

Whoops:

  intIsIncrementable : Incrementable<a>

should be

  intIsIncrementable : Incrementable<Int>

Agreed! I was excited because I thought I was going to get a better explanation of Foldable than what the linked docs provide!

`Foldable` is basically the FP equivalent of `Iterable` in Java if you're familiar with that. It's an abstraction you can write against if you want to support all sorts of data structures that can be iterated on (e.g. arrays, lists, trees, etc.).