[Haskell-cafe] On the purity of Haskell

[Conal Elliott]

On Fri, Dec 30, 2011 at 9:19 AM, Heinrich Apfelmus <
apfelmus at quantentunnel.de> 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.
>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111230/5b7d5069/attachment.htm>