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/

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?

Would you recommend using cabal or stack to package Haskell components in a Yocto layer, for sandboxed, reproducible, cross-compiled builds that are independent of host toolchains?

I’m personally quite interested in the Koka language. It has some novel ideas (functional-but-in-place algorithms, effect-handler-aware compilation, it uses reference counting rather than garbage collection) and is a Microsoft Research project. It’s starting to look more and more like an actual production-ready language. I can daydream about Microsoft throwing support behind it, along with some tooling to add some sort of Koka-Rust interoperability.

`-fdefer-type-errors` will report those errors as warnings and fail at runtime, which is good when writing/refactoring code. Even better the Haskell LSP does this out of the box.

> * The tooling, although significantly better than it was, is still poor compared to other some other functional languages, and really poor compared to mainstream languages like C#

Which other functional programming languages do you think have better tooling? Experimenting lately with OCaml, feels like Haskell's tooling is more mature, though OCaml's LSP starts up faster, almost instantly.

- The Haskell ecosystem doesn't have the budget of languages like Java or C# to build its tooling.

- The haskell ecosystem was innovative 20 years ago, but some newer languages like Rust or Elm have much better ergonomics due to learning from their forebearers.

Yes, it's true. And it's true for almost any smaller language out there.

I'd love to know which things specifically you're thinking about. For what we've been building, the "integration" libraries for postgres, AWS, etc. have been fine for us, likewise HTTP libraries (e.g. Servant) have been great.

I haven't _yet_ encountered a library problem, so am just very curious.

I'm also curious about the slowness of compilation and whether that's intrinsic to the design of GHC.

Sort of. It has a "failure at a stage prevents progress to next stage", so a parse error means you won't type check (or indeed, continue parsing). See these proposals for some progress on the matter

* https://github.com/haskellfoundation/tech-proposals/pull/63

* https://github.com/ghc-proposals/ghc-proposals/pull/333

Depends on which mainstream languages one compares with; there's always C++.

My project here has 50k lines Haskell, 10k C++, 50k lines TypeScript (code-only, not comments). Counting user CPU time (1 core, Xeon E5-1650 v3 3.50GHz):

    TypeScript 123 lines/s
    Haskell     33 lines/s
    C++          7 lines/s

  All mainstream, general purpose programming languages are (basically) Turing-complete, and therefore any programme you can write in one you can, in fact, write in another. There is a computational equivalence between them. The main differences are instead in the expressiveness of the languages, the guardrails they give you, and their performance characteristics (although this is possibly more of a runtime/compiler implementation question).

The syntax summary in the article is really good. Short and clear.

Out of curiosity does this also hold true for F#?

From everything I've ready about people's experiences with using Haskell for large projects, it sounds like lazy evaluation unfortunately adds more problems than it removes.

I’m not sure I’m experienced enough in PLT enough to have a strong opinion myself.

However, from experience, laziness has a lot of advantages both from a program construction and performance perspective.

This is quite the claim. I know plenty of experienced and productive Haskellers who disagree with this (myself included)

(Of course a small minority of people don't consider laziness as a mistake as it enables equational reasoning; let's not go there.)

Use modules as your basic unit of abstraction. Don’t go out of your way to make their organization over-engineered, but each module should basically do one thing, and should define everything it needs to do that thing (types, classes, functions).

Use parametric polymorphism as much as you can, without making the code too hard to read. Prefer functions and records over type classes as much as possible. Type classes that only ever have a single instance, don’t have laws, or type classes defined for unit data types are major code smells.

Don’t worry about avoiding IO, but as much as you can try to keep IO code separate from pure code. For example, if you need to read a value from the user, do some calculations, then print a message, it’s far better to factor the “do some calculations” part out into a pure function that takes the things you read in as arguments and returns a value to print. It’s really tempting to interleave logic with IO but you’ll save so much time, energy, and pain if you avoid this.

Essentially, keep things as simple as you can without getting belligerent about it. The type system will help you a lot with refactoring.

Start at the beginning. Write functions. When you see some piece of functionality that you need, use `undefined` to make a placeholder function. Then, go to your place holder and start implementing it. Use undefined to fill in bits that you need, and so on.

Fancy types are neat but it’s easy to end up with a solution in search of a problem. Avoid them until you really have a concrete problem that they solve- then embrace them for that problem (and only that problem).

