Pure usually has a stricter definition. First we need the ability to state whether two functions are equal. Then we need a function which is constantly unit. Finally we need composition such that (f >> g) is "f then g". Now, a function f is pure if and only if
constantly_unit = f >> constantly_unit
If you unpack that a bit it might translate as "if we throw away the return value of a function, it is exactly the same as if nothing is happening at all".
If your notion of equality differentiates "println" and "constantly_unit" then we cannot call "println" pure.
Note that this is a very powerful notion of purity. It's so powerful as to render Haskell impure as if we have the function
loop x = loop x
then `loop >> constantly_unit` never returns and is therefore easy to distinguish from `constantly_unit` itself. This just drives home that non-termination is an effect itself!
Hmm I wonder if that loop example can be rehabilitated. If we interpret it, not as a description of how to evaluate loop, but rather as a constraint on loop. Then we see that the statement is simply a non-condition on loop.
This would mean that non-termination is not a property of the function, but of the compiler/runtime, in that they failed to notice that loop was a partial function called with an input value for which it was not defined!
Comments
Pure usually has a stricter definition. First we need the ability to state whether two functions are equal. Then we need a function which is constantly unit. Finally we need composition such that (f >> g) is "f then g". Now, a function f is pure if and only if
If you unpack that a bit it might translate as "if we throw away the return value of a function, it is exactly the same as if nothing is happening at all".If your notion of equality differentiates "println" and "constantly_unit" then we cannot call "println" pure.
Note that this is a very powerful notion of purity. It's so powerful as to render Haskell impure as if we have the function
then `loop >> constantly_unit` never returns and is therefore easy to distinguish from `constantly_unit` itself. This just drives home that non-termination is an effect itself!Hmm I wonder if that loop example can be rehabilitated. If we interpret it, not as a description of how to evaluate loop, but rather as a constraint on loop. Then we see that the statement is simply a non-condition on loop.
This would mean that non-termination is not a property of the function, but of the compiler/runtime, in that they failed to notice that loop was a partial function called with an input value for which it was not defined!
That's probably possibly in this particular case but it sounds a lot like you're heading toward Halting Problem territory here :)
Ah, but Haskell is lazy so loop will never be evaluated and a
will return unit no matter what.Ah, yeah, I was being fast and loose with laziness. You have to `seq` the argument to `constantly_unit`, too.