Those two languages are popular because they bring some of the benefit of languages like Haskell into an environment that is compatible with an outdated but widely used OOP language.

Haskell will bring you more of the benefits from FP with expressive types; Idris will bring you even more. But you will lose the integration.

A lot of people mistake Purity as a language feature for meaning a more pure functional language. What makes a language functional is that their basic unit of abstraction is functions, not whether they isolate IO effects by default.

Impure functions lack referential transparency, which is often sacrificed but kind of important to being a function - getting the same result every time you call it with the same input. Alternatively, you can say that every function has an implicit input parameter of the the current program state, but that turns every function on one bit of input to a potentially astronomically complex function of gigabytes of input.

I do agree with what you're saying about the value of referential transparency and the formal definition of a function as a lambda term. In fact, I work professionally as a Haskell developer and highly value this aspect of the language design; equational reasoning is a really powerful tool.

My point is that functional programming as engineering practice and language family is broader then variants of pure lambda calculi and Haskell occupies one particular place in that broad space.

Haskell focuses on both, but prioritizes research. I have had several Haskell jobs and highly recommend it for the personal enjoyment.

F# is not particularly practical as far as jobs go, but it benefits from the large C# ecosystem.

I'm primarily a C# dev, but after dabbling in some F#, I concluded that most of the niceties in F# could also be done (to some extent and with some limitations) on C# as they have the same compile targets.

Haskell is far from being an academic language. It’s used in industry and has very practical features and libraries.

Same as F#, OCaml, etc.