[HN Gopher] Understanding higher-kinded types
___________________________________________________________________
Understanding higher-kinded types
Author : dan-so
Score : 53 points
Date : 2022-03-01 15:26 UTC (7 hours ago)
(HTM) web link (danso.ca)
(TXT) w3m dump (danso.ca)
| alexashka wrote:
| 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.
| edude03 wrote:
| 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 wrote:
| 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.
| dwohnitmok wrote:
| > 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).
| adamgordonbell wrote:
| 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.
| wk_end wrote:
| 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.
| estebank wrote:
| 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.
| _zachs wrote:
| Agreed! I was excited because I thought I was going to get a
| better explanation of Foldable than what the linked docs
| provide!
| dwohnitmok wrote:
| `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.).
| CobrastanJorji wrote:
| 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.
| dwohnitmok wrote:
| 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).
| dwohnitmok wrote:
| Whoops: intIsIncrementable : Incrementable<a>
|
| should be intIsIncrementable :
| Incrementable<Int>
___________________________________________________________________
(page generated 2022-03-01 23:02 UTC)