Higher-Kinded Types (HKT)

[Heimdell]

Problem

At the moment, Gleam only supports type variables which are simple types, not generics themselves. Therefore, you cannot abstract over a generic.

Proposition

It is possible to introduce HKT into the language without changing existing userspace code. I'd like to fork and try adding HKTs into the language.

The PROs of the change are:

• All the existing code should still compile and have its semantics unchanged.
• The language of types becomes more powerful.
• HKT will synergize with typeclasses/implicits greatly, enabling very powerful abstractions.
• You can write and use map, foldr and other operations that abstract over container type.

The CONs are:

• The code becomes a bit more indirect, when this feature is used.
• The size of typechecker grows up.

Syntax changes

1. Allow type variables to be in function position in the type application;
2. add a reserved name for kind of ground types - probably Type;
3. allow kind signatures.

Here is a piece of code demonstrating all changes:

// An example type to be used as `layer`
//
pub type LambdaCalc_(self) {
  Var(name : Name),
  Fun(args : List(Name), body : self),
  App(callee : self, args : List(self))
}

// The signature here is not necessary, it is totally inferrable.
//
// By default, type argument is assumed to be a simple type.
//
pub type Tree (info: Type, layer: Type -> Type) {
  Tree (info: info, siblings: layer (Tree (info, layer))
}

pub fn foldTree (algebra : fn (info, layer (res)) -> res, tree : Tree (info, layer)) : res {
  ...
}

pub type LambdaCalc = Tree(Position, LambdaCalc_)

Implementation

Currently, the "kind-check" is implemented as comparison of formal argument count and real argument supplied. I plan to add a proper kind-check.

There are 2 ways to do it that I know, which I need your help to select:

Add a separate notion of kind

This way we can say that each value has a type value: type and each type has kind type : kind.
I propose two syntactic forms in this case:

1. Type or * - a kind of types, that can have a value, like Int, String, List(Int) and so on;
2. k1 -> k2 - a kind of type functions, where k1 and k2 are kinds, like List : Type -> Type.

PROs:

• Reliable way, was used in haskell for a long time.

CONs:

• I would need a separate unifier for kinds.

Type : Type

In this case, we say that types have types, not kinds, and add Type, a type of all types.

CONs:

• We well be able to accept types as value-level arguments: pub fn id (a : Type, x : a);
• They should be erased before codegen;
• They may or may not require us to disable them.

PROs:

• We reuse unifier from typecheck.
• If we later want to have visible type application id(@Int, 1), we just enable them back.

Conclusion

I'd like any feedback about those methods, the syntactic changes and the HKT itself.

[lpil]

Hello, thanks for your thorough proposal.

One thing I am interesting in when considering extension to the language is the impact it will have on the ergonomics of the language. Having HKTs in Gleam would open the door to more sophisticated polymorphism but it is not clear what practical problems this would solve for Gleam programmers.

HKTs would add some amount of complexity to the language which is in tension with Gleam's goal of being simple and easy to learn, so we want a clear reason to accept that complexity.

I would like to collect practical examples of Gleam code which could be improved with HKTs, and we can then compare it to alternative designs and features to see which would be the best improvement for the lowest cost.

[Heimdell]

TL;DR:

1. It should not scare people, because it is hard to notice till you try and find that it is, indeed, possible.
2. The lack of it can scare people, coming from Scala and Purescript.

That would be nice to have before we run into the need of it.

And this is not a thing that sticks in front of the language and "you shall not pass"-es people 'till they learn it. I don't ask to rewriting the stdlib, it would stay unchanged.

Most users will not even notice that this is a thing - and since it generalizes current behaviour, 99.9% of the code will continue to work. I'm leaving 0.1% for those who use name Type, and I can use * instead.

The lack of HKT is a limitation that will prevent some clever stuff from helping people - like functors and applicatives (parsers and validators made using appicatives are very good).

P.S.: The current limitation looks almost artifical.

[lpil]

Yes, we could add this feature without making any breaking changes- existing code can continue to exist as before so there is no difficult migration path.

Let's collect some real examples of how HKTs could be used in Gleam to better understand how this feature would impact Gleam programming and what the practical advantages would be.