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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
