Implementing Pure Functions

[Don]

Byakkun wrote:
> On Fri, 17 Jun 2011 10:49:43 +0300, Don <nospam at nospam.com> wrote:
> 
>> Andrei Alexandrescu wrote:
>>> On 6/17/11 1:56 AM, Kagamin wrote:
>>>> Andrei Alexandrescu Wrote:
>>>>
>>>>> This has sparked an interesting discussion, to which I added my
>>>>> bit.
>>>>
>>>> int fun(int a) pure { if (a > 10) writeln("I'm impure); }
>>>>
>>>> As I understand, even if some calls to a function have some
>>>> repeatability properties, this doesn't mean the function is pure. In
>>>> this example fun is obviously impure. Here one can talk about
>>>> allowing to call impure functions from pure ones, but that's a way
>>>> different task.
>>>  Right. I gave that example within the context of the discussion, 
>>> which considered purity a path-sensitive property. By that 
>>> definition, if fun is provably never invoked with a > 10, then it's 
>>> effectively pure.
>>>  Andrei
>>
>> And that's an interesting thing about CTFE: although it can never do 
>> anything impure, it can call impure functions, provided it avoids the 
>> impure bits of them:
>>
>> int foo(int n)
>> {
>>     static int x = 56;
>>     if (n<10)
>>     return n;
>>     ++x;
>>     return x;
>> }
>>
>> static assert(n(5) == 5);
>>
>> Likewise, it can never doing anything unsafe, but can call unsafe 
>> functions.
>>
>> bool bar(int n)
>> {
>>     if (n < 2) return true;
>>     corruptTheStack();
>>     return false;
>> }
>>
>> static assert(bar(1));
> 
> I was wondering if you could not implement [weak] purity in the language 
> so that it requires the programmer to use contracts to insure that side 
> effects newer happen. I would imagine that this should work with the 
> semantic analysis the compiler provides without adding a specialized 
> theorem prover.

You mean like:

int foo(int n)
in pure {
    assert(n < 10);
}
body {
      static int x = 56;
      if (n<10)
	     return n;
      ++x;
      return x;
  }

where the 'in pure' contract applies only if the function is called from 
a pure function?

> (Note: my knowledge of compilers and semantic analysis is fairly limited 
> so ignore this if it is plain stupid).

That'd probably work if the compiler already had a theorem prover -- but 
it doesn't.