Hopefully someday, but nothing is free until someone comes up with a zero-cost abstraction, and in the meantime Haskell relies on a garbage collector.

Thank you for the link, I enjoyed it a great deal!

There's no reason monad shouldn't be a zero-cost abstraction, to the same extent as any other trait (i.e. using them in cases where the type is not statically known would require boxing, but the abstraction is not really a cost overhead in that case since you simply couldn't write that code at all without it).

Haskell currently uses a garbage collector, as do most languages that we could look to for inspiration, but I don't see that that's an essential barrier. The part I would be worried about doing in the presence of a borrow checker would be being able to form first-class functions, especially closures, but Rust already has those! AFAICS the only other "hard" part is having higher-kinded types and preserving good type inference, but the solution to that is already known (Hindley-Milner).

I didn't look deep enough to be confident, but I don't understand Rust's issue with do notation.

It already has monads, and uses them in a lot of places. Do notation is just syntax sugar.

Here's one simple part of this very large and thorny problem: each of Rust's monad instances does not share the same type signature, even for similar methods. This is because Rust has more novel features that appear in type signatures.

To reduce the problem to a simpler (but useful) one: what would it take to be able to write a generic "compose" function (on function values) that would be polymorphic across at least Fn/FnMut/FnOnce? This is something that people already write the specific versions of; obviously the general version requires some form of HKT, but it's not clear (at least to me) what's blocking that.

When I've seen discussions of HKT in Rust it feels like there's an awkward circularity where if you talk about HKT people say the use cases aren't there, but if you talk about things that need HKT people say they can't be implemented because they need HKT. And I'm worried that the conversation about extending the type system has reached a place where adding ad-hoc special cases is seen as the "cautious" approach, when the result is a funny subset of a more general system that's both more complex and less powerful than biting the bullet and implementing the general system.

I am not an expert in this area, but the problem is that these things all have very different kinds of permissions, in a sense... I'm not sure what being polymorphic over ownership looks like.

I don't think that anyone who understands this stuff deeply denies that there's good use cases for HKT. There's just not a design, and we're not sure that one actually exists. And a general perception that GATs will give us most of the big benefits of HKT in a way that feels more Rust-like. That being said, there have been a few attempts at this. We'll see.

Being polymorphic over ownership is the most important problem Rust should be looking to solve, IMO: it would make a lot of other problems trivial. I don't necessarily think it's easy, but I do think it's tractable.

The choice to focus on GATs is exactly what I was thinking of. I think Rust will come to regret it, as it comes with most of the costs of full HKT but leads one into working with a limited subset that's not so theoretically well-founded, and I'm not convinced the forward-compatibility is as good as claimed (the semantics may extend to full HKT, but it pushes syntax in a direction that seems likely to make for a frustrating syntax for full HKT). I hope it ends up working out.

How are GATs any less theoretically well founded than HKT?

I can see how maybe working toward that would be a priority in a PLT research sense, but Rust isn't that kind of language anymore. (This is my own opinion and I'm not on the lang team, mind you.)

> How are GATs any less theoretically well founded than HKT?

I'm not aware of their having been studied to the same extent, so I don't have the same level of confidence that they are well-behaved. For example, is there a known algorithm for doing perfect type inference in the presence of GAT? What about when we add in subtyping, or higher-rank types? Maybe it's all going to be fine, but the further you stray from the path that's been trodden by PLT research, the more I'd worry about falling down a hole.

Gotcha. My understanding was that they were, but not my area of expertise.