[Swift-devel] swift write once array/struct

[Mihael Hategan]

On Sat, 2015-03-21 at 15:26 -0500, Tim Armstrong wrote:

> E.g. this script is not sensible because there's no consistent value for
> the size of the array.
> 
> int A[];
> if (size(A) == 0) {
>   A[0] = 1;
> }

Right. Which is why size(A) is only defined on a closed array in K. 

So the above example is a deadlock that could even possibly be detected
at compile time.

> 
> This script could reasonably have size(A) == 1 but I don't think it's
> reasonable to guarantee progress.
> int A[];
> if (size(A) == 1) {
>   A[0] = 1;
> }
> 
> This script could reasonably have size(A) == 1, and it might be reasonable
> to guarantee progress, since you could have some system where "intent" to
> assign the subscript is registered before the subscript is assigned.  I.e.
> it goes from EMPTY -> WILL_BE_FULL -> FULL.
> 
> int A[];
> A[0] = size(A);
> 
> Another example might be
> 
> int A[];
> if (contains(A, 0)) {
>   A[1] = x;
> }
> 
> This example could make progress if the language was smart enough to infer
> that A[0] wasn't assigned in the conditional.

That's in a sense what confuses me. If we re-write that as:

int A0, A1;
if (A0 == 1) {
   A1 = x;
}

This does, in K, result in a compile-time error. I don't see a
distinction between the two cases, and I don't understand why my brain
finds it difficult to implement it in the array case.

> 
> I think to better pin down the specification/implementation we probably
> need some kind of effect system that models more precisely which bits of
> code have what effect on the data structures  -
> http://en.wikipedia.org/wiki/Effect_system
> 
> We have a prototypical effect system with the write reference counting but
> you can have more granular ones where you track which parts of the array
> might be modified, etc.

Right.

Mihael