Re: Pure function aspect?...

[Martin <martin@thedowies.com>]

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"):


function F1 (P1 : T1; P2 : T2) return Boolean
  with Pure => (Global, P1);  -- promise to not change globals or
parameter P1, might tamper with P2

function F1 (P1 : T1; P2 : T2) return Boolean
  with Pure => (all);  -- promise to not change anything (other than
subprogram local objects)

function F1 (P1 : in out T1) return Boolean
  with Pure => (Global);  -- promise to not change anything other than
subprogram local objects or parameters


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


-- Martin