2009/4/10 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' = _|_ .
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Eugene Kirpichov Web IR developer, market.yandex.ru