[Haskell-cafe] On the purity of Haskell

[AUGER Cédric]

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