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.
Best Answer
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:
io
effect.io
, so I add anexn
effect. Now I need to be able to combine effects.h
, and I want the compiler to make sure that my mutable references don’t escape their scope, so I add anst<h>
effect. Now I need parameterised effects.map
with a pure function versusmap
with an impure function. Now I need effect polymorphism.Monads support all of these use cases:
Either
monad.EitherT IO
monad.ST h
monad lets you do local mutation onSTRef
s in the scope of a heaph
.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 inIO
, but it also works inEither
orST
or any other monad.IO
andST
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 fromMaybeT 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 parametere
for effects: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.