On 4/5/06, Robert Dockins
Hey, if we wanted a private conversation, we'd take it off-list. :-)
:-)
Do you have any reference to the fact that there is any diagreement about the term? I know it has been used sloppily at times but I think it is pretty well defined. See section 4 of the following paper: http://www.dina.kvl.dk/~sestoft/papers/SondergaardSestoft1990.pdf
http://en.wikipedia.org/wiki/Referential_transparency http://lambda-the-ultimate.org/node/1237
It may be that experts have a well defined notion of what it means, but I think that non-experts (ie, most people) have a pretty vague idea of exactly what it means.
The wikipedia article was very enlightening on this subject, especially the disclaimer on the top :-) Thanks!
So it's a standard substitutivity property. The only problem here is that Haskell has a pretty hairy denotational semantics and I don't think anyone has spelled it out in detail.
I think that may be the main problem, at least in this context. We can take a nice lovely definition of rt, as above, but its meaningless without a good semantic model. So we're forced to approximate and hand-wave, which is where the disagreement comes in.
Yes, I know what you mean. In the last few weeks this legacy of hand-waving has been showing its ugly face on the haskell-prime list as well. Maybe its time to sit down and define properly what we mean in certain contexts. It seems we would need more than one semantics to cover the different ways that reason about Haskell program. Just so that one can say: "Here I'll be using Fast'n-Loose Reasoning(TM)" or "This law holds in the Handwaving Semantics(TM)". The point is to be able to reference these precisely defined approximations and thus enjoying being both sloppy and precise at the same time. But it's real work doing this kind of thing. During a graduate course at Chalmers we started at something like this but it grew pretty hairy pretty quickly. Cheers, /Josef