Implementing Pure Functions

[Byakkun]

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.

(Note: my knowledge of compilers and semantic analysis is fairly limited  
so ignore this if it is plain stupid).
-- 
Using Opera's revolutionary email client: http://www.opera.com/mail/