Alternative to language purity

Question

Purity

One of the interesting concepts in Haskell is the purity. However, I am wondering what the pragmatic reasons behind this is - let me explain a bit more before you reject my question.

My main point is that we are going to have side-effect no matter how we might encapsulate these in a language. So, even if a programming language like Haskell is pure, we are just "postponing" the side-effects till a later point.

I understand the idea that purity makes reasoning about programs easier (referential transparency and so on). In Haskell, we encapsulate all side-effects in the type system (the IO monad). As such, we cannot have a side-effect without propagating the IO monad down through the types of all functions calling our impure function, so to speak.

As such, I am very keen on the idea of separating pure functions from impure ones in the type system. This seems like a good way to force ourselves to limit such effects.

Still, Haskell is often getting bashed because of its pure nature - people say it isn't practical or pragmatic. Whether this is true or not is another matter, but the fact is that many people reject Haskell for this reason.

An alternative approach? (let us call it "type pollution")

To me, it seems that the main winning point is not purity itself, but the separation of pure and impure code. If encapsulating IO in a monad is too impractical, why don't we try a simpler approach?

What if we instead labelled every return type and argument type in the system as pure or impure. The D language has en explicit "pure" keyword, but I am thinking that we let functions be pure by default and only mark impure functions.

In an ML-like language this could look like this:

let square x = x * x

let impure getDbData connectionString = ...

let impure getMappedDbData mapping =
    let dbData = getDbData "<some connection info>"
    in map mapping dbData

let main =  // Compiler error, as it is not marked as impure
    let mappedData = getMappedData square
    in ...

Further, calling any impure function would "pollute" the calling functions return type, turning it impure. If it wasn't labelled as such, it would give a compile error.

(of course, passing functions as arguments would need to be checked against the expected purity as well, but it should be easy to infer the expected "purity" of arguments)

(the "impure" label could be inferred as well, by I guess it is better to keep this one explicit, for readability)

Pure functions on the other hand, can be passed anywhere, no matter the expected purity. We could give a pure function as input to a function accepting an impure one. So it is not a symmetric relationship - therefore the word "pollution".

All in all, this would explicitly (and statically checked) separate the codebase into a pure and impure part. In many ways, it is close to the functionality of an IO monad (although the asymmetry probably rules out a 1-to-1 mapping between the two), but with an implicit unwrapping done automatically. Most importantly, many programmers would find it more intuitive and pragmatic than an explicit IO monad or something similar.

And unlike the completely impure solutions, this gives a lot more safety to reason about the pure parts (without standing too much in our way, when defining the impure ones). And all in all, it is mostly a statically enforced version of what most functional programmers consider best practice anyway (the separation).

TL;DR;

Has something like the above described approach ever been tried out? If not, is there any reason why not (both technical, practical, theoretic and philosophical reasons are interesting)?

And finally, would such a purity check be easier to accept for people who claim Haskell is impractical?

Disclaimer

I do not personally hold any grudges towards Haskell and the choice of using monads for IO. In fact, I find Haskell to be one of the most elegant languages in use, and maybe the one language I enjoy the most.

Further, it is clear that the above mentioned approach does not offer something that the IO monad does not - the only thing is that it more closely (visually) resembles impure languages like OCaml, F# and so on, which is bound to make it easier to grasp for many people. In fact, taking existing F# code and adding some "impure" labels would be the only visual difference in code.

Hence, this could be an easy step towards purity for languages that do not have the same ecosystem surrounding monads as Haskell has.

Answer 1

You have described an effect system. It’s true that there are other effect systems than monads, but in practice monads give you a lot of expressive power that you would need to reinvent in any practical effect system you might devise.

For example:

• I start by tagging my I/O procedures with an io effect.
• My pure functions can still throw exceptions, but throwing exceptions isn’t io, so I add an exn effect. Now I need to be able to combine effects.
• I want to have non-I/O functions that use mutation internally on a local heap h, and I want the compiler to make sure that my mutable references don’t escape their scope, so I add an st<h> effect. Now I need parameterised effects.
• For higher-order functions, I need to write multiple versions for every combination of effects I want to support—for example, map with a pure function versus map with an impure function. Now I need effect polymorphism.
• I notice that my user-defined type could be used to model effects (benign failure, nondeterminism) that the language doesn’t have natively. Now I need user-defined effects.

Monads support all of these use cases:

• Functions that may return errors can use the Either monad.
• Effects can be combined with monad transformers—if I need exceptions and I/O, I can use the EitherT IO monad.
• Monads can be parameterised like any other type; the ST h monad lets you do local mutation on STRefs in the scope of a heap h.
• Because of the Monad typeclass, I can overload an operation to work on any kind of effect. For example, mapM :: (Monad m) => (a -> m b) -> [a] -> m [b] works in IO, but it also works in Either or ST or any other monad.
• All monads are implemented as user-defined types, except for things like IO and ST which must be implemented in the Haskell runtime.

There are of course some significant warts in Haskell’s use of monads for side effects.

For one thing, monad transformers are generally not commutative, so StateT Maybe is different from MaybeT State, and you have to be careful to choose the combination that you actually mean.

The bigger problem is that a function can be polymorphic in which monad is being used, but it cannot be polymorphic in whether a monad is being used. So we get loads of duplicated code: map vs. mapM; zipWith vs. zipWithM, &c.

Now, in answer to your actual question…

Koka from Microsoft Research is a language with an effect system that does not suffer from these problems. For example, the type of Koka’s map function includes a type parameter e for effects:

map : (xs : list<a>, f : (a) -> e b) -> e list<b>

And this parameter can be instantiated to the null effect, making map work for pure and impure functions alike. In addition, the order in which effects are specified is immaterial: <exn,io> is the same as <io,exn>.

It’s also worth mentioning that Java’s checked exception mechanism is an example of an effect system that people have widely accepted, but I don’t feel it adequately answers your question because it’s not general.

Answer 2

I think you've reinvented monads! Let's look at what we have here, we can "dirty" a pure computation implicitly and use it in an impure one, and we can call impure function from another impure one.

That sounds a lot like monads, we can dirty a pure value with return, to call another function from an impure function, we can just use >>=

apply :: (a -> IO b) -> IO a -> IO b
apply f a = a >>= f

Now your approach is a little more familiar to people from other languages: we all have some sort of purity check running through our heads to try to figure out what's happening where.

The disadvantage is that by making these things a language level concept, we've made it very difficult to build on. In Haskell, there's a whole library of normal, user defined functions that work across all monads. If we baked IO wholesale into the language we'd be forced to make all of these functions primitive!

By minimizing the amount of dark magic around how purity is handled, we can actually make things easier to work with from userland.