having side effects and having lazy evaluation are distinct features though. One can conceive of a strictly evaluated haskell-like which isolates side effects in monads and is still largely composed of pure functions.
> having side effects and having lazy evaluation are distinct features though
Fair enough, but lazyness also plays nicer with things like `if` and `&&` that comput things lazily. (Without lazyness you need to add lots of wrapper anonymous functions).
Another thins is that, from a hystorical point of view, the only reason Haskell managed to be so pure in the first place was the lazyness. If your language is not lazy its very tempting to add sideeffects.
Idris is explicitly billed as a programming language. You can do pretty sophisticated programming in Coq too (Coq can be reasonably straightforwardly compiled down to Ocaml, Haskell and some other languages.)
