Byakkun wrote:
On Fri, 17 Jun 2011 10:49:43 +0300, Don <[email protected]> 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.
