2009/4/10 Heinrich Apfelmus <[email protected]>: > Brandon S. Allbery wrote: >> Heinrich Apfelmus wrote: >> >>> loop' :: IO () >>> loop' = putStr "o" >> loop' >>> >>> are indistinguishable in the >>> >>> IO a ~ World -> (a, World) >> >> >> I still don't understand this; we are passing a World and getting a >> World back, *conceptually* the returned World is modified by putStr. >> It's not in reality, but we get the same effects if we write to a buffer >> and observe that buffer with a debugger --- state threading constrains >> the program to the rules that must be followed for ordered I/O, which is >> what matters. > > 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 ? Thu _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
