On Friday 10 April 2009 3:17:39 am Eugene Kirpichov wrote:
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...
At the very least, you could probably default to a term algebra. Then, loop is still the value _|_, whereas loop' is more of a tree, like: loop' = PutStr "o" `Then` PutStr "o" `Then` PutStr "o" `Then` ... Which is a well defined value in the same way that 'fix (1:)' is. And, of course, the runtime interprets such trees to get the actual operation of your program (add conceptual constructors to the tree as you add functionality to the IO monad). It's possible a continuation passing implementation might do the trick, too, since loop' goes something like: f e k = putStr "o" $ \_ -> e k f _|_ = \k -> putStr "o" $ \_ -> _|_ k /= _|_ loop' = fix f = \k -> putStr "o" $ \_ -> loop' k although that is, perhaps, a naive implementation as far as the whole semantics of IO are concerned (but then, so is World -> a * World). I haven't thought hard about whether it's subject to similar problems. Cheers, -- Dan