Re: trusted purity?

[bearophile]

monarch_dodra:

FYI, the problem I'm trying to fix is this one:
* "uninitializedArray" returns an array with un-initialized 
elements. This, by definition, is not pure, since the value 
returned is garbage. I'm fixing the function so that it becomes 
*impure*.
* "array" is implemented in terms of "uninitializedArray": 
Allocate an array, and then fill it. "array" is pure, since its 
return is defined. array also works with ctfe.

Here are some examples of what I think you are talking about. 
foo1 is pure, foo2 is pure (but currently the type system doesn't 
complain), foo3 is pure again because all array items are 
deterministically initialized using only pure/immutable data:


// Pure:
int[3] foo1(in int x) pure {
    int[3] arr;
    return arr;
}

// Not pure:
int[3] foo2(in int x) pure {
    int[3] arr = void;
    return arr;
}

// Pure:
int[3] foo3(in int x) pure {
    int[3] arr = void;
    arr[] = x;
    return arr;
}

void main() {}


I presume foo2 should be refused as not pure. The array() 
function is like foo3, it creates data that is not pure, not 
deterministic, but then overwrites it all with referentially 
transparent information. So on the whole foo3 is pure and array() 
is often pure.

The problem is that while writing down the proof of the purity of 
foo3 is probably not too much hard, later the D compiler is not 
able to verify such proof. So some alternative solution is 
needed. The trusted pure you talk about is a solution, it means 
saying to the compiler, "trust me I have a proof of purity of 
this function". But programmers should be trusted as little as 
possible if you want a reliable language and reliable programs. 
So perhaps some mid-way solution is preferable.

Andrei used the idea of cooked and uncooked variables, it's 
probably used here:

class Bar1 {
    immutable int[2] x;
    this() {
    }
}

Bar1 gives the error:
Error: constructor test.Bar1.this missing initializer for 
immutable field x


While this gives no errors:

class Bar2 {
    immutable int[2] x;
    this() {
        x[0] = 1;
    }
}


Perhaps using a similar strategy you can accept a function like 
this:

int[3] foo3(in int x) pure {
    int[3] arr = void;
    arr[] = x;
    return arr;
}


Because now arr is not uncooked, it was overwritten by 
referentially transparent data...

For the function array() this is not enough, because instead of 
"= void" you have a function that returns some void-initialized 
data. To help the D type system a bit perhaps an annotations like 
@void_init is useful, to be attached to functions like 
uninitializedArray and minimallyInitializedArray.

Bye,
bearophile