Spec#, nullables and more

[bearophile]

Simen kjaeraas:

> As others have pointed out, this would be impossible for a proper
> non-nullable type. The only ways to create an array of non-nullable
> elements would be a literal, concatenation with non-nullable elements,
> or casting an existing array of nullable elements.
> 
> You do not have write access to the length of an array of non-nullable
> elements, so that you cannot increase the length (thus adding null
> elements). You can decrease the length by slicing.
> 
> This way, it should be impossible to have elements of our array that are
> null.

That's right in theory, but in practice if you want more efficiency, some other solution may be invented. See here for something about the Spec# solution:
http://www.digitalmars.com/webnews/newsgroups.php?art_group=digitalmars.D&article_id=121140

In practice the creation of the array is in two phases, in a phase the array can't be read, and its items can't be used, but they are allowed to be null. Then you use something to tell the compiler that the array is committed. Then you are free to use your array of nonnulls. At that moment the array is mutable still, but you may only assign its elements with nonnulls (using a runtime cast or just the right item of nonnull type), or you may append an nonnull item to the end of the array.

Bye,
bearophile