Hello,
recently someone in the Haskell Café [1] mentioned a paper I wish I
had been aware of earlier:
Referential Transparency, Definiteness and Unfoldability
Harald Søndergaard and Peter Sestoft
Acta Informatica 27, 505-517 (1990)
http://www.springerlink.com/content/x83n623522w8g565/fulltext.pdf
Referential transparency means different things to different people
and this paper clarifies the different concepts involved.
Briefly expressed with CRWL notation, the following notions are
distinguished:
1. Referential Transparency.
A language is said to be referentially transparent if for all
expressions e and contexts C
[| e |] = [| e' |] ==> [| C[e] |] = [| C[e'] |]
The paper defines a more detailed notion based on purely referential
positions in expressions. In CRWL, the above implication follows from
Theorem 1 of [2].
2. Definiteness.
A language is called definite if every variable denotes a single
value. So definiteness means call-time choice.
3. Unfoldability.
Unfoldability means
f x = e ==> [| f a |] = [| e[a/x] |]
This does not hold in a non-deterministic language with call-time
choice as Wolfgang once pointed out to me [3]. Indeed, the authors of
the mentioned paper argue (on page 514) that "in the presence of non-
determinism one cannot obtain both definiteness and unfoldability".
A lazy deterministic language such as Haskell has all of the above
properties which may explain the confusion when talking about
referential transparency in that context.
Although meanwhile I've had all the mentioned insights, it was a
surprise to see them explained in such an accessible way in a paper
that has been written 20 years ago. I recommend reading it!
Cheers,
Sebastian
[1]:
http://www.haskell.org/pipermail/haskell-cafe/2010-July/080323.html
[2]: Paco et al. Rewriting and Call-Time choice: The HO case. FLOPS 2008
[3]:
http://informatik.uni-kiel.de/~curry/listarchive/0819.html
--
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Do Jul 15 2010 - 11:59:15 CEST