From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,1e369abf7da96fac X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Received: by 10.68.75.170 with SMTP id d10mr1439516pbw.6.1326474786958; Fri, 13 Jan 2012 09:13:06 -0800 (PST) Path: lh20ni178091pbb.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Pure function aspect?... Date: Fri, 13 Jan 2012 18:12:58 +0100 Organization: cbb software GmbH Message-ID: References: <1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com> <18gmy0hbklhv5.swfwyybigqv2$.dlg@40tude.net> <26153f03-40a0-4101-a9aa-b15f90cb0b69@h13g2000vbn.googlegroups.com> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: PPt+vSuBRqtkVsMLa1J3Dg.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit Date: 2012-01-13T18:12:58+01:00 List-Id: On Fri, 13 Jan 2012 03:01:35 -0800 (PST), Martin wrote: > On Jan 13, 8:45�am, "Dmitry A. Kazakov" > wrote: >> On Thu, 12 Jan 2012 18:00:05 -0600, Randy Brukardt wrote: >>> "Martin" 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