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