On Wednesday 18 August 2010 11:14:06 am Ertugrul Soeylemez wrote:
loop, loop' :: IO () loop = loop loop' = putStr "c" >> loop'
Huh?! Let's translate them. 'loop' becomes:
undefined
But 'loop\'' becomes:
\w0 -> let (w1, ()) = putStr "c" w0 in loop w1
Because this program runs forever it makes no sense to ask what its result is after the program is run, but that's evaluation semantics. Semantically they are both undefined. But execution is something separate and there is no Haskell notion for it.
This argument doesn't make much sense to me. The "execution" that people talk about in Haskell is conceptualizing the operation of a program written in the embedded language defined by a monad abstractly. On the other hand, the purpose of something like World -> (World, a) is to give a more denotational semantics of IO a, saying what an IO a is, as a value. The world passing model is one in which IO values are functions that accept a world, and return a transformed world. Now, moving to the two loops: loop = loop loop' = \w0 -> let (w1, ()) = putStr "c" w0 in loop' w1 How are we to distinguish between these? I know of exactly one Haskell function that can do so: seq. And this is only because it can distinguish bottom from const bottom. Extensionally, these are equal functions. Saying that the latter is different is tantamount to saying it has different side effects, because it keeps chugging through worlds. But that side steps the point of the exercise. Consider, for instance: multLoop = multLoop multLoop' = \acc0 -> let acc1 = (*) 3 acc0 in multLoop' acc1 These are also extensionally equal functions. multLoop is trivially bottom, while multLoop' keeps an ever-increasing (or, repeatedly overflowing) accumulator, but never returns. These are essentially the same as the world- passing loops above, but there's certainly no temptation to say they are not equal. That's telling, though, because I don't see any justification for treating the first set of loops differently, other than "World is magic." 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." -- Dan