[Haskell-cafe] On the purity of Haskell

[Steve Horne]

On 01/01/2012 22:57, Jerzy Karczmarczuk wrote:
> Dan Doel :
> ...
>> Also, the embedded IO language does not have this property.
>>
>>      do x<- m ; f x x
>>
>> is different from
>>
>>      do x<- m ; y<- m ; f x y
>>
>> and so on. This is why you shouldn't write your whole program with IO
>> functions; it lacks nice properties for working with your code.
> Sorry, what are you trying to suggest?
>
> You show two OBVIOUSLY different pieces of code, and you say that they
> are different.
> If, by chance, some newbie reads that and gets the impression that
> (<-) is something equivalent to (=), you are serving the devil.
>
Speaking as the devil...

The do-notation sugar may confuse the issue - the <- looks like an 
operator, but translating to binds-and-lambdas form suggests otherwise. 
Quick translations (I hope no mistakes) with lots of parens...

   m >>= (\x -> (f x x))

   m >>= (\x -> (m >>= (\y -> (f x y))))

At first sight, these two expressions can give different results for 
reasons other than evaluation order. In particular, there are two bind 
operators, not just one.

That is, x and y could get different values for reasons other than the 
two m references referring to different things. So... is that true?

Of course even the bind operator arguably isn't primitive. We could 
translate to get rid of those too, and see what lies underneath. This is 
where we start seeing functions of type...

   World -> (x, World)

Problem - this level of abstraction is hypothetical. It is not part of 
the Haskell language. Haskell specifically defines the IO monad to be a 
black box.

I look at this World parameter as purely hypothetical, a trick used to 
gain an intuition. Whereas Jerzy (I think) uses it to claim Haskell is 
referentially transparent - those differing x and y values come from 
different worlds, or different world-states. I'm not entirely sure, 
though, as we got sidetracked.

If main returns a function of type "World -> (x, World)" wrapped in a 
monad context, then there is referential transparency as defined in 
computer science. But is that a fair claim?

In this model, Haskell is an interpreted language for compositing 
functions. We can call those functions programs. The executable is a 
translation of the function returned by main, but *not* a translation of 
the source code.

But GHC is called a compiler, and compilation is usually considered a 
kind of translation - the executable is a translation of the source 
code. GHCi is an interpreter, but it doesn't stop at returning a 
function of type World -> (x, World) - it does the I/O. And the reason 
we use these terms is because, as programmers, we think of the 
executable as the program - as a translation of the source code.

So what main returns - that hypothetical function World -> (x, World) - 
isn't just a product of the program, it's also a representation of the 
program.

I've made similar points before, but how do they work out this time...

So...

   when           evaluate what             effects  referentially 
transparent
   -------------  ------------------------  ------- 
-------------------------
   compile-time   main                      no       yes
   run-time       main someParticularWorld  yes      yes(?)

I've proved effects at run-time, but in this model, the intermediate and 
final world-states are products of the evaluation of that "main 
someParticularWorld" expression. Even the results extracted from input 
actions are referentially transparent - or if not, we're dealing with 
the philosophy of determinism.

It's probable that Jerzy told me this earlier and I wasn't ready to hear 
it then.

However - we can say basically the same things about C. The World 
parameter is implicit in C but then it's implicit in Haskell too. 
Everything inside the IO monad black box is outside the scope of the 
Haskell language except in that semantics are defined for the primitive 
IO actions - basically what happens when a result is extracted out as 
part of evaluating a bind. That "(?)" in the "yes(?)" is because this is 
all contingent on that hypothetical World -> (x, World) function hidden 
inside the IO monad context, which is not specified in the Haskell language.

When I say that Haskell lacks referential transparency because the 
execution of primitive IO actions is tied to the evaluation of the bind 
operators that extract out their results, and different executions of 
the same action yield different results, I'm only appealing to the 
defined semantics of the Haskell language. I'm not appealing to a 
hypothetical model where the world is passed as a parameter.

OTOH, this World -> (x, World) model is much more appealing than my 
partially-evaluated-functions-as-AST-nodes model.

So - the issue seems to be whether the IO monad is a context holding 
world-manipulating functions, or whether it's a black box with semantics 
specified at the bind level. And if referential transparency is decided 
at this level, what practical relevance does it have?

It's probably better to stick with "the functional core is referentially 
transparent - IO actions break that, so don't overuse the IO monad". You 
can argue "may or may not break that depending on your viewpoint", but 
if you can't objectively decide which viewpoint is correct, then you 
haven't proven referential transparency.