[tel]

I suppose that's true. I guess in my eyes DTs are such a meteoric difference that Idris is not sufficiently more interesting than the others yet. But time will tell if they manage to build a better way to manage proofs, for instance, they could really change the game.

[coolsunglasses]

That there is no game-plan for doing anything any better than Coq presently does is why I'm a bit skeptical. The trimmings are nicer - nothing else as of yet.

[freyrs3]

The elephant in the room in these discussions is that the cost of bringing a function compiler to fruition is so high that too much of the discussion gets muddled in the semantics of these hypothetical Haskell-successor languages while no one is actually working on said language. Academia simply isn't set up to incentivize large engineering projects, and industry would never invest in building such a thing either since there's no profit in language dev sadly.

The blunt truth is that at the end of the day Haskell works today, period, and until someone actually forks or starts writing a new language very little of these criticisms of Haskell actually matter if the answer to "what should I use for my project at work" is "well it doesn't exist yet, but it has modules and extensionality and a magical pony that shits money".

[coolsunglasses]

This is more or less where I stand as well. Haskell has an efficient RTS, well designed compiler, best-in-industry concurrency, good-enough type-safety that is light-years ahead of even things like Scala, and a good library ecosystem.

It's ready now and I'd like to begin work with Haskell in the hopes that industry wakes up to the utility of future successors to Haskell by seeing Haskell itself in action.