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.
The idea is to represent IO as an abstract data type
type IO' a = Program IOInstr a
data Program instr a where
Return :: a -> Program instr a
Then :: instr a -> (a -> Program instr b) -> Program instr b
instance Monad (Program instr) where
return = Return
(Return a) >>= g = g a
(i `Then` f) >>= g = i `Then` (\x -> f x >>= g)
date IOInstr a where
PutChar :: Char -> IOInstr ()
GetChar :: IOInstr Char
etc...
So, two values of type IO' a are equal iff their "program codes" are equal (= intensional equality), and this is indeed the case for f 42 and f (43-1) . Therefore, the (extensional) interpretations of these values by GHC are equal, too, even though you don't think we know what these interpretations are.
(Of course, programs with different source code may be extensionally equal, i.e. have the same effects. That's something we would need a semantics of IO for.)
How do you know that GHC's (or YHC's, etc) interpretation of IO is a composition of this program code interpretation with some other (more extensional) interpretation? In particular, how do you know that no IO primitive can ever distinguish between 42 and 43-1.
- Conal