On 30-08-2011 17:31, bearophile wrote:
I've found a nice paper, "99.44% pure: Useful Abstractions in Specifications",
By Mike Barnett, David A. Naumann, Wolfram Schulte, Qi Sun (Microsoft Research, 2004):
http://www.cs.ru.nl/ftfjp/2004/Purity.pdf
It presents yet another kind of purity, "observational purity", such methods
are meant to be used inside contracts. It is quite different from the usual definition of
purity and less strict.
When specifications contain expressions that change the state of the
program, then the meaning of the program may differ depending on
whether or not the specifications are present; the two are no longer
independent. [...] We propose a definition of observational purity
and a static analysis to determine it. The intuition behind
observational purity is that a function is allowed to have
side-effects only if they are not observable to callers of the
function. [...] Our prototypical example of an observationally pure
function is one that maintains an internal cache. Changing this
internal cache is a side-effect, but it is not visible outside of
the object. Other examples are methods that write to a log file that
is not read by the rest of the program and methods that perform lazy
initialization. Algorithms that are optimized for amortized
complexity, such as a list that uses a “move to front” heuristic,
also perform significant state updates that are not visible
externally. Observationally pure methods often occur in library
code that is highly optimized and also frequently used in
specifications, e.g., the equality methods in a string library.<
So a strongly pure function with memoization becomes observationally pure :-)
This seems useful.
Time ago I have suggested a "trusted purity" to allow the implementation of
pure function with memoization, but this observational purity seems better.
Bye,
bearophile
This is exactly what I dislike about D's pure: It's *too* pure. I fully
support this idea.
- Alex
