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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
