Alberto G. Corona writes:

(...) Desugarize the "do" notation, after that, desugarize the >>= and >> operators down to the function call notation and suddenly everithing lost its magic because it becomes clear that a haskell monad is a sugarization of plain functional tricks.

Yep. But, BTW, could you tell me what was the result of the final desugarization and the BASIC sense of the IO monad for you? Jerzy Karczmarczuk

There are various models. One (the state monad model) of them would desugar this to:

\world0 -> let (x, world1) = getLine world0 world2 = print (x+1) world1 world3 = print (x+2) world2 in world3

Hi Ertugrul, This state monad model does not really work for IO, since it fails to capture IO's concurrency (with non-deterministic interleaving). I don't know whether/how the "EDSL model" you mention addresses concurrency or FFI. So, maybe these models are models of something other (and much less expressive) than Haskell's IO. Which re-raises Jerzy's question. Regards, - Conal On Mon, Aug 9, 2010 at 10:38 PM, Ertugrul Soeylemez wrote:

jerzy.karczmarczuk@info.unicaen.fr wrote:

...

Alberto G. Corona writes:

...

(...) Desugarize the "do" notation, after that, desugarize the >>= and >> operators down to the function call notation and suddenly everithing lost its magic because it becomes clear that a haskell monad is a sugarization of plain functional tricks.

Yep.

But, BTW, could you tell me what was the result of the final desugarization and the BASIC sense of the IO monad for you?

Example:

do x <- getLine print (x+1) print (x+2)

There are various models. One (the state monad model) of them would desugar this to:

\world0 -> let (x, world1) = getLine world0 world2 = print (x+1) world1 world3 = print (x+2) world2 in world3

Another one (the EDSL model, which I personally prefer) would desugar it to something as simple as this:

GetLine `BindIO` \x -> Print (x+1) `BindIO` const (Print (x+2))

I wonder if there are more models for IO.

Greets, Ertugrul

-- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Sat, Aug 14, 2010 at 9:27 AM, Ertugrul Soeylemez wrote:

Conal Elliott wrote:

...

...

There are various models. One (the state monad model) of them would desugar this to:

\world0 -> let (x, world1) = getLine world0 world2 = print (x+1) world1 world3 = print (x+2) world2 in world3

Hi Ertugrul,

This state monad model does not really work for IO, since it fails to capture IO's concurrency (with non-deterministic interleaving).

Well, it does capture concurrency and FFI, but it has no explicit notion for it. In other words, concurrent threads and FFI calls are effects like everything else, so the forkIO function just changes the world state implicitly and that's it.

Consider that IO's concurrency means that something else can happen between printing x+1 and printing x+2, so that x+2 is *not* printed in world2, but rather in a world influenced outside of this thread. Similarly, x+1 might not be printed in world1, and the getLine might not be executed in world0. So World -> (a, World) is *not* expressive enough to explain Haskell-IO-style concurrency. Do you see what I mean?

...

I don't know whether/how the "EDSL model" you mention addresses concurrency or FFI.

Just like the state monad model. This is not a weakness of the interpretation, but of the IO monad itself, because it is quite a raw and straightforward language for doing I/O.

And the IO monad is what Jerzy asked about. I'm pointing out that the state monad does not capture concurrency, and the "EDSL model" does not capture FFI. (Really, it depends which "EDSL model". I haven't seen one that can capture FFI. And maybe not concurrency either.)

Other approaches like functional reactive programming may be better at capturing these things, particularly the interactions between concurrent threads, at least for specific applications.

...

So, maybe these models are models of something other (and much less expressive) than Haskell's IO. Which re-raises Jerzy's question.

Haskell's IO is flexible at the cost of being quite low level. I think to capture things like concurrency properly and explicitly you need a richer sublanguage, maybe something based on the pi calculus.

Greets, Ertugrul

-- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Sat, Aug 14, 2010 at 10:11 PM, Bill Atkins wrote:

On Saturday Aug 14, 2010, at 12:50 AM, Conal Elliott wrote:

...

And the IO monad is what Jerzy asked about. I'm pointing out that the state monad does not capture concurrency, and the "EDSL model" does not capture FFI. (Really, it depends which "EDSL model". I haven't seen one that can capture FFI. And maybe not concurrency either.)

So which model captures the way the IO monad works?

I don't think anyone has given a denotational (functional-style) model for the meaning of IO. As I wrote elsewherehttp://conal.net/blog/posts/notions-of-purity-in-haskell/#comment-22829 : IO carries the collective sins of our tribe, as the scapegoat did among the ancient Hebrews. Or, as Simon Peyton Jones expressed it, “The IO monad has become Haskell’s sin-bin. Whenever we don’t understand something, we toss it in the IO monad.” (From Wearing the hair shirt – A retrospective on Haskellhttp://research.microsoft.com/en-us/um/people/simonpj/papers/haskell-retrosp....) Is it likely that we can then come along later and give a compelling and mathematically well-behaved notion of equality to our toxic waste pile? Or will it insist on behaving anti-sociably, as our own home-grown Toxic Avenger http://en.wikipedia.org/wiki/Toxic_Avenger?

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. But 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. There is nothing wrong with it being undefined. You could even have: type RealWorld = [WorldRevision] You can view execution as the transition from one state to the next, or in other words: Each time a new world value pops up, this is the current world's state. Old revisions of the world may be kept, because of late garbage collection, but only the most recent revision is the current state of the world. If you take RealWorld to be a list (at which point the two loops above /may/ be semantically different), then it's something like a movie of world revisions. The only thing which this model really cannot capture is that of premature exit of the program. However, you can change it to: type IO = ContT RealWorld (State RealWorld) which would even invalidate the above statement that the two loops can't be distinguished. At that point it would even capture exceptions. Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

On 08/18/10 11:30, Dan Doel wrote:

Now, moving to the two loops:

loop = loop loop' = \w0 -> let (w1, ()) = putStr "c" w0 in loop' w1

How are we to distinguish between these? I know of exactly one Haskell function that can do so: seq. And this is only because it can distinguish bottom from const bottom. Extensionally, these are equal functions. No, the very fact that one is bottom and the other is const bottom demonstrates that they are *not* equal.

On 08/18/10 11:30, Dan Doel wrote:

Consider, for instance:

multLoop = multLoop multLoop' = \acc0 -> let acc1 = (*) 3 acc0 in multLoop' acc1

These are also extensionally equal functions. multLoop is trivially bottom, while multLoop' keeps an ever-increasing (or, repeatedly overflowing) accumulator, but never returns. These are essentially the same as the world- passing loops above, but there's certainly no temptation to say they are not equal. I wouldn't say that they are equal at all. They are *extensionally* equal, but they aren't equal.

Cheers, Greg

On 08/18/10 11:30, Dan Doel wrote:

By contrast, here:

http://code.haskell.org/~dolio/agda-share/html/IOE.html

is a term model of IO. It's in Agda, for some proofs, but it's easily done in GHC. And if we write the above loops in this model, we get:

loop = loop ==> undefined loop' = putStr "c" >> loop' ==> Put 'c' :>>= \_ -> loop'

so the model actually represents the difference between these two loops, and we don't have to fall back to saying, "well, they have different, unrepresented side-effects." I see your point here, but I think that comparing loop' to loop is misleading because they *are* values that can be distinguished. A better example would be

loop' = putStr "c" >> loop' loop'' = putStr "d" >> loop'' Now we have that loop' = loop''. Cheers, Greg

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

Alberto G. Corona wrote:

But it seems that the trick is so productive because it comes from some fundamental properties of math, the reality, and maybe the human mind . Jost now I found this article:

Categorial Compositionality: A Category Theory Explanation for the Systematicity of Human Cognitionhttp://www.ploscompbiol.org/article/info:doi/10.1371/journal.pcbi.1000858?utm_source=feedburner&utm_medium=feed&utm_campaign=Feed:+ploscompbiol/NewArticles+(PLoS+Computational+Biology:+New+Articles)

Ooh, that looks very shiny. Thanks for sharing :) -- Live well, ~wren