Dan Doel | 1 Jan 22:31 2012
Picon

Re: On the purity of Haskell

On Sun, Jan 1, 2012 at 3:26 PM, Ketil Malde <ketil <at> malde.org> wrote:
> Chris Smith <cdsmith <at> gmail.com> writes:
>
>>> I wonder: can writing to memory be called a “computational effect”? If
>>> yes, then every computation is impure.
>
> I wonder if not the important bit is that pure computations are unaffected by
> other computations (and not whether they can affect other computations).
> Many pure computations have side effects (increases temperature,
> modifies hardware registers and memory, etc), but their effect can only
> be observed in IO.
>
> (E.g. Debug.Trace.trace provides a non-IO interface by use of
> unsafePerformIO which is often considered cheating, but in
> this view it really is pure.)

The point of purity (and related concepts) is to have useful tools for
working with and reasoning about your code. Lambda calculi can be seen
as the prototypical functional languages, and the standard ones have
the following nice property:

  The only difference between reduction strategies is termination.

Non-strict strategies will terminate for more expressions than strict
ones, but that is the only difference.

This property is often taken to be the nub of what it means to be a
pure functional language. If the language is an extension of the
lambda calculus that preserves this property, then it is a pure
functional language. Haskell with the 'unsafe' stuff removed is such a
(Continue reading)

Jerzy Karczmarczuk | 1 Jan 23:57 2012
Picon

Re: On the purity of Haskell

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.

Jerzy Karczmarczuk
Steve Horne | 2 Jan 04:43 2012
Picon

Re: On the purity of Haskell

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))))

(Continue reading)

Conal Elliott | 2 Jan 06:41 2012
Picon

Re: On the purity of Haskell

... World -> (x, World) ...
 
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 don't see this interpretation in Jerzy's words, and I'd be very surprised if he had that sort of argument in mind.

If main returns a function of type "World -> (x, World)" wrapped in ...

Main does not return or denote such a thing. The idea that Haskell IO can be accurately explained as (i.e., denotes) World -> (x,World) is a persistent myth. That model cannot explain concurrency (even with the outside world) or nondeterminism, both of which are part of Haskell IO. We don't have an precise & accurate denotational model for IO, in contrast to most other types in Haskell. Which is to say that while much of Haskell programming is denotative, IO programming is not. Peter Landin, an important figure in functional programming, proposed and defined this term "denotative" as a substantive & precise replacement for the fuzzier notions of "functional" and "declarative". He offered his definition and suggested that "When faced with a new notation that borrows the functional appearance of everyday algebra, it is (c) that gives us a test for whether the notation is genuinely functional or merely masquerading."

Of course, various subsets of IO can be precisely and accurately modeled, but so far not IO as we use it. It's very unlikely that we ever will have such a (precise & accurate) model, and by design, as explained at http://conal.net/blog/posts/notions-of-purity-in-haskell/#comment-22829 .

  - Conal

On Sun, Jan 1, 2012 at 7:43 PM, Steve Horne <sh006d3592 <at> blueyonder.co.uk> wrote:
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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Jerzy Karczmarczuk | 2 Jan 11:03 2012
Picon

Re: On the purity of Haskell

Conal Elliott cites Steve Horne:
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 don't see this interpretation in Jerzy's words, and I'd be very surprised if he had that sort of argument in mind.
I don't think either having used the 'World' model as an argument of the referential transparency.
The main reason is that I don't know what does it mean, the referential transparency of the real world.

There is a philosophical issue involved: the problem of IDENTITY, which is as old as the humanity, and it will survive it... We simply don't know what does it mean: "the same"...

But I disagree quite strongly with the idea of "World parameter as purely hypothetical, a trick used to gain an intuition". I mentioned the language Clean (no reaction, seems that Haskellians continue to ignore it...)

In Clean this IS the IO model. You have such entities as FileSystem, which has the Unique Access property, etc. You can put all that in an equivalent of the IO Monad, constructed within Clean itself, not as a primitive.

Jerzy

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Steve Horne | 2 Jan 11:58 2012
Picon

Re: On the purity of Haskell

On 02/01/2012 10:03, Jerzy Karczmarczuk wrote:
But I disagree quite strongly with the idea of "World parameter as purely hypothetical, a trick used to gain an intuition". I mentioned the language Clean (no reaction, seems that Haskellians continue to ignore it...)

I don't know about others, but I intend to learn one language at a time.

In any case, that's Clean, not Haskell.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Ertugrul Söylemez | 2 Jan 06:46 2012
Picon

Re: On the purity of Haskell

Steve Horne <sh006d3592 <at> blueyonder.co.uk> wrote:

> 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))))

First of all, you can omit all parentheses, because the (>>=) operator
is associative by definition (this is not checked by the compiler
though).

> 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?

Yes, that's correct.  Remember that referential transparency does not
say that you are not allowed to pass different values to the same
function.  It just forbids functions to return different results for
different inputs, and this is true for both expressions you showed.

Using a state monad to get more concrete, let's say that 'm' returns the
current state and then increments it.  If the start state is 3, then 'x'
will become 3 on execution and 'y' will become 4.  However, the result
of the composition is /always/ the state computation that returns the
result of 'f' applied to the current state and the incremented current
state.

Just like when you write "x = getLine", then you can safely replace any
occurence of 'getLine' by 'x'.

> 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.

And that's fine, because IO is an embedded DSL.  A better view of IO is
a GADT like:

    data IO :: * -> * where
        GetLine  :: IO String
        PutStrLn :: String -> IO ()
        ...

This is still hypothetical, but it shows how even IO is easily
referentially transparent (as long as you don't use unsafe* cheats).
Furthermore you have to consider that /execution/ of IO actions is
entirely outside the scope of the language itself.  A compiler turns an
expression of type "IO ()" into machine code that executes the encoded
recipe.  In any case, you have to differentiate between evaluation and
IO execution.

> 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?

Even though the World state monad is a bad intuition in my opinion, why
not?  Evaluation is referentially transparent, because you don't
evaluate to results of IO actions.  You evaluate to the IO actions
themselves.  This is not a hack, it is a great feature, because it's
precisely what allows us to build real world actions using combinators.

> 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.

It is a translation of the source code, because evaluation happens at
run-time, interleaved with the execution of 'main', as 'main' goes along
forcing thunks (in a thunk-based implementation).

> 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.

And there comes the limitation of this intuition.  It is so theoretical
that you can't express a function of that type even as machine code.  On
the other hand, the GADT variant could indeed be turned into bytecode
and then interpreted by a bytecode machine.

But this is not how it works in, say, GHC.  GHC compiles to native code
using the thunk approach I mentioned earlier.

> 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.

This is where your mistake is again:  execution vs. evaluation.  The
(>>=) operator does /not/ extract results.  It doesn't have to.  It just
makes sure (abstractly!) that the second argument is applied to the
result of the first argument at execution time.  It builds a data
dependency between monadic actions.

(>>=) is composition, not execution.  Execution is outside the scope of
the monadic interface, and for the specific case of IO it's even outside
the scope of the language.

If you think about it, you will find that (>>=) can't even extract
results.  The only thing it can do with results is to make other things
dependent on them.  This is because the type of the result is fully
polymorphic.

> 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 a black box and that's fine.  There is nothing impure about IO.

> 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.

You can objectively decide.  Referential transparency means that an
expression cannot magically evaluate to something this time and to
something other the next time, be it an Int value, a function or an IO
action.  'getLine' will always be 'getLine', and 'putStrLn "abc"' will
always be the action that prints "abc" with a line feed.  If you /had/ a
concrete representation of 'putStrLn "abc"' (like with the GADT), then
you could safely replace 'putStrLn "abc"' in the code by this
representation.  This is what you can do with all monads and everything
else in Haskell.

Again, I'm assuming you don't cheat.  If you do cheat, then you are
turning execution into evaluation, thereby potentially breaking
referential transparency.

Greets,
Ertugrul

--

-- 
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Conal Elliott | 2 Jan 19:30 2012
Picon

Re: On the purity of Haskell

On 2012/1/1 Ertugrul Söylemez <es <at> ertes.de> wrote:

Steve Horne <sh006d3592 <at> blueyonder.co.uk> wrote:
> 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.

And that's fine, because IO is an embedded DSL.  A better view of IO is
a GADT like:

   data IO :: * -> * where
       GetLine  :: IO String
       PutStrLn :: String -> IO ()
       ...

This is still hypothetical, but it shows how even IO is easily
referentially transparent (as long as you don't use unsafe* cheats).

What?? I see how a definition like this one shows how something else that you call "IO" can be denotative & RT. I don't see how what that conclusion has to do with Haskell's IO.

I also wonder whether you're assuming that all of the IO primitives we have in Haskell treat their non-IO arguments denotationally/extensionally, so that there cannot be operations like "isWHNF :: a -> IO Bool".

  - Conal
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
James Cook | 3 Jan 00:51 2012
Picon

Re: On the purity of Haskell

On Jan 2, 2012, at 1:30 PM, Conal Elliott wrote:

On 2012/1/1 Ertugrul Söylemez <es <at> ertes.de> wrote:

And that's fine, because IO is an embedded DSL.  A better view of IO is
a GADT like:

   data IO :: * -> * where
       GetLine  :: IO String
       PutStrLn :: String -> IO ()
       ...

This is still hypothetical, but it shows how even IO is easily
referentially transparent (as long as you don't use unsafe* cheats).

What?? I see how a definition like this one shows how something else that you call "IO" can be denotative & RT. I don't see how what that conclusion has to do with Haskell's IO.

Whether you say such a beast "is" IO or "something else that you call 'IO'", I don't see the problem with positing an open GADT of this form, new constructors of which are introduced by built-in magic and/or by 'foreign import', and letting the denotation of IO be terms in the free algebraic theory on the resulting signature.  It is then the job of the compiler, linker, et al, to implement a model of that algebraic theory in the machine language.  Foreign imports introduce new "external names" - constructors of the GADT  - and the linker connects those names to their "implementations" - giving them denotations as terms in the target machine's language.  Maybe I'm missing something but, in the presence of FFI, how can the world-interfacing portion of a programming language possibly be any more denotative than that?

Once you cross that threshold, I'd much rather have an operational semantics anyway.  Ultimately, programming a computer is about making the computer _do_ things.  No matter what sort of denotational semantics you come up with, I don't see any way to avoid it eventually "bottoming out" at some abstract representation which must then either have an operational semantics or an informal "everyone who matters knows what that means" semantics.  Eventually, the denotation of anything that potentially involves interaction with the real world must be "a program" in some real or imaginary machine's language.  This model chooses a very reasonable place to sever the infinite tower of turtles because it produces a language that is universal:  it is the free algebra of the signature specified by the GADT.

Incidentally, this model also addresses a concern I've heard voiced before that IO isn't demonstrably a monad.  The whole point of IO is, as I understand it, that it is a monad _by construction_ - specifically, it is the monad whose Kleisli category is the category of contexts and substitutions in the free algebraic theory generated on this signature.  There are even at least 2 published implementations of this construction in Haskell - the MonadPrompt and operational packages - and it has been shown that it does, in fact, form a monad.  I would assert that if there is any sense in which the IO type _implementation_ fails to be a monad, it is a bug and not a flaw in the concept of an IO monad.

I also wonder whether you're assuming that all of the IO primitives we have in Haskell treat their non-IO arguments denotationally/extensionally, so that there cannot be operations like "isWHNF :: a -> IO Bool".

Correct me if I'm wrong, but it appears the implication here is that [[isWHNF x]] /= [[isWHNF]] [[x]].  I don't think this is necessarily true though.  Somewhere in any formal model of any language which takes the real world into account, there must be some translation from a denotational semantics to an operational one.  If the denotational semantics is not computable, that translation necessarily must introduce some kind of "accidental" extra state.  The denotational semantics will generally include no concept of this state, so no denotation can mention it.  But I see no problem in there being a value in the denotation which is translated to an operation which does make use of this state.  In this model, [[isWHNF x]] is something like "IsWHNF [[x]]", which the compiler then translates into some code that, at run time, checks the progress of the attempt to compute the denotation of x.  At no point is there a term whose denotation depends on that state; instead, there is a computation which chooses how to proceed to do based on that state.

This does not infect the denotation with the forbidden knowledge, it only allows you to denote operations which are aware of the mechanism by which the denotation is computed.  Similarly, the operations 'peek' and 'poke' allow you to denote operations which may do unspeakably evil things at runtime, including entirely subverting that mechanism.  That doesn't mean the denotation is wrong, it means the machine has a back door.  Certainly it would be better, all other things being equal, if the translation did not open the back door like that but, as is so often the case, all other things are not equal.  The FFI and the occasional heinous performance hack are far too useful for most people to ever consider throwing out.

This may mean that my concept of Haskell does not match your definition of denotational.  But if that's the case, I'm perfectly OK with that.  Furthermore, I'd like to know how any real programming language actually could be.  In any case, the real power of Haskell's IO model is that it gives you first class procedures and treats them on an absolutely equal footing with numbers, functions, mutable references, data structures, etc.  Whether you call that "purity", "referential transparency", "denotationality", or something else, the fact is that Haskell has it and very few other languages do.  Personally, I call it "nifty".

-- James

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
AUGER Cédric | 2 Jan 01:00 2012
Picon

Re: On the purity of Haskell

Le Sun, 1 Jan 2012 16:31:51 -0500,
Dan Doel <dan.doel <at> gmail.com> a écrit :

> On Sun, Jan 1, 2012 at 3:26 PM, Ketil Malde <ketil <at> malde.org> wrote:
> > Chris Smith <cdsmith <at> gmail.com> writes:
> >
> >>> I wonder: can writing to memory be called a “computational
> >>> effect”? If yes, then every computation is impure.
> >
> > I wonder if not the important bit is that pure computations are
> > unaffected by other computations (and not whether they can affect
> > other computations). Many pure computations have side effects
> > (increases temperature, modifies hardware registers and memory,
> > etc), but their effect can only be observed in IO.
> >
> > (E.g. Debug.Trace.trace provides a non-IO interface by use of
> > unsafePerformIO which is often considered cheating, but in
> > this view it really is pure.)
> 
> The point of purity (and related concepts) is to have useful tools for
> working with and reasoning about your code. Lambda calculi can be seen
> as the prototypical functional languages, and the standard ones have
> the following nice property:
> 
>   The only difference between reduction strategies is termination.
> 
> Non-strict strategies will terminate for more expressions than strict
> ones, but that is the only difference.

This has nothing to do with purity (purity and strictness/lazyness
are different).

> 
> This property is often taken to be the nub of what it means to be a
> pure functional language. If the language is an extension of the
> lambda calculus that preserves this property, then it is a pure
> functional language. Haskell with the 'unsafe' stuff removed is such a
> language by this definition, and most GHC additions are too, depending
> on how you want to argue. It is even true with respect to the output
> of programs, but not when you're using Debug.Trace, because:
> 
>     flip (+) ("foo" `trace` 1) ("bar" `trace` 1)
> 
> will print different things with different evaluation orders.
> 
> A similar property is referential transparency, which allows you to
> factor your program however you want without changing its denotation.
> So:
> 
>     (\x -> x + x) e
> 
> is the same as:
> 
>     e + e
> 

That is not really what I call referential transparency; for me this is
rather β reduction…

For me, referential transparency means that the same two closed
expression in one context denote the same value.

So that is rather:

let x = e
    y = e
in x + y

is the same as:

e + e

> This actually fails for strict evaluation strategies unless you relax
> it to be 'same denotation up to bottoms' or some such. But not having
> to worry about whether you're changing the definedness of your
> programs by factoring/inlining is actually a useful property that
> strict languages lack.

In fact, strict language can be referentially transparent; it is the
case in ML (in fact I only know of Ocaml minus impure features, but
well…).

> 
> 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
> 

In fact IO IS referentially transparent; do NOT FORGET that there is
some syntactic sugar:

  do x <- m ; f x x
= (>>=) m (\x -> f x x)

  do x <- m ; y <- m ; f x y
= (>>=) m (\x -> (>>=) m (\y -> f x y))

So when we desugar it (and it is only desugaring, it is no
optimization/reduction/whatEverElseYouWant; these two expressions have
the same AST once parsed), where would you want to put referential
transparency?

> 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. But
> the embedded IO language lacking this property should not be confused
> with Haskell lacking this property.

It is not an "embedded IO language", it is just some sugar for monads;
you can as well do:

maybePlus :: (Mabe Int) -> (Maybe Int) -> Maybe Int
maybePlus mx my = do x <- mx
                     y <- my
                     return $ x+y

and there is absolutely no IO.

> 
> Anyhow, here's my point: these properties can be grounded in useful
> features of the language. However, for the vast majority of people,
> being able to factor their code differently and have it appear exactly
> the same to someone with a memory sniffer isn't useful. And unless
> you're doing serious crypto or something, there is no correct amount
> of heat for a program to produce. So if we're wondering about whether
> we should define purity or referential transparency to incorporate
> these things, the answer is an easy, "no." We throw out the
> possibility that 'e + e' may do more work than '(\x -> x + x) e' for
> the same reason (indeed, we often want to factor it so that it
> performs better, while still being confident that it is in some sense
> the same program, despite the fact that performing better might by
> some definitions mean that it isn't the same program).
> 
> But the stuff that shows up on stdout/stderr typically is something we
> care about, so it's sensible to include that. If you don't care what
> happens there, go ahead and use Debug.Trace. It's pure/referentially
> transparent modulo stuff you don't care about.
> 
> -- Dan
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Daniel Peebles | 2 Jan 01:22 2012
Picon

Re: On the purity of Haskell

This thread pretty much exemplifies why many people don't bother with this mailing list anymore.

On Sun, Jan 1, 2012 at 7:00 PM, AUGER Cédric <sedrikov <at> gmail.com> wrote:
Le Sun, 1 Jan 2012 16:31:51 -0500,
Dan Doel <dan.doel <at> gmail.com> a écrit :

> On Sun, Jan 1, 2012 at 3:26 PM, Ketil Malde <ketil <at> malde.org> wrote:
> > Chris Smith <cdsmith <at> gmail.com> writes:
> >
> >>> I wonder: can writing to memory be called a “computational
> >>> effect”? If yes, then every computation is impure.
> >
> > I wonder if not the important bit is that pure computations are
> > unaffected by other computations (and not whether they can affect
> > other computations). Many pure computations have side effects
> > (increases temperature, modifies hardware registers and memory,
> > etc), but their effect can only be observed in IO.
> >
> > (E.g. Debug.Trace.trace provides a non-IO interface by use of
> > unsafePerformIO which is often considered cheating, but in
> > this view it really is pure.)
>
> The point of purity (and related concepts) is to have useful tools for
> working with and reasoning about your code. Lambda calculi can be seen
> as the prototypical functional languages, and the standard ones have
> the following nice property:
>
>   The only difference between reduction strategies is termination.
>
> Non-strict strategies will terminate for more expressions than strict
> ones, but that is the only difference.

This has nothing to do with purity (purity and strictness/lazyness
are different).

>
> This property is often taken to be the nub of what it means to be a
> pure functional language. If the language is an extension of the
> lambda calculus that preserves this property, then it is a pure
> functional language. Haskell with the 'unsafe' stuff removed is such a
> language by this definition, and most GHC additions are too, depending
> on how you want to argue. It is even true with respect to the output
> of programs, but not when you're using Debug.Trace, because:
>
>     flip (+) ("foo" `trace` 1) ("bar" `trace` 1)
>
> will print different things with different evaluation orders.
>
> A similar property is referential transparency, which allows you to
> factor your program however you want without changing its denotation.
> So:
>
>     (\x -> x + x) e
>
> is the same as:
>
>     e + e
>

That is not really what I call referential transparency; for me this is
rather β reduction…

For me, referential transparency means that the same two closed
expression in one context denote the same value.

So that is rather:

let x = e
   y = e
in x + y

is the same as:

e + e

> This actually fails for strict evaluation strategies unless you relax
> it to be 'same denotation up to bottoms' or some such. But not having
> to worry about whether you're changing the definedness of your
> programs by factoring/inlining is actually a useful property that
> strict languages lack.

In fact, strict language can be referentially transparent; it is the
case in ML (in fact I only know of Ocaml minus impure features, but
well…).

>
> 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
>

In fact IO IS referentially transparent; do NOT FORGET that there is
some syntactic sugar:

 do x <- m ; f x x
= (>>=) m (\x -> f x x)

 do x <- m ; y <- m ; f x y
= (>>=) m (\x -> (>>=) m (\y -> f x y))

So when we desugar it (and it is only desugaring, it is no
optimization/reduction/whatEverElseYouWant; these two expressions have
the same AST once parsed), where would you want to put referential
transparency?

> 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. But
> the embedded IO language lacking this property should not be confused
> with Haskell lacking this property.

It is not an "embedded IO language", it is just some sugar for monads;
you can as well do:

maybePlus :: (Mabe Int) -> (Maybe Int) -> Maybe Int
maybePlus mx my = do x <- mx
                    y <- my
                    return $ x+y

and there is absolutely no IO.

>
> Anyhow, here's my point: these properties can be grounded in useful
> features of the language. However, for the vast majority of people,
> being able to factor their code differently and have it appear exactly
> the same to someone with a memory sniffer isn't useful. And unless
> you're doing serious crypto or something, there is no correct amount
> of heat for a program to produce. So if we're wondering about whether
> we should define purity or referential transparency to incorporate
> these things, the answer is an easy, "no." We throw out the
> possibility that 'e + e' may do more work than '(\x -> x + x) e' for
> the same reason (indeed, we often want to factor it so that it
> performs better, while still being confident that it is in some sense
> the same program, despite the fact that performing better might by
> some definitions mean that it isn't the same program).
>
> But the stuff that shows up on stdout/stderr typically is something we
> care about, so it's sensible to include that. If you don't care what
> happens there, go ahead and use Debug.Trace. It's pure/referentially
> transparent modulo stuff you don't care about.
>
> -- Dan
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane