CODEWITHSUNDEEP
haskellmoduletype-systemspurely-functionalio-monad
Josh Grosso
Josh Grosso

Reputation: 2124

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

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

Upvotes: 2

Views: 145

Answers (2)

Ingo
Ingo

Reputation: 36339

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.

Upvotes: 4

chi
chi

Reputation: 116174

Sure, exporting low-level primitives could allow side effects everywhere. And, yes, you could obtain purity only by avoiding to export each dangerous thing. No type-level machinery is needed.

However, with no type constraints everything IO-related would be dangerous. So we would completely disallow IO. Not really useful.

With the help of the type system, instead, we can export some "dangerous" IO-actions, knowing that they can be executed only in "controlled" places, which have to carry an IO tag in their type. Making them no longer dangerous.

So, purity comes from a combination of static guarantees and careful exporting.

Upvotes: 4

Related Questions