There is no need to put "has" in scare quotes. Haskell does have side effects like C, Java and Python (although maybe not quite as conveniently). If you want to look at side-effect free languages, consider Miranda, Coq, Agda.

What Haskell contributes (in a concrete implementation, the ideas go back to Moggi's theory) is the monadic encapsulation of effects, which I treat as a separate point under (viii). Monadic encapsulation of effects is not absence of effects. It's a reflection of effects at the type level.

You're using a somewhat non-standard definition of "purity", which makes your claims more confusing than they need to be. Haskell is usually referred to as pure, and has had encapsulated effects from the start. Your claims are true using your definition of "purity", but false using the more common one.

As a point of historical note, Haskell has not had encapsulated effects from the start. Monadic IO was introduced in version 1.3, roughly 6 years after version 1.0.

http://research.microsoft.com/en-us/um/people/simonpj/papers...

Thanks for the correction! I wondered about that when I was writing it but didn't have time to go double-check.

It is an absence of side effects because side effects are defined as effects that cannot be accounted for. As soon as you have a mechanism to document those effects, they are not "side effects" any more.

hello :: IO () hello = putStrLn "Hello World"

`hello` is a "pure" value of type IO (). putStrLn a "pure" function of type -> IO ()

IO () is a value like any other "pure" value, like [Int].

C is "pure" too.

The statement

   puts ("hello");

is a "pure" value of type int.

No, that statement evaluates to a pure value of type int. In the process, it does something else as well that effects the visible behavior of the program.

The C equivalent of

    putStrLn "hello"

is probably actually

    void putsHello(void) {
        puts("hello");
    }

Unfortunately, function definitions aren't something you can really manipulate at runtime in C.

Here is a comment I wrote about the same issue some time ago:

https://news.ycombinator.com/item?id=9085403

Haskell IO is severely misunderstood.

Can you clarify the essential difference between Haskell's and Agda's versions of monadic I/O?

Or are you talking about divergent side-effects like bottom and exceptions?

Thanks for your question. I should have been more careful. I meant Agda used as a prover, not Agda used as a 'conventional' programming language (Indeed in years of usage, I've never executed an Agda program, I've only ever used the type checker). In other words, Agda, the proof calculus for Martin-Loef type theory.

That said, I was talking about effects in general, including non-termination, exceptions, concurrency ...