Why Haskell?
https://www.gtf.io/musings/why-haskellHaskell doesn't prevent endless recursion. (try e.g. `main = main`)
As the typed FP ecosystem is moving towards dependent typing (Agda, Idris, Lean), this becomes an issue, because you don't want the type checker to run indefinitely.
The many ad-hoc extensions to Haskell (TypeFamilies, DataKinds) are tying it down. Even the foundations might be a bit too ad-hoc: I've seen the type class resolution algorithm compared to a bad implementation of Prolog.
That's why, if you like the Haskell philosophy, why would you restrict yourself to Haskell? It's not bleeding edge any more.
Haskell had the possibility of being a standardized language, but look at how few packages MicroHS compiles (Lennart admitted to this at ICFP '24[0]). So the standardization has failed. The ecosystem is built upon C. The Wasm backend can't use the Wasm GC because of how idiosyncratic GHC's RTS is.[1]
So what does unique value proposition does GHC have left? Possibly the GHC runtime system, but it's not as sexy to pitch in a blog post like this.
[0]: Lennart Augustsson, MicroHS: https://www.youtube.com/watch?v=uMurx1a6Zck&t=36m
[1]: Cheng Shao, the Wasm backend for GHC: https://www.youtube.com/watch?v=uMurx1a6Zck&t=13290s
I went through Software Foundations [0] (Coq) which was fun and interesting but I can't say I ever really applied what I used there in software (I did get more comfortable with induction proofs).
You're mentioning Lean with Agda and Idris - is Lean usable as a general purpose language? I've been curious about Lean but I got the impression it sort of steps away from Haskell's legacy in terms of syntax and the like (unlike Agda and Idris) so was concerned it would be a large investment and wouldn't add much to what I've learned from Coq.
I'd love any insights on what's a useful way to learn more in the area of dependent types for a working engineer today.
I'm not using Haskell because it's bleeding edge.
I use it because it is advanced enough and practical enough. It's at a good balanced spot now to do practical things while tapping into some of the advances in programming language theory.
The compiler and the build system have gotten a lot more stable over the past several years. The libraries for most production-type activities have gotten a lot more mature.
And I get all of the above plus strong type safety and composability, which helps me maintain applications in a way that I find satisfactory. For someone who aims to be pragmatic with a hint of scholarliness, Haskell is great.
In the essay, I didn't say "Haskell is the only thing you should use", what I said was:
> Many languages have bits of these features, but only a few have all of them, and, of those languages (others include Idris, Agda, and Lean), Haskell is the most mature, and therefore has the largest ecosystem.
On this:
> It's not bleeding edge any more.
"Bleeding edge" is certainly not something I've used as a benefit in this essay, so not really sure where this comes from (unless you're not actually responding to the linked essay itself, but rather to ... something else?).
The point is that programming in a pure language with typed side effects and immutable data dramatically reduces the size of the state space that must be reasoned about. This makes programming significantly easier (especially over the long term).
Of the languages that support this programming style Haskell remains the one with the largest library ecosystem, most comprehensive documentation, and most optimised compiler. I love lean and use it professionally, but it is nowhere near the usability of Haskell when it comes to being a production ready general purpose language.
I'm not really sure where the borders of "the typed FP language ecosystem" would be but feel pretty certain that such a thing would enclose also F#, Haskell, and OCaml. Any one of which has more users and more successful "public facing" projects than the languages you mentioned combined. This is not a dig on those languages, but they are niche languages even by the standards of the niche we're talking about.
You could argue that they point to the future but I don't seriously believe a trend among them represents a shift in the main stream of functional programming.
Because it has a robust and mature ecosystem that is more viable for mainstream commercial use than any of the other "bleeding edge" languages.
First of all, does ecosystem move to dependent types? I think the practical value of Hindley-Milner is exactly in the fact that there is a nice boundary between types and terms.
Second, why would type checking running indefinitely be a practical problem? If I can't prove a theorem, I can't use it. The program that doesn't typecheck in practical amount of time is in practice identical to non-type-checked program, i.e. no worse than a status quo.
Do you mean to say Haskell hasn't solved the halting problem yet?
THIS - and none of the other things cited in the article - is the main reason why Haskell is getting no traction in the real world.
The syntax is an abomination, and worse, IMO pretty much unnecessary. The ideas of the language are interesting, and could be expressed in a much more familiar syntax which would be a huge win for the language (although the convoluted hoops you have to jump through when you truly and actually need to mutate data would still be a sheer nightmare).
Haskell's syntax is exactly what keeps it niche and academic, except for the happy few who have managed to twist their brain into being able to parse that grotesque syntax.