That is not the only reason to have an IO monad. PureScript and Idris are both strict languages that still reify IO effects. Its still useful to know which functions are pure.
I'm actually not a fan of Idris' implementation of the IO monad, it really should have been a free monad with a cofree comonad so you can enforce invariants against the world without a bunch of extra machinery. It seems kind of important for a dependent type system.
I quite like Mercury's non-monadic linear IO + determinism semantics. You can subtype the world with insts and unify against the world-state pretty easily.
I quite like Mercury's non-monadic linear IO + determinism semantics. You can subtype the world with insts and unify against the world-state pretty easily.