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 w

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".