[Haskell-cafe] Re: philosophy of Haskell

[Dan Doel]

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