On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus
<apfelmus@quantentunnel.de> wrote:
The function
f :: Int -> IO Int
f x = getAnIntFromTheUser >>= \i -> return (i+x)
is pure according to the common definition of "pure" in the context of purely functional programming. That's because
f 42 = f (43-1) = etc.
Put differently, the function always returns the same IO action, i.e. the same value (of type IO Int) when given the same parameter.
Two questions trouble me:
How can we know whether this claim is true or not?
What does the claim even mean, i.e., what does "the same IO action" mean, considering that we lack a denotational model of IO?
- Conal