Hacker News new | past | comments | ask | show | jobs | submit
> We can generalise this idea of being forced to handle the failure cases by saying that Haskell makes us write total functions rather than partial functions.

Haskell 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

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/

loading story #41525223
loading story #41520713
loading story #41521318
loading story #41523205
loading story #41522938
loading story #41527792
> 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.

loading story #41522068
loading story #41530325
> 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.

loading story #41527613
loading story #41526321
> 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.

loading story #41526520
> 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.

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

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

loading story #41529566
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.
loading story #41527455
loading story #41519486
loading story #41518959
loading story #41522355
loading story #41519406
loading story #41519643
loading story #41519079
loading story #41519451
loading story #41519002
loading story #41525287
loading story #41519694
loading story #41519892
loading story #41520998
loading story #41529507
loading story #41521764
loading story #41519893
loading story #41519720
loading story #41529066
loading story #41519348
loading story #41523476
loading story #41530256
loading story #41534463
> Since the syntax is quite distant from C-like syntax

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.

loading story #41523477
loading story #41525788
loading story #41533124
loading story #41527166
loading story #41519150
loading story #41527164
loading story #41523940
loading story #41523026
loading story #41522889
loading story #41523534
loading story #41525346
loading story #41522169
loading story #41528483
loading story #41533747
loading story #41520295
loading story #41523040
loading story #41519656
loading story #41528426
loading story #41522945
loading story #41521255
loading story #41519072
loading story #41519094
loading story #41520689
loading story #41519321
loading story #41519536