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