[Haskell-cafe] On the purity of Haskell

[Conal Elliott]

On Fri, Dec 30, 2011 at 9:11 AM, Chris Smith <cdsmith at gmail.com> wrote:

>
> > time t:  f 42   (computational process implementing func application
> > begins…)
> > t+1:   <keystroke> = 1
> > t+2:  43   (… and ends)
> >
> >
> > time t+3:  f 42
> > t+4:  <keystroke> = 2
> > t+5:  44
> >
> >
> > Conclusion:  f 42 != f 42
>
> That conclusion would only follow if the same IO action always produced
> the same result when performed twice in a row.  That's obviously untrue,
> so the conclusion doesn't follow.  What you've done is entirely
> consistent with the fact that f 42 = f 42... it just demonstrates that
> whatever f 42 is, it doesn't always produce the same result when you o
> it twice.
>

Exactly. Gregg threw in two different executions, which of course can
produce two different values, whether or not the IOs are equal.


> What Conal is getting at is that we don't have a formal model of what an
> IO action means.  Nevertheless, we know because f is a function, that
> when it is applied twice to the same argument, the values we get back
> (which are IO actions, NOT integers) are the same.


And I also raised a more fundamental question than whether this claim of
sameness is true, namely what is equality on IO? Without a precise &
consistent definition of equality, the claims like "f 42 == f (43 - 1)" are
even defined, let alone true. And since the conversation is about Haskell
IO, I'm looking for a definition that applies to all of IO, not just some
relatively well-behaved subset like putchar/getchar+IORefs+threads.

  - Conal

 - Conal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111230/e611ff81/attachment.htm>