world as value

[Fergus Henderson]

On 17-Jun-1999, Simon Peyton-Jones <simonpj@microsoft.com> wrote:
> [Fergus wrote:]
> > 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

Why does that follow?  Why should `main = loop' and `main = blah >> loop'
(`>>' is the sequencing operator implicit in the above `do' notation)
necessarily have the same denotation?
I don't think that inference is correct.

Consider for example if World is defined as a list of states,
so that it includes a history,

	data World = [State]

and `>>' is defined as

	(action1 >> action2) states0 = states0 ++ newstates1 ++ newstates2
		where states1 = action1 states0
		      states2 = action2 states1
		      newstates1 = states1 `minus` states0
		      newstates2 = states2 `minus` states1
		      list1 `minus` list2 = drop (length list2) list1

Then `loop' and `main' would have different denotations.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh@128.250.37.3        |     -- the last words of T. S. Garp.