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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
