Re: Pure function aspect?...

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 13 Jan 2012 03:01:35 -0800 (PST), Martin wrote:

> On Jan 13, 8:45�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote:
>>> "Martin" <mar...@thedowies.com> wrote in message
>>>news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com...
>>>> Now Ada has bitten the bullet and allowed "in out" mode parameters in
>>>> functions, is it time to allow users to contract the other extreme and
>>>> allow a function to be declared Pure (no state changes, not even
>>>> hidden ones)? e.g.
>>
>>>> package P is
>>>> � type T is tagged private;
>>>> � function Pure_F � (Self : T) return Integer
>>>> � � �with Pure;
>>>> � function Impure_F (Self : T) return Integer;
>>>> private
>>>> � type T is tagged record
>>>> � � �I : Integer := 0;
>>>> � end record;
>>>> end P;
>>
>>>> Functions with a Pure contract would be allowed to call other
>>>> functions with pure contracts, read values/parameters but promise to
>>>> change nothing (not even via 'tricks' a la random number generator!!).
>>
>>> We've argued this for a long time within the ARG, and we haven't been able
>>> to get a real consensus. This discussion goes back to Ada 79 (which is even
>>> before I got involved in Ada) -- early drafts of Ada had both functions
>>> (which were what we now call pure) and value-returning procedures (which
>>> were not). The concern was that there was not a clear line between them, and
>>> moreover there are many sorts of functions that are "logically" pure but
>>> still do change things (the "memo function" being the banner carrier for
>>> that idea).
>>
>> I think that the problem may be resolved by considering the contexts where
>> the function is pure. There is no absolutely pure functions, any one is
>> impure because it returns something, pumps stack etc. The result is taken
>> out of consideration, so are local variables etc. There should be some
>> syntax for specifying what is not touched at the given level of "purity"
>> and what is.
> [snip]
> 
> Care to mock up an example of the levels you had in mind?
> 
> Is it something like (and stealing Randy's "Global"):

Global = Standard (the topmost Ada package is Standard).

A body is impure in some nested context and pure outside it. So the meaning
is not pure-in-A, but rather pure-outside-A, while impure inside A. E.g.

      with Pure => (out Foo)
          -- Pure outside the specification of Foo, can change parameters

      with Pure => (out body Foo)
          -- Pure outside the body of Foo, cannot change parameters

      with Pure => (in Standard)
          -- Pure everywhere = static, constant

   type Func is not null access function (X : Float) return Float
      with Pure => ...;
   function Integrate (F : Func) return Float
      with Pure => (out Integrate and out Func)
          -- Pure outside the specification of Integrate everwhere
          -- Func is pure as well

> A function with no pure aspect might be equivilent of:
> 
> function F1 (P1 : T1; P2 : T2) return Boolean
>   with Pure => (null);  -- no promise to not change anything local,
> global or parameter

   function F1 ...
      with Pure => (out Standard)
         -- impure, out Standard = empty set = null

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de