On Fri 08 Oct, Fergus Henderson wrote:
> > It is hard to sensibly define interaction between a timeless universe
> > of pure functions and values and a real universe which continually evolves
> > in real time. A state transformer method is about as good as you'll
> > get, but this requires that somehow the times of future events is
> > information which is embedded in the whatever state the program last left
> > the universe in. Perhaps some people believe this, but I don't think
> > the world works this way. (And even if this were true, unless we had
> > some systematic way of extracting this information and predicting the
> > future, it won't help us at all.)
> Whether or not the world "really" works that way, the point is that we
> can model it that way, and the world's behaviour matches the predictions
> of our model.
But unless the model is exact in _every_ detail, there will be discrepencies
between the observations of the behaviour of the model and those of reality.
How do you account for these discrepencies?
Who decides if they are significant or not?
Why is imprecise specification of these models tolerable for IO but
not for other parts of a Haskell program?
> When we say that something is _not_ referentially transparent, it means
> that we can't reason about it directly using the usual techniques of
> equational reasoning.
Yes, I agree with this, but as a consequence I would say that in general
we don't have referential transparency with IO. (Though we may have it
for a few systems which can be modelled exactly.)
> Several previous concurrent extensions to Haskell did _not_ preserve
> referential transparency, but Concurrent Haskell does, I believe.
That wasn't my impression when I read the paper, but maybe I misunderstood.
> Your suggestion on the Clean discussion list was quite vague, so perhaps
> those who responded that it would result in a loss of referential transparency
> were simply making a (pessimistic) assumption about what you meant,
> thinking it would be like the concurrent extensions to Haskell that did
> not preserve referential transparency.
Well I won't elaborate that proposal any more, other than I consider it
to be essentially the same as Concurrent Haskell (as described in the
Concurrent Haskell paper), except that with concurrency as the norm
forks would be implicit whereas in Concurrent Haskell they would have
to be explicit. So anything that is or isn't true about Concurrent Haskell
would also be true (or not) about that proposal.
And yes, we wouldn't have referential transparency with regard to the
interactions of Actions with the outside world. That's why they're
Actions, not functions. But in all other respects (I.E. anything not
related to IO) the language would have been every bit as functional
as Concurrent Haskell is (or isn't). (E.G. It's impossible for
a function to invoke an action, only actions can invoke actions.)
> > I think it's important
> > to understand whether or not we really do have referential transparency
> > with monadic IO, if other models of interaction between program and
> > outside world are (like those in Concurrent Haskell) going to be rejected
> > because we 'lose referential transparency'.
>
> The models of interaction between programs and the outside world
> in Concurrent Haskell are not going to be rejected for that reason.
Are you sure about that? I get the impression that Concurrent Haskell
is regarded very much as 'fringe Haskell'. It rarely gets a mention on
this list (in fact I cannot recall a single post re. it).
> Some _other_ attempts to add concurrency to languages like Haskell
> will be or have been rejected because the violated referential transparency,
> and thus invalidated certain proofs or program transformations that one could
> apply to programs.
I think that if invalidating some transformations regarding IO 'functions'
is the price to be paid for providing a language with what we need to
write real programs, then that's OK. I don't recall anybody rejecting
non-strict semantics because it invalidated a && b = b && a :-)
But I would agree that we don't want to do anything that turns functions
into notfunctions. That's really why I kept insisting that actions
_weren't_ functions (although everyone else seems to think they are, for
reasons I'm still unable to fathom.)
Regards
--
Adrian Hey
