[Haskell-cafe] Re: philosophy of Haskell
gcross at phys.washington.edu
Wed Aug 18 15:04:07 EDT 2010
On 08/18/10 11:30, Dan Doel wrote:
> By contrast, here:
> 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''.
More information about the Haskell-Cafe