throwaway518365

I probably wouldn't until/unless Idris 2 gained some steam, it would probably be Ocaml.

I was thinking more along the lines of dependent types, because the kinds of problems where you'd really really need strong static types overlap with the need for dependent types, which Haskell has some support for (and Ocaml but less so).

But if I needed to prove something I'd probably do it in Coq since it interops with Ocaml fairly well.

Not much afaict. For mathematics, it's usually Coq, maybe Lean or Agda. For scientific computing it's Python or Julia.

What software issue does category theory and abstract algebra solve?

Don't get me wrong, it's cool and it has expanded my appreciation and understanding of math. But I just don't see what engineering problem it's solving besides mathematical elegance.

If you're thinking monads and IO -- separating side effects is nice and useful, but it doesn't solve any real problem IMO. It's not like people are losing sleep because they don't know which code is side effecting. Side effects are where a lot of engineering complexity is, but IO doesn't wrangle it much better than anything else. Maybe Erlang does the best job at it IMO.

And plus monads don't compose. Algebraic effects (ie multicore Ocaml), or even Actors, does "IO" in a better way without the math jargon.

> I find it hard to believe that anyone who’s really used both prefers OCaml over Haskell.

I've actually used Haskell, Ocaml and Purescript for several years and a lot of locs, and I actually like Ocaml better. Reasons:

- The module system -- a very intuitive way to structure code

- Poly variants

- Strictness -- predictable performance and easy debugging

- Allowing side effects

- Private types -- better than newtypes imo since you can upcast to it's structural counterpart

- Really good type inference -- you never have to write type signatures. Haskell and Purescript type inference is ok-ish and sometimes craps out, which is part of why type signatures for each function is recommended.

- Stupidly fast compiler -- yes it matters, try contributing to the Idris codebase. It's like trying to contribute to the linux kernel, you'll wait 30+ minutes for it to compile.

- Very fast programs

- An actual package manager (stack uninstall?)

It is an overall better experience for me. And the language features that are coming down the pipeline are looking great:

- Modular implicits - a more sound ad hoc polymorphism system than typeclasses. Typeclasses can't handle simple things like if half of the Haskell ecosystem uses one Filterable typeclass and the other half uses a different Filterable.

- Algebraic effects - a strongly typed system for writing effects that will be part of multicore -- delimited continuations / conditions and restarts

These days I'm more interested in Erlang/Elixir though. I just don't think static typing is all that after having spent so much time with Haskell/Purescript/Idris/Ocaml. There are really nice benefits you get with dynamic typing that you don't with static, and there are better ways to deal with those problems that won't be noticeably worse in most business applications with just a little bit of coding discipline, such as good testing habits and having good fault tolerance built into the language.

I do like Haskell though, it's definitely really fun to program in. It's just not something I'd use for anything. If I really needed something with strong static typing I'd either go with Ocaml or Idris.