The problem is more that you cannot formally express your type system in such a case. The "pure" perspective you mentioned is basically the limited view that on

The problem is more that you cannot formally express your type system in such a case. The "pure" perspective you mentioned is basically the limited view that one can still work with when defining a type system. Side effects are then basically magic functions that have any necessary type (in fact, OCaml has such a function in its stdlib, called "magic", if I am not mistaken).