Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Understanding higher-kinded types

danso.ca

Post reply on HN
Print view View original

1–10 of 16 posts

Re: Understanding higher-kinded types

#2

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

Re: Understanding higher-kinded types

#3

Post by 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.

Re: Understanding higher-kinded types

#4

Post by CobrastanJorji »

wk_end wrote: post #3

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 brea…

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.

Re: Understanding higher-kinded types

#5

Post by _zachs »

wk_end wrote: post #3

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 brea…

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

Re: Understanding higher-kinded types

#6

Post by estebank »

wk_end wrote: post #3

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 brea…

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. This is being worked on.

Re: Understanding higher-kinded types

#7

Post by dwohnitmok »

wk_end wrote: post #3

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 brea…

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 =
    {  increment : a -> a
    }

  intIsIncrementable : Incrementable
  intIsIncrementable =
    { increment = incrementInt
    }

  floatIsIncrementable : Incrementable
  floatIsIncrementable =
    { increment = incrementFloat
    }

  incrementByTwo : (Incrementable, 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

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

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

  type List

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

  compareTwoHeads : (List, List) -> 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 =
    { head : c -> 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` appear in it. That's the only way we could write something like

  Headable
or

  Headable
Without the ability to write something like `c` 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).

Re: Understanding higher-kinded types

#8

Post by dwohnitmok »

_zachs wrote: post #5
wk_end wrote: post #3

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 brea…

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

Re: Understanding higher-kinded types

#9

Post by 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.

Re: Understanding higher-kinded types

#10

Post by 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.
Post reply on HN