[Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:19 AM, Heinrich Apfelmus wrote:

> Conal Elliott wrote:
>> Heinrich Apfelmus 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?
> 
> I think you can put at least these troubles to rest by noting that  f 42  and  f (43-1)  are intentionally equal, even though you're not confident on their extensional meaning.

(I think you meant "intensionally").  Ok, I think I can go with that, something like "f 42 means the sum of 42 and the user input".  And I suppose one could argue that the extension of f is well-defined as the set of integer pairs.  But that does not make f a (computable) function, because the mapping from domain to co-domain remains undefined, dependent as it is on IO.

-Gregg