[Haskell-cafe] Re: Referential Transparency and Monads

[Heinrich Apfelmus]

minh thu wrote:
> Heinrich Apfelmus wrote:
>
>> 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 ?

No. Unlike  loop  and  loop'  which are both  _|_ ,  ones  is a proper
value, namely it's an infinite list of 1 . Granted, saying that  ones
is "terminating" is a bit silly, but it's not "non-terminating" in the
sense that it's not _|_.

The fact that some recursive definition are _|_ and some are not is
rather unsurprising when looking at functions. For instance,

   foo x = foo x                                -- is _|_
   fac n = if n == 0 then 1 else n * fac (n-1)  -- is not _|_


For more on the meaning of recursive definitions, see also

   http://en.wikibooks.org/wiki/Haskell/Denotational_semantics


Here the detailed calculation of why both  loop  and  loop'  are _|_ :

*loop*

     loop = fix f where f = \x -> x

   Hence, the iteration sequence for finding the fixed point reads

     _|_
     f _|_ = (\x -> x) _|_ = _|_

   and the sequence repeats already, so  loop = _|_ .

*loop'*

     loop' = fix f where f = \x -> putStr 'o' >> x

   Hence, the iteration sequence for finding the fixed point reads

     _|_
     f _|_ = putStr 'o' >> _|_
           = \w -> let (_,w') = putStr 'o' w in _|_ w'
           = _|_

   Again, the sequence repeats already and we have  loop' = _|_ .


Regards,
apfelmus

--
http://apfelmus.nfshost.com