IO aをRealWorld -> (a,RealWorld)とみなした上で外延性から
∀ x :: IO a, ∃s.s' :: RealWorld. x s /= x s'について解釈することで参照透明性をもう少し厳密に言えないのかな