world as value

[Simon Peyton-Jones]

> I think you should say that the papers which have been 
> written about CH
> explicitly abandon that goal, rather than that CH itself 
> abandons that goal,
> because the way in which CH's semantics happen to have been 
> described is a
> property of the papers, not of CH itself.  CH does have a denotational
> semantics, it's just that no-one has written it down yet ;-)

You are clearly right: I should say that I have abandoned denotational
semantics for Concurrent Haskell, rather than saying the language does.

However, I'd be interested to know how you'd go about it.
You have to deal with I/O, concurrency, inter-thread communication
through MVars, interrupts and inter-thread signals, and so on.
This is all pretty easy to describe using a process calculus style,
but I have no idea how to do it with denotational semantics.

For a start, Concurrent Haskell is non-deterministic, so the
semantics has to acknowledge that.  

Concurrency aside, even the interaction of I/O and non-termination
is troubling.  For example, what's the semantics of

	loop = loop
	main = do { systemCall "rm Wibble.hs" ;
			loop
		 }

If we regard main as a function from World -> World,
then this function is denotationally identical:

	main = loop

Both have denotation (\world. bottom)

but the two programs are clearly different; clearly, that is, to a
user.  Some programs are designed to run for ever; their meaning
is the interactions they participate in.  

I think you end up with a denotation of the form
	World -> [World]
returning the sequence of worlds the program produces.
Only it's not-deterministic, so perhaps it's
	World -> Tree World

Anyway it seems to get hard.  Not impossible, perhaps, but
harder than my brain can deal with.

Simon