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.)
Best regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
