[Haskell-cafe] Re: philosophy of Haskell
apfelmus at quantentunnel.de
Fri Aug 20 04:13:40 EDT 2010
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:
> 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.
More information about the Haskell-Cafe