> 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