Understanding higher-kinded types

[dwohnitmok]

> Examples include Foldable, Traversable, Functor, and Monad

This wording is confusing. Generally we don't think of Foldable, Traversable, Functor, and Monad as higher-kinded types themselves, they are typeclasses on type constructors. That is `Monad(List)` is not itself a type. This is especially true in Haskell, which is where the links for those typeclasses go to.

This is less true for e.g. Scala, where `Monad[List]` is indeed technically another type, even if it's not usually used as such.

However various reifications of those typeclasses are indeed examples of higher-kinded types (e.g. `Free`, the free monad).

[keithalewis]

The older I get the more I appreciate the wisdom of people who lived before me. When I believe I've finally managed to figure something out that I hope others will find worthwhile and put together the bibliography, I have to confess I don't actually read most of the citations. It is impossible to read all of them carefully. When I make the effort to do that I find wide variation in the information content. The Bell Curve is a real thing, whether it comes to how fast humans can run or how clearly they can think. There is no stopwatch to measure thinking. I rely on other people I've met over the years who's judgement I trust to help me not waste time sifting through the riffraff. One technique is qualification. If the OP hasn't done their diligence in understanding the lambda cube then my default is to assume they wrote this in an attempt to clarify their limited understanding, just like I am guilty of. On a positive note, I recently learned here about the Kind language. It is still under development, but it has a radically simple approach to dependent types that makes it much easier to understand than Haskell.

[alexashka]

Meh, it's like this:

You have values. Then you have types.

You can modify values, you can't modify types. If you want to modify types, then you need a third thing, let's call it 'kinds'.

Then if you want to modify kinds, then you need a forth thing. That's when you realize oh, why not just have types be same as values - you've now arrived at dependent types :)

If you're curious about this sorta thing - play with Idris (the language) for a few days. It's the most approachable dependent type system in a friendly package that I've seen.

[wk_end]

This post spends most of its time explaining types and kinds in general, and very little time explaining much about higher-kinded types or why they're useful - it just kinda rattles off a list of a few at the end. Really exploring one of those examples, why it's useful, why they need higher-kinded type support, how you'd get the job done without them, would have made this feel much more complete.

Also: end notes break the flow of reading - I have to click on it, the whole page changes due to scroll, I have to find the end note I clicked on, then I have to click back and find my place again - so I feel pretty annoyed when they add very little or could have been just a parenthetical, the way notes 3-7 inclusive (and especially 4-7 inclusive) do here.

[CobrastanJorji]

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.

[estebank]

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.

[dwohnitmok]

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

[_zachs]

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

[edude03]

Thanks to the author for sharing this. I do want to learn more about HKTs but I feel like this article is written for people who already know what HKTs are. It gives me the same feeling as “Monads are just monoids in the category of endofunctors” - great but if I’m googling “what is a HKT” I probably don’t know about set theory or domain theory.

[whatshisface]

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.

[azurelake]

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.

[adamgordonbell]

HKT is a cool concept. I'm super rusty on them but they always just seemed one step up from generics.

From ArrayList to List[A] is a cool step, but what if you want to define something generic over the container, a L[A] : Foldable where L could be a List[A] or a Tree[A] or a IO[A] action, as long as they implement Foldable.

Then if they implement Foldable you can access lots of std lib things that require a Foldable (or Traversable or Functor or whatever)

It gives you a lot of abstractive power to be able to write operations in terms of Foldable or other HKTs and then share them among many specific instances.

It's sort of like being able to define things like Iterable or IEnumerable but from a polymorphism perspective rather than an inheritance one.

[eternityforest]

It's amazing how you can use this stuff every day for years but be completely lost when it comes to the theory, or even the slightly more math heavy practice.