Observational purity

[Alex Rønne Petersen]

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