[Haskell-cafe] Re: philosophy of Haskell

[Gregory Crosswhite]

 On 08/18/10 11:30, Dan Doel wrote:
> By contrast, here:
>
>   http://code.haskell.org/~dolio/agda-share/html/IOE.html
>
> is a term model of IO. It's in Agda, for some proofs, but it's easily done in 
> GHC. And if we write the above loops in this model, we get:
>
>   loop = loop                  ==>  undefined
>   loop' = putStr "c" >> loop'  ==>  Put 'c' :>>= \_ -> loop'
>
> so the model actually represents the difference between these two loops, and 
> we don't have to fall back to saying, "well, they have different, 
> unrepresented side-effects."
I see your point here, but I think that comparing loop' to loop is
misleading because they *are* values that can be distinguished.  A
better example would be

    loop' = putStr "c" >> loop'
    loop'' = putStr "d" >> loop''

Now we have that loop' = loop''.

Cheers,
Greg