[Haskell-cafe] Re: philosophy of Haskell

[Heinrich Apfelmus]

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