[Haskell-cafe] Re: Referential Transparency and Monads

[minh thu]

2009/4/10 Heinrich Apfelmus <apfelmus at quantentunnel.de>:
> 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.

I'm not sure I follow.

> ones = 1:ones

is similar to loop or loop' but I can 'take 5' from it.

Even if loop or loop' do not terminate, some value is produced, isn't it ?

Thu