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. Regards, apfelmus -- http://apfelmus.nfshost.com