Ask HN: What language has a functional feature that haskell doesn't yet?

There are languages that have stronger type systems. I.e. idris, agda.<p>There is paralel lineage of ml-style languages (ocaml, F#) that deal with abstraction in different way (I find ocaml module system fascinating and yet have to fully comprehend it)<p>Haskell is by default lazy, you might prefer strict evaluation.<p>You might like the macro-system of Lisp, meta-programming in Haskell is trickier.<p>Purescript has much nicer record system, with row-polymorphic types.<p>On the other hand, if there is a niche Haskell was actually built for, it is researching functional language features. So if you are missing a feature, there is a chance somebody is working on a pragma for that :)

a-saleh mentioned that Idris and Agda have &quot;stronger type systems.&quot; I would like to expand that Idris and Agda (and Coq&#x2F;Gallina, too) are &quot;dependently typed&quot; programming languages, meaning that types and terms can mix. To my understanding, GHC Haskell is on the way to getting dependent types. GHC currently has the TypeInType and DataKinds extensions, which allow type-level programming. However, Haskell will not get a termination checker, so all types are inhabited by divergent terms. So, you can prove anything. Coq, Agda, and Idris have termination checkers, so you can use them to prove things.<p>Agda has &quot;Cubical mode,&quot; which extends it with Cubical Type Theory, a take on Homotopy Type Theory where the Univalence Axiom is not an axiom, but rather has computational meaning.