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



Reply via email to