2009/4/10 Heinrich Apfelmus <[email protected]>: > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > -- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
