[Haskell-cafe] On the purity of Haskell
pumpkingod at gmail.com
Mon Jan 2 01:22:42 CET 2012
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
> > 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
> > 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe