world as value

[Fergus Henderson]

On 17-Jun-1999, Simon Peyton-Jones <simonpj@microsoft.com> wrote:
> > Well, I think I more or less agree with you. if I try to simplify
> > things I normally come up with two more or less complementary views.
> > 
> > - if I'm interested in values, I end up with lamda calculus and
> >   functional languages.
> > - if I'm interested in actions, I end up with process algebra,
> >   CSP, and more or less the good old imperative world.
> > 
> > Well, wat would be really great is to have a proper interface between
> > these two paradigms, so than one can use both instead of choosing one.
> > 
> > And I do NOT mean calling C from a functional language, assuming
> > that the C call is 'safe'.
> 
> Concurrent Haskell was intended for just this purpose:
> 	
> http://research.microsoft.com/~simonpj/papers/concurrent-haskell.ps.gz
> 
> It explicitly adopts a 'layered' semantics:
> 
> 	- a purely functional layer, given a denotational semantics
> 
> 	- a concurrent I/O layer, using an operational semantics,
> 		in the process-calculus style

It would be quite possible to give the concurrent I/O layer
a denotational semantics too (in a way that is a consistent extension
of the denotational semantics for the purely functional layer).

It's just that the operational semantics is simpler and more convenient
for reasoning about the concurrent I/O layer.

> The conceptual point is that
> CH explicitly abandons the goal of regarding a *program* as
> a function.  Instead, the top layer has an explicit, operational
> semantics in the process-calculus style.  This 'coordiation layer'
> sits on top of a 'computation layer', which is an ordinary standard
> denotational semantics, and in which functions really are pure functions.

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 ;-)

-- 
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.