[Haskell-cafe] Re: Referential Transparency and Monads

[Heinrich Apfelmus]

Brandon S. Allbery wrote:
> Heinrich Apfelmus wrote:
>
>>  loop' :: IO ()
>>  loop' = putStr "o" >> loop'
>>
>> are indistinguishable in the
>>
>>  IO a  ~  World -> (a, World)
> 
> 
> I still don't understand this; we are passing a World and getting a
> World back, *conceptually* the returned World is modified by putStr. 
> It's not in reality, but we get the same effects if we write to a buffer
> and observe that buffer with a debugger --- state threading constrains
> the program to the rules that must be followed for ordered I/O, which is
> what matters.

Basically, the problem is that neither computation returns the final
World because neither one terminates.

More precisely, the goal of the

    IO a  ~  World -> (a, World)

semantics is to assign each expression of type  IO a  a pure function
World -> (a, World) . For instance, the expression

    putChar 'c'

would be assigned a function

    \world -> ((), world where 'c' has been printed)

or similar.

Now, the problem is that both  loop  and  loop'  are being assigned the
same semantic function

    loop   ~  \world -> _|_
    loop'  ~  \world -> _|_

We can't distinguish between a function that mutilates the world and
then doesn't terminate and a function that is harmless but doesn't
terminate either. After all, both return the same result (namely _|_)
for the same input worlds.


Regards,
apfelmus

--
http://apfelmus.nfshost.com