You’ll refactor a lot, and learn to have a better gut feeling for how to structure things, but that’s just the process of gaining experience. Leaning into the basics of FP (pure functions, composed together) will be the path of least resistance as you are getting there.

1. Decide on an effect system

Remember, Haskell is pure, so any side-effect will be strictly explicit. What broad capabilities do you want? Usually, you need to access some program-level configuration (e.g. command-line options) and the ability to do IO (networking, reading/writing files, etc), so most people start with that.

https://tech.fpcomplete.com/blog/2017/06/readert-design-patt...

2. Encode your business logic in functions (purely if possible)

Your application does some processing of data. The details don't matter. Use pure functions as much as possible, and factor effectful computations (e.g. database accesses) out into their own functions.

3. Glue everything together in a monadic context

Once you have all your business logic, glue everything together in a context with your effect system (usually a monad stack using ReaderT). This is usually where concurrency comes in (e.g. launch 1 thread per request).

---

Beyond this, your application design will depend on your use-case.

If you are interested, I strongly suggest to read 'Production Haskell' by Matt Parsons, which has many chapters on 'Haskell application structure'.

There are still plenty of ways to do things wrong. Strong types don't prevent that. Laziness is a double-edged sword and can be difficult to reason about.

I am one of these people.

People are much more reluctant to share what it is that led them to the conclusion that Haskell isn't something they want to use professionally, or something they can't use professionally. It's a combination of things, such as it just generally being less energizing to talk about that, and also some degree of frankly-justified fear of being harassed by people who will argue loudly and insultingly that you just Don't Get It.

I am not one of those people.

I will share the three main reasons I don't even consider it professionally.

First, Hacker News has a stronger-than-average egalitarian streak and really wants to believe that everybody in the world is already a developer with 15 years of experience and expert-level knowledge in all they survey from atop their accomplished throne, but that's not how the real world works. In the real world I work with coworkers who I have to train why in my Go code, a "DomainName" is a type instead of just a string. Then, just as the light bulb goes off, they move on from the project and I get the next junior dev who I have to explain it to. I'm hardly going to get to the point where I have a team of people who are Haskell experts when I'm explaining this basic thing over and over.

And, to be 100% clear, this is not their "fault", because being a junior programmer in 2024 is facing a mountain of issues I didn't face at their age: https://news.ycombinator.com/item?id=33911633 I wasn't expected to know about how to do source control or write everything to be rollback-able or interact with QA, or, well, see linked post for more examples. Haskell is another stack of requirements on top of a modern junior dev that is a hell of an ask. There better be some damn good reasons for me to add this to my minimim-viable developer for a project. I am not expressing contempt for the junior programmers here from atop my own lofty perch; I am encouraging people to have sympathy with them, especially if you also come up in the 90s when it was really relatively easy, and to make sure you don't spec out projects where you're basically pulling the ladder up after yourself. You need to have an onboarding plan, and "spend a whole bunch of time learning Haskell" is spending a lot of your onboarding plan currency.

Second, while a Haskell program that has the chef's kiss perfect architecture is a joy to work with, it is much more difficult to get there for a real project. When I was playing with Haskell it was a frequent occurrence to discover I'd architected something wrong, and to essentially need to rewrite the whole program, because there is no intermediate functioning program between where I was and where I needed to be. The strength of the type system is a great benefit, but it does not put up with your crap. But "your crap" includes things like being able to rearchitect a system in phases, or partially, and still have a functioning system, and some other things that are harder to characterize but you do a lot of without even realizing it.

I'd analogize it to a metalworker working with titanium. If you need it, you need it. If you can afford it, great. The end result is amazing. But it's a much harder metal to work with for the exact same reason it's amazing. The strength of the end part is directly reflected in the metal resisting you working with it.

I expect at a true expert level you can get over this, but then as per my first point, demanding that all my fellow developers become true experts in this obscure language is taking it up another level past just being able to work in it at all.

