<[EMAIL PROTECTED]> wrote,
> Manuel M. T. Chakravarty writes:
> > <[EMAIL PROTECTED]> wrote,
> >
> > > I'm not surprised you are puzzled. Concurrent Haskell, as
> > > implemented in ghc, does NOT preserve referential
> > > transparency, nor could it.
> >
> > Of course it does! If it wouldn't many of the optimisations
> > performed by GHC would be invalid and you would be doomed if
> > you compiled a Concurrent Haskell module with -O (actually,
> > you would most certainly already be doomed without -O).
> >
> > Check out the type signatures of the `MVar'-related
> > operations and you will find that they are all nicely
> > encapsulated in the `IO' monad.
>
> That does not help. Encapsulation within the IO monad
> forces MVar operations to be explicitly ordered only
> within the thread in which they occur; it does not effect
> the relative order with respect to MVar operations in
> other threads.
Sure, a program using IO is not necessarily deterministic.
> In summary, Concurrent Haskell only has declarative
> semantics for an individual thread (called a process in
> the paper) - the entire program does *not* have
> declarative semantics i.e it is not referentially
> transparent.
The pure lambda calculus is not the only logic on which you
can base a declarative semantics. A language based on a
semantics expressed in linear logic won't necessarily be
deterministic, but can be declarative. Given such a
semantics, there is not necessarily a contradiction to
referential transparency. Referential transparency means,
IMHO, that you can replace variables by their values
without changing the semantics of the program, ie,
let x = e1
in = [x/e1]e2
e2
This is still guaranteed in Concurrent Haskell, and it is
guaranteed due to the use of monads. This does not imply
that the `=' sign above is the equality in a model that is
restricted to deterministic computations.
Manuel
