> but none of these languages have much foundation in category theory or the ambitious kind of type system that Haskell has been pioneering for a while.
Is that a requirement? If so, why?
Is that a requirement? If so, why?
Having used a system with higher-level type constructs I find myself thinking in them. So many complex sequences of operations shake out as something much simpler once you realise the right monad, or arrow, or so on. And it becomes painful to manually expand it out; it would be like working in a language without generics. So I couldn't stand to work in a language that can't express these concepts; I need either higher-kinded types or something equivalent to them.
And for a type system that powerful, I'd want some assurance it was correct. Theoretical underpinnings are not the only way to do that - if it had been in use a while, and had enough tests and experience to give me a decent level of confidence, that would be enough. But for a new language I think the only way I could be confident enough to use it would be if it had this kind of theoretical backing.
FWIW it seems that many of the Rust developers want this for Rust.
However, the Rust team is trying to get 1.0 out the door, and higher-kinded types would be backwards compatible, so I don't think we'll be seeing them for a while. There's also questions about the overhead and syntax that would need to be resolved for them to make it in.
I have no idea if a similar problem is possible with Rust, but it'll be interesting to see how HKTs enter the scene if and when they do.