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

On Monday, 19 August 2013 at 12:55:54 UTC, bearophile wrote:
> 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.
>
> Bye,
> bearophile

Right, that is pretty much it. EG:

//----
import core.stdc.stdlib;

int* myPureFun(int i) pure
{
    auto p = cast(int*) malloc(int.sizeof);
    if (!p) assert(0);
    *p = i;
    return p;
}
//----

I can solve this the same way (kind of) as with safety, by marking the function as I can mark a function as trusted, by casting the function as pure:

//----
int* myPureFun(int i) pure
{
    alias extern (C) void* function(size_t) pure PureF_t;
    auto p = cast(int*) (cast(PureF_t)&malloc)(int.sizeof);
    if (!p) assert(0);
    *p = i;
    return p;
}
//----

A basic "I know what I'm doing compiler" kind of assertion.

My only issue with doing this is I'm afraid it might be wrong: A "trusted" function means nothing to the compiler.

However, in the above example, I *marked* malloc as pure, and even though "myPureFun" is conceptually pure, *malloc* remains impure, and I don't know how the compiler deals with being told it is pure.

Is that code snippet wrong?

On Monday, 19 August 2013 at 12:55:54 UTC, bearophile wrote:
> 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

After re-reading "pure" documentation, I think I can solve the problem by marking uninitialized/minimallyInitialized as "weakly pure". From there using it in a pure context is trivial.

This is in line with what GC.malloc does.