Dan Doel dan.doel at gmail.com
Wed Aug 18 14:30:23 EDT 2010

```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:

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
```