[Haskell-cafe] Re: Referential Transparency and Monads

[Eugene Kirpichov]

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

Makes sense.
The thing that is lacking to show difference between these two
functions is that there is no way to 'erase' information from the
world.
T.i., even _|_ w' can't "really" be _|_, it must be a value that
contains all the information from w'.
_|_ w' /= _|_ is nonsense, thus a state monad does not suffice. I
wonder what does...

>
> Regards,
> apfelmus
>
> --
> http://apfelmus.nfshost.com
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru