Is Haskell's purity enforced by the type system or IO's implementation?

Question

It's always said that Haskell's type system prevents impure code from polluting pure code, since you always have to specify IO in the type signature. However, is that a consequence of the type system itself, or is it really just that IO(..) isn't exported?

Basically, is it not true that, if the type constructor was available, something like this could be done?

ioToPure :: IO a -> a
ioToPure (IO ioValue) = ioValue

Answer 1

Yes, that is in a sense true.

The type system in and of itself doesn't know anything about IO nor does it need to. It are different language features that hide the real representation of an IO action from the users, so that it is impossible to "just run" an IO action.

So, the truth is, that the IO security in Haskell and comparable languages is a combined result of several language features and properties, most prominently:

• a strong type system that doesn't accept "shut up, I know better" from the user.
• the property that everything is typed. What I mean here is that in impure languages, you have "statements" and even if the type system is strong, it doesn't look past the next semicolon. Whereas in Haskell, we only have expressions, and every bit of every expression gets a type, and influences, in the end, the type of the function the expression occurs in.
• The language features that hide type representation.

Nevertheless, I think that the expression "the type system makes sure that impure and pure code is separated" is a harmless simplification.