For a long time already I've wanted to make the leap towards learning dependently typed programming, but I was never sure which language to invest in - they all seemed either very focused on just proofs (Coq, Lean) or just relatively far from Haskell in terms of maturity (Agda, Idris).

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.

[0] https://softwarefoundations.cis.upenn.edu/

> why would you restrict yourself to Haskell? It's not bleeding edge any more.

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.

> That's why, if you like the Haskell philosophy, why would you restrict yourself to Haskell?

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?).

> 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.

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.

> As the typed FP ecosystem is moving towards dependent typing (Agda, Idris, Lean)

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.

> That's why, if you like the Haskell philosophy, why would you restrict yourself to Haskell? It's not bleeding edge any more.

Because it has a robust and mature ecosystem that is more viable for mainstream commercial use than any of the other "bleeding edge" languages.

> 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.

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.

>Haskell doesn't prevent endless recursion. (try e.g. `main = main`)

Do you mean to say Haskell hasn't solved the halting problem yet?

Uhh, endless recursion doesn't cause your typechecker to run indefinitely; all recursion is sort of "endless" from a type perspective, since the recursion only hits a base case based on values. The problem with non-well-founded recursion like `main = main` is that it prevents you from soundly using types as propositions, since you can trivially inhabit any type.