5 ms·
Purity is not dead. Haskell 'has' side effects but they are explicitly managed. Managing side effects and relegating them to well defined areas lives on in newe
by efnx 11y ago
Purity is not dead. Haskell 'has' side effects but they are explicitly managed. Managing side effects and relegating them to well defined areas lives on in newer languages.
- mafribe 11y agoThere 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.
- mbrock 11y agoCan 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?
- mafribe 11y agoThanks 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 ...
- wz1000 11y agoIt 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].
- denim_chicken 11y agoC is "pure" too. The statement puts ("hello"); is a "pure" value of type int.
- dllthomas 11y agoNo, 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.
- deleted 11y ago[deleted]
- wz1000 11y agoHere is a comment I wrote about the same issue some time ago: https://news.ycombinator.com/item?id=9085403 https://news.ycombinator.com/item?id=9085403 Haskell IO is severely misunderstood.
- nbouscal 11y agoYou'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.
- dllthomas 11y agoAs 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/history-of-haskell/history.pdf http://research.microsoft.com/en-us/um/people/simonpj/papers...
- nbouscal 11y agoThanks for the correction! I wondered about that when I was writing it but didn't have time to go double-check.