Finally, a lot of programming requirements have changed over the years. 10-15 years ago I could feasibly break my program into a "functional core" and an external IO system. This has become a great deal less true, because the baseline requirement for logging, metrics, and visibility have gone up a lot, and suddenly that "pure core" becomes a lot less appealing. Yes, of course, our pure functions could all return logs and metrics and whathaveyou, and sure, you can set up the syntax to the point that it's almost tolerable, but you're still going to face issues where basically everything is now in some sort of IO. If nothing else, those beautiful (Int -> Int -> Int) functions all become (Int -> Int -> LoggingMetrics Int) and now it isn't just that you "get" to use monadic interfaces but you're in the LoggingMetrics monad for everything and the advantages of Haskell, while they do not go away entirely, are somewhat mitigated, because it really wants purity. It puts me halfway to being in the "imperative monad" already, and makes the plan of just going ahead and being there and programming carefully a lot more appealing. Especially when you combine that with the junior devs being able to understand the resulting code.

In the end, while I still strongly recommend professional programmers spend some time in this world to glean some lessons from it that are much more challenging to learn anywhere else, it is better to take the lessons learned and learn how to apply them back into conventional languages than to try to insist on using the more pure functional languages in an engineering environment. This isn't even the complete list of issues, but they're sufficient to eliminate them from consideration for almost every engineering task. And in fact every case I have personally witnessed where someone pushed through anyhow and did it, it was ultimately a business failure.

If that's all you want it to do, it's very easy with Wai/Warp.

> - How easy is it to auth a JWT?

We don't use JWTs, but we did look at it and Servant (which is a library for building HTTP APIs) has built in functionality for them.

> - Is there a good ORM that supports migrations?

There are several with quite interesting properties. Some (like persistent) do automatic migrations based on your schema definitions. Others you have to write migration SQL/other DSL.

> - Do I have to remodel half my type system because a product owner told me about this weird business logic edge case we have to deal with?

I think that's going to really depend on how you have structured your domain model, it's not a language question as much as a design question.

> - How do I do logging?

We use a library called Katip for logging, but there are others which are simpler. You can also just print to stdout if you want to.

Imagine you talk to someone who has done assembly his whole life and now wants to write something in, let's say, Java.

What would you think if he asks the question in the way you did?

Sometimes, when you learn a language that is so different you really really should NOT try to assume that your current knowledge just translates.

> And I've had a lot of fun micro-optimizing Haskell code for Project Euler problems when I was studying.

Sounds a lot like my experience. I never really used Haskell for "real work", where I need support for high-performance numerical calculations that is simply better in other languages (Python, Julia, C/C++, Fortran).

But learning functional programming through Haskell – mostly by following the "Learn you a Haskell" book and then spending time working through Project Euler exercises using it – had a quite formative effect on how I write code.

I even ended up baking some functional programming concepts into my Fortran code later. For instance, I implemented the ability to "map" functions on my data structures, and made heavy use of "pure functions" which are supported by the modern Fortran standard (the compiler then checks for side effects).

It's however hard to go all the way on functional programming in HPC contexts, although I wish there were better libraries available to enable this.

I hear this a lot, but am curious about two things: (a) which bit(s) of the toolchain are you thinking about specifically -- I know HLS can be quite janky but I haven't really been blocked by any tooling problems myself; (b) have you done much Haskell in production recently -- i.e. is this scar tissue from some ago or have you tried the toolchain recently and still found it to be lacking?

My take on this is that this was all nice and interesting but a lot of this stuff was a bit academic. F# is probably the closest the community got to having a mature tooling and developer ecosystem.

I don't use Haskell myself and have no strong opinions on the topic. But usually a good community response to challenges like this is somebody stepping up and doing something about it. That starts with caring enough. If nobody cares, nothing happens.

Smalltalk kicked off a small tool revolution in the nineties with its refactoring browser. Smalltalk was famous for having its own IDE. That was no accident. Alan Kay, who was at Xerox PARC famously said that the best way to predict the future was to invent it. And of course he was (and is) very active in the Smalltalk community and its early development. Smalltalk was a language community that was from day one focused on having great tools. Lots of good stuff came out of that community at IBM (Visual Age, Eclipse) and later Jetbrains and other IDE makers.

Rust is a good recent example of a community that's very passionate about having good tools as well. Down to the firmware and operating system and everything up. In terms of IDE support they could do better perhaps. But I think there are ongoing efforts on making the compiler more suitable for IDE features (which overlap with compiler features). And of course Cargo has a good reputation. That's a community that cares.

