[chousuke]

Haskell IO is pure because an IO action is basically just an "instruction". For example, one way to make a pure thing out of a side-effecting procedure is to wrap it in a lambda; it won't do anything until you actually call it, so you can use it as a value. The reason why IO is "separated" by the type system is the same as why Strings are "separated" from Ints: They are different.

The monad operations happen to be a convenient interface for combining IO values to form a composite value that is then called "main", and when the program is actually run, the value of main is executed to produce all the effects.

[Peaker]

"Pure" typically means referentially transparent. Wrapping a side-effecting procedure in a lambda does not make it referentially transparent, therefore it isn't pure.

[chousuke]

It is referentially transparent. The lambda (or thunk) itself can be used freely as a value. For example

  newtype PureIO a = PureIO (() -> a)
  print :: String -> PureIO ()
  print s = PureIO $ \_ -> unsafePrint s -- impure primitive

If the user only has access to the "print" variable, then they can only use it as a pure value. two applications of print "foo" would result in two thunks, either of which, when actually invoked, would cause the side-effect of printing "foo".

Invoking the pure IO values is something only the runtime can do, so referential transparency is not violated.

[Peaker]

The important thing here is not the wrapping with a lambda. That's not what made it pure.

The important thing here is the abstract type wrapper. You're exposing pure primitives that are implemented in terms of (hidden) impure ones.

That's why code that uses unsafePerformIO can be pure and referentially transparent, as long as the exposed primitives are pure and implementation details are hidden.

To demonstrate this, imagine that you did expose the PureIO data constructor -- then values of type PureIO would not be referentially transparent anymore.