Ertugrul Soeylemez wrote:
Heinrich Apfelmus wrote:In particular, the World -> (a,World) model is unsuitable even without concurrency because it cannot distinguish loop, loop' :: IO () loop = loop loop' = putStr "c" >> loop' I interpret the "EDSL model" to be the operational semantics presented in the tutorial paper.Huh?! Let's translate them. 'loop' becomes: undefined But 'loop\'' becomes: \w0 -> let (w1, ()) = putStr "c" w0 in loop w1 Because this program runs forever it makes no sense to ask what its result is after the program is run, but that's evaluation semantics. Semantically they are both undefined.
They do have well-defined semantics, namely loop = _|_ = loop' , the problem is that they are equal. You note that
execution is something separate and there is no Haskell notion for it. In particular execution is /not/ evaluation, and the program's monadic result is not related to the world state.
, but the whole point of the IO a = World -> (a, World) model is to give *denotational* semantics to IO. The goal is that two values of type IO a should do the same thing exactly when their denotations World -> (a, World) are equal. Clearly, the above examples show that this goal is not achieved.
If you also have to look at how these functions World -> (a,World) "are executed", i.e. if you cannot treat them as *pure* functions, then the world passing model is no use; it's easier to just leave IO a opaque and not introduce the complicating World metaphor.
Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
