Spec#, nullables and more

bearophile bearophileHUGS at lycos.com
Sat Nov 6 18:43:14 PDT 2010


Simen kjaeraas:

> 3 Can only be created with a nonzero length with a runtime check of a
>    nullable-element array/collection, or as a literal containing only
>    non-nullable elements.
> ...
> In many cases, rule #3 will
> allow you to create your collection using nullable elements, and casting
> it to non-nullable afterwards.

Spec# uses a kind of that rule 3. The main difference is that that final cast is done on the same variable. So you don't need to do:

class T {...}
T[5] tempArray; // nulls allowed, the same as T?[5]
// creates items of tempArray
T@[5] array = cast(@)tempArray;


That's not too much bad. But it requires two different variables.

Spec# does something more like this, that needs only one variable:


class T {...}
T@[5] arr; // nulls not allowed
// creation phase of array, nulls are allowed inside arr
// but you can't read arr contents
arr.done(); // imaginary syntax
// Now arr is not immutable, you may append nonnulls to
// it, replace it items with nonnulls, etc.


To allow this, the compiler has to see the type of arr as different before and after the call to the "done" function/method/attribute.

This is not different from allowing the usage of assert() to change the state of the type of a variable, as done in Spec# (this is very limited form of typestate):

void foo(T@ x) {...}
class T {...}
T t = something(); // nullable, the same as T?
assert(t !is null); // using D syntax
foo(t); // no cast to @ required here because after
        // the assert the type system knows t is not null


Something similar happens in the branch of this if:

void foo(T@ x) {...}
class T {...}
T t = something(); // nullable, the same as T?
if (t !is null) {
  foo(t); // no cast to @ required here
}

Bye,
bearophile


More information about the Digitalmars-d mailing list