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