Observational purity

[Timon Gehr]

On 08/30/2011 05:44 PM, Alex Rønne Petersen wrote:
> 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

Yes, D's pure does not mean 'functionally pure'. It means 'stateless'. 
But since pure member functions can modify their object, I think it is 
usually not even such a big restriction.