Understanding higher-kinded types

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.

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

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).

HKTs only stick out when you're in a rigidly structured programming environment where the compiler has to understand what you're writing. In old-fashioned static languages, the following is impossible, while in Python it's unremarkable:

  def class_closure(x):
    class A(object):
      def tell_me_x(self):
        return x
    return A

Then,

class_closure(7)().tell_me_x() => 7

This is just a weird pattern (with some rare uses) in Python, but in a strictly typed language, you're going to have to be able to express what the signature of class_closure is. In this case, it'd be something like,

class_closure: Int -> Type

The signature is a type that refers to, within itself, the concept of types. That makes it "higher-kinded." Before researchers got a grip on the theory surrounding this, you could only have either languages where that was impossible, or languages that gave up on static type checking entirely.

It's just a fancy way of saying you can use generics for the "outer" type of a container. e.g. List<T> vs. U<T>. That's literally all there is to it.