Lots of tedious back-and-forth in here about how many pure angels can dance on the head of a side-effecting IO monad, as usual.

The desirable properties that we are trying to enforce are that, firstly

    x = expression
    y = expression
    ...

is the same as

    x = expression
    y = x
    ...

and that, secondly

    x = expression
    ...

is the same as

    ...

when x does not appear in ... .

These conditions are an order of magnitude more important than any considerations about what "purity" really means, what side effects are versus effects, whether there's an impure runtime below a pure language and whether IO is a "sublanguage".