~icefox/garnet#62: 
Higher kinded types

I keep going back and forth on these, so it's past time to write some shit down.

Higher kinded types are basically the ability to put generic parameters on generic types. So, you can have some generic type T<U> where both T and U can be generics. IE, the type constructor T also has a type parameter U. This is handy in some cases 'cause you can do things like, for example, write a function that takes a Map<K,V> and then you are able to pass it a HashMap or a BTreeMap. There's more use cases described in this thread: https://users.rust-lang.org/t/does-rust-really-need-higher-kinded-types/5531/3. Part of it is they allow you to make monads and monad-looking structures, so higher level combinators in general get easier.

Rust and F# don't have HKT's, OCaml and Scala do. So you can have a perfectly cromulent language without them. The inspiration for most of the fancier parts of Garnet's type system is OCaml, so departing from that design to strike off on our own feels like it will potentially come back to bite us in the ass.

My original intention was to not have HKT's, 'cause Rust has been trying to add them forever and has not been successful yet. But Rust also has to preserve backwards compatibility. You can also generally fake the things you can do with HKT's with functors, sufficient amounts of trait salad, etc. But also since lifetimes are type parameters, there's some lifetime patterns that are pretty damn hard to write without HKT's.

So it comes down to ye olde cost-benefit tradeoff. Benefits:

  • If you don't need them they don't add extra work for you
  • Simplifies complex code, a little
  • Might turn some unsafe code hacks safe
  • Could be a big win for low cost if they're put in early

Costs:

  • More complicated compiler (how much though?)
  • Significantly slower typechecking??? Find out.
  • Does it require more global analysis of stuff or codegen that is impossible to parallelize??? Find out.
  • You could just hardwire the most useful bits of their functionality into the language if you really want to, or generate them with macros.
Status
REPORTED
Submitter
~icefox
Assigned to
No-one
Submitted
7 months ago
Updated
7 months ago
Labels
T-DESIGN

~icefox 7 months ago

Enhancing standard-ish HM with HKT's, by mbones: https://gist.github.com/mb64/307c8344f3663b04257faa0c359556fd

Arguments against HKT's in Roc: https://github.com/roc-lang/roc/blob/main/FAQ.md#why-doesnt-roc-have-higher-kinded-polymorphism-or-arbitrary-rank-types (not all of which are applicable to Garnet)

Why Rust wants HKT's: https://users.rust-lang.org/t/does-rust-really-need-higher-kinded-types/5531

Basically, being able to express Foo<Bar> where both Foo and Bar are generics is useful for borrow checking, since lifetimes are generic types anyway. So if you have HKT's you can write fn foo<T>(thing: &'a T) -> T::Item<'a>. Which is a pretty compelling use case for Garnet too.

I wonder how the heck you compile HKT's. Monomorphize like normal, I guess? Apparently so.

Register here or Log in to comment, or comment via email.