www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Observational purity

reply bearophile <bearophileHUGS lycos.com> writes:
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
Aug 30 2011
next sibling parent reply =?windows-1252?Q?Alex_R=F8nne_Petersen?= <xtzgzorex gmail.com> writes:
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
Aug 30 2011
parent Timon Gehr <timon.gehr gmx.ch> writes:
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.
Aug 30 2011
prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 8/30/2011 8:31 AM, bearophile wrote:

 Time ago I have suggested a "trusted purity" to allow the implementation of
 pure function with memoization, but this observational purity seems better.



"observational purity" seems like another word for "logical const". This has 
been debated here many times.
Aug 30 2011
parent bearophile <bearophileHUGS lycos.com> writes:
Walter Bright:


 "observational purity" seems like another word for "logical const". This has 
 been debated here many times.


They show how to enforce "observational purity". I don't remember people
discussing this here.

They use observational purity just for methods called by contracts, to find a
trade-off between flexibility and analyzability. I don't remember this
discussed in this newsgroup.

So, it's not a so boring paper as you say.

Bye,
bearophile
Aug 30 2011
prev sibling parent reply Don <nospam nospam.com> writes:
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.




I didn't understand this line of the paper. Although what they propose 
clearly works for caching, I don't see how it can possibly apply to the 
log file example.

If caching is the _only_ case which is required, it can be implemented 
strictly with a special pure-aware AA, where the only access to the AA 
is a tiny piece of code:
get(Params p, pure func)
{
   static __pureAA;
   val =_pureAA.get(p);
   if (val) return *val;
   return __pureAA[p] = func(p);
}

 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
Aug 30 2011
next sibling parent reply bearophile <bearophileHUGS lycos.com> writes:
Don:


 If caching is the _only_ case which is required,


They have developed this observational purity plus a way to enforce it, to
allow static analyzability of contracts (so they are allowed to call only
observationally pure methods), while keeping them flexible enough.

Bye,
bearophile
Aug 31 2011
parent Don <nospam nospam.com> writes:
On 31.08.2011 09:35, bearophile wrote:

 Don:


 If caching is the _only_ case which is required,


 They have developed this observational purity plus a way to enforce it, to
allow static analyzability of contracts (so they are allowed to call only
observationally pure methods), while keeping them flexible enough.


That's not the impression I got, though I didn't read it very carefully.
It seemed to me that what they have, is a runtime check (an assert that 
compares a read from a static variable, with a pure function; if they're 
the same, then the static variable isn't providing any extra state). The 
static analysis is used to ensure that the runtime check is always present.

They focused on the example of caching, but I found that a bit 
misleading, since you can easily get some kind of "real" purity in that 
case (there is no observable state AND there are no observable 
side-effects).
But this is not true of other forms of observational purity. I do not 
see how allowing a call to an impure function from inside a pure one, 
could ever be anything other than a convention. So I don't see how the 
logfile example could possibly be statically checked.
Aug 31 2011
prev sibling parent reply "Marco Leise" <Marco.Leise gmx.de> writes:
Am 31.08.2011, 08:12 Uhr, schrieb Don <nospam nospam.com>:


 I didn't understand this line of the paper. Although what they propose  
 clearly works for caching, I don't see how it can possibly apply to the  
 log file example.


A log file is appended to and never read from. It is not part of the  
program state, like a temporary or cache file would be. Writing the log  
does not change an observable state in the program. Compare the file to a  
memory location in your program. Usually you don't access arbitrary raw  
memory addresses like that private member of an object that caches a  
value, but you could. Observational purity only works because we restrict  
ourselves to operations that are in the spirit of things like 'private  
members' or 'log files'. Admittedly it is possible for a language/compiler  
to disallow unsafe pointer operations, but not keep you from reading your  
log files back in.
Aug 31 2011
parent Walter Bright <newshound2 digitalmars.com> writes:
On 8/31/2011 7:55 AM, Marco Leise wrote:

 Admittedly it is
 possible for a language/compiler to disallow unsafe pointer operations, but not
 keep you from reading your log files back in.


But that's purity by convention, not by static checking.
Aug 31 2011