| Do you have any examples? In my experience theoretical purity is largely independent of usability, which I find is more a function of the language's expressibility and the available abstractions (and how well those abstractions play together.) Take Elm, Haskell and Agda/Idris as examples of four programming languages with strong theoretical foundations, that also vary widely in expressibility and usability Elm is (imho) very usable even when teaching beginners unfamiliar with the ML-style syntax. The main abstraction is parametric polymorphism (generics in oop-terms), no subtyping with inheritance and no typeclass/interface mechanism. The language has a carefully crafted culture to maintain the beginner-friendliness of the language, explicitly at the expense of expressibility (but not usability.) I personally find elm to be an incredibly usable language, specifically because it's both simple and theoretically pure. Less to understand, for more gained reliability. More practically, I often prototype completely without type signatures, relying on type inference to make sure that I'm not doing anything nonsensical. The end result (for me at least) is the speed and ease of a dynamic language, with the reliability of a statically typed language. Haskell (without GHC extensions) offers more abstractions and is consequently "less usable" in the sense that you need to understand more theory to use things like Higher Kinded Types and whatnot. By adding GHC extensions you can gradually ramp up the expressibility (by adding abstractions,) while at the same time making the language (slightly) more difficult to use. You can get almost all the way to dependent types which brings us to.. Agda and Idris offers an incredibly powerful mechanism for abstraction called dependent types, where you essentially program your type checker as a logic. But they are (somewhat infamously) difficult to use due to having to understand the consequences of having computations at the type-level (and beyond) and consequently at compile time. If any of those are any less pure than the other it's probably Haskell, and that's more due to the ad hoc nature of the GHC extension system, which allows you to combine extensions in problematic ways that can hide impurity. They all compile based on some type theory as a model of computation, but those type theories can vary widely in how complex they are to understand, but the level of complexity doesn't make anything more or less pure. All of them also offers some degree of escape hatch from their "theoretical purity"-prison. Elm has its ports for js interop, Haskell has unsafeIO and friends, Agda has FFI to both js and haskell depending on backend, and I'm guessing Idris has some way of doing this as well. In this sense Elm is probably the most pure. |