On Sized Types and Rereference Counting References

[DavePearce]

Some observations about array types:

• int[] is a dynamically sized array with a known length. Accesses can be checked.
• int[8] is a fixed-size array. Again, accesses can be checked.
• int[n] is a dynamically sized array with a known length determined by some variable n currently in scope. Again, accesses can be checked.
• int[?] is a dynamically sized array with an unknown length. Accesses cannot be checked.

Based on this model, we can extend to references as follows:

• &int is a reference with an dynamically sized but known number of referents. Deletion can be checked.
• &int:1 is a reference with a statically sized known of references. Deletion can be checked.
• &int:n is a reference with a dynamically sized number of referents determined by some variable n currently in scope. Again, deletion can be checked.
• &int:? is a reference with an unknown number of referents. Deletion cannot be checked (though it could be disallowed).

An interesting question here is how you create an instance of e.g. &int:2. Presumably, something like the following would be necessary:

&int:1 p = new 123
(&int:2 q, &int:2 r) = (p,p)

A similar question is how you would destroy such a reference.