I use Kotlin myself. Made by Jetbrains and heavily used in their IDEs and toolchains. It shows. This is a language made by tool specialists. Which is why I love it. Not necessarily for functional purists. Even though som Scala users have reluctantly switched to it. And the rest is flirting with things like Haskel and Elixir.

Exactly the same for me.

> Granted, the tooling is sh*t.

Stack and Stackage (one of the package managers and library distribution systems in Haskell-land) is the best I found in any language.

Other than that I also found some tools to be lacking.

And I will as strongly as possible emphasize the opposite you should not.

If you are are already experienced in functional programming, as well as in statically typed functional programming or something lovely in the ML family of languages then only then does Haskell make sense to learn.

If you are looking to learn about either FP in general, or staticly typed FP Haskell is about the single worst language anyone can start with. More people have been discouraged from using FP because they started with Haskell than is probably appreciated. The effort to insight ratio for Haskell is incredibly high.

You can learn the majority of the concepts faster in another language with likely 1/10th the effort. For general FP learn clojure, Racket, or another scheme. For statically typed FP learn F# or Scala or OCAML or even Elm.

In fact if you really want to learn Haskell is is faster to learn Elm and then Haskell than it is to just learn Haskel. Because the amout or weeds you have to navigate through to get to the concepts in Haskell are so high that you can first learn the concepts and approach in a tiny language like Elm and it will more than save the amount of time it would take to understand those approaches from trying to learn Haskell. It seems unbelievable but ai found it to be very try. You can learn two languages faster than just one because of how muddy Haskell is.

Now that said FP is valuable and in my opinion a cleaner design and why in general our industry keeps shifting that way. Monoids, Functors, Applicative are nice design patterns. Pushing side effects to the edge of your code (which is enforced by types) is a great practice. Monads are way overhyped, thinking in types is way undervalued. But you can get all of these concepts without learning Haskell.

So that's the end of my rant as I've grown tired of watching people dismiss FP because they confuse the great concepts of FP with the horrible warts that come with Haskell.

Haskell is a great language, and I'm glad I learned it (and am in no way an expert at it)- but it is the single worst language for an introduction to FP concepts. If you're already deep in FP it's and awesome addition to your toolbox of concepts and for that specific purpose I highly recommend it.

And finally, LYAH is a terrible resource.

    import Data.Vector.Unboxed.Mutable
    
    import Data.Foldable (for_)
    import Prelude hiding (foldr, read, replicate)
    
    -- ghci> main
    -- [0,0,0,0,0,0,0,0,0,0]
    -- [0,5,10,15,20,25,30,35,40,45]
    main = do
      v <- replicate 10 0
    
      printVector v
    
      for_ [1 .. 5] $ \_ -> do
        for_ [0 .. 9] $ \i -> do
          v_i <- read v i
          write v i (v_i + i)
    
      printVector v
    
    printVector :: (Show a, Unbox a) => MVector RealWorld a -> IO ()
    printVector v = do
      list <- foldr (:) [] v
      print list

    # python /tmp/test28.py
    # [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    # [0, 5, 10, 15, 20, 25, 30, 35, 40, 45]
    def main():
        v = [0] * 10
    
        print(v)
    
        for _ in range(5):
            for i in range(10):
                v_i = v[i]
                v[i] = v_i + i
    
    
        print(v)
    
    if __name__ == '__main__': main()

For me, I stopped trying to learn Haskell because I couldn't quite make the jump from writing trivial (but neat) little self-contained programs to writing larger, more involved, programs. You seem to need to buy into a contorted way of mentally modelling the problem domain that doesn't quite pay off in the ways advertised to you by Haskell's proponents (as arguments against contrary approaches tend to be hyperbolic). I'm all for persistent data structures, avoiding global state, monadic style, etc. but I find that OCaml is a simpler, pragmatic, vehicle for these ideas without being forced to bend over backwards at every hurdle for limited benefit.

> In Haskell, how is that handled? do I have to recreate the list of entities with their changes at every simulation step? does Haskell have a special construct that allows for values to be overwritten, just like in imperative languages?

You don't _have to_ recreate the list each time, but that's probably where I'd suggest starting. GHC is optimized for these kinds of patterns, and in many cases it'll compile your code to something that does in-place updates for you, while letting you write pure functions that return a new list. Even when it can't, the runtime is designed for these kinds of small allocations and updates, and the performance is much better than what you'd get with that kind of code in another language.

If you decided that you really did need in-place updates, then there are a few options. Instead of storing a vector of values (if you are thinking about performance you probably want vectors instead of lists), you can store a vector of references that can be updated. IO is one way to do that (with IORefs) but you can also get "internal mutability" using STRefs. ST is great because it lets you write a function that uses mutable memory but still looks like a pure function to the callers because it guarantees that the impure stuff is only visible inside of the pure function. If you need concurrency, you might use STM and store them as MVars. Ultimately all of these options are different variations on "Store a list of pointers, rather than a list of values".

There are various other optimizations you could do too. For example, you can use unboxed mutable vectors to avoid having to do a bunch of pointer chasing. You can use GHC primitives to eek out even better performance. In the best case scenario I've seen programs like this written in Haskell be competitive with Java (after the warmup period), and you can keep the memory utilization pretty low. You probably won't get something that's competitive with C unless you are writing extremely optimized code, and at that point most of the time I'd suggest just writing the critical bits in C and using the FFI to link that into your program.

Monads are more-or-less syntax sugar. They give you a structure that allows these optimizations more easily, and also make the code more readable sometimes.

But in your example, update returns a new copy of the state, and you map it over a list for each step. The compiler tries to optimize that into in-place mutation.

IMO, having to rely so much on optimization is one of the weak points of the language.

When I worked on a relatively simple simulation in Haskell, that's exactly what I did: the individual entities were immutable, but the state of the system was stored in a mutable vector and updated in place. The actual "loop" of the simulation was a stream[2] of events, which is what managed the actual IO effect.

My favorite aspect of designing the system in Haskell was that I could separate out the core logic of the simulation which could mutate the state on each event from observers which could only read the state on events. This separation between logic and pure metrics made the code much easier to maintain, especially since most of the business needs and complexity ended up being in the metrics rather than the core simulation dynamics. (Not to say that this would always be the case, that's just what happened for this specific supply chain domain.)

Looking back, if I were going to write a more complex performance-sensitive simulation, I'd probably end up with state stored in a bunch of different mutable arrays, which sounds a lot like an ECS. Doing that with base Haskell would be really awkward, but luckily Haskell is expressive enough that you can build a legitimately nice interface on top of the low-level mutable code. I haven't used it but I imagine that's exactly what apces[3] does and that's where I'd start if I were writing a similar sort of simulation today, but, who knows, sometimes it's straight-up faster to write your own abstractions instead...

[1]: https://hackage.haskell.org/package/vector-0.13.1.0/docs/Dat...

[2]: https://hackage.haskell.org/package/streaming

[3]: https://hackage.haskell.org/package/apecs

    World simulation(Stream<Event> events, World world) =>
       events.IsComplete
           ? world
           : simulation(applyEventToWorld(events.Head, world), events.Tail);

    World applyEventToWorld(Event event, World world) =>
       // .. create a new World using the immutable inputs

However, there are real mutation constructs, like IORef [1] It will do actual in-place (atomic) mutation if you really want in-place updates. It requires the IO monad.

[1] https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-...

Yes and no.

No, the language doesn't have a special construct. Yes, there are all kinds of mutable values for different usage patterns and restrictions.

Most likely you end up with mutable containers with some space reserved for entity state.

You can start with putting `IORef EntityState` as a field and let the `update` write there. Or multiple fields for state sub-parts that mutate at different rates. The next step is putting all entity state into big blobs of data and let entities keep an index to their stuff inside that big blob. If your entities are a mishmash of data, then there's `apecs`, ECS library that will do it in AoS way. It even can do concurrent updates in STM if you need that.

Going further, there's `massiv` library with integrated task supervisor and `repa`/`accelerate` that can produce even faster kernels. Finally, you can have your happy Haskell glue code and offload all the difficult work to GPU with `vulkan` compute.

The same way games do it. The whole world, one frame at a time. If you are simulating objects affected by gravity, you do not recalculate the position of each item in-place before moving onto the next item. You figure out all the new accelerations, velocities and positions, and then apply them all.

But let's put that aside. You can instead use the ST monad (not to be confused with the State monad) and get the same performance benefit of in-place update of values.