digitalmars.D - Observational purity
- bearophile <bearophileHUGS lycos.com> Aug 30 2011
- =?windows-1252?Q?Alex_R=F8nne_Petersen?= <xtzgzorex gmail.com> Aug 30 2011
- Timon Gehr <timon.gehr gmx.ch> Aug 30 2011
- Walter Bright <newshound2 digitalmars.com> Aug 30 2011
- bearophile <bearophileHUGS lycos.com> Aug 30 2011
- Don <nospam nospam.com> Aug 30 2011
- bearophile <bearophileHUGS lycos.com> Aug 31 2011
- Don <nospam nospam.com> Aug 31 2011
- "Marco Leise" <Marco.Leise gmx.de> Aug 31 2011
- Walter Bright <newshound2 digitalmars.com> Aug 31 2011
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
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
Timon Gehr <timon.gehr gmx.ch> 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
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
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
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
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
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
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
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