Live data from Hacker News

Understanding higher-kinded types

danso.ca

11–16 of 16 posts

Re: Understanding higher-kinded types

#11
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.

Re: Understanding higher-kinded types

#12
post #10

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.

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.

Re: Understanding higher-kinded types

#13
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 incrementFlo…

Whoops:

  intIsIncrementable : Incrementable
should be

  intIsIncrementable : Incrementable

Re: Understanding higher-kinded types

#14
post #10

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.

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

Re: Understanding higher-kinded types

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