Spec#, nullables and more

[bearophile]

Thank you for this post Walter, because here you actually discuss with me/us about the topic (regardless what the final decisions will be).

Non-null types aren't a fully tidy and simple idea, they have some complexities and special situations. And probably some problems need to be improved along the way (as the refinements to pure functions done in D).

But Spec# shows a good implementation of nonnull reference types, clearly the designers have given lot of thought in that design, so ignoring their work is the wrong thing to do. The interactive site of Spec# is far from being useless, because you may put there small programs and see how Spec# behaves in some corner cases (you may also just install Spec# on your PC, but it requires time, and maybe a Windows too).

The Spec# tutorial has a section about arrays of references, so I suggest you to read that part of the document to see how they have faced the relative problems. You may even write tiny programs in the interactive site, to see how the current implementation of Spec# deals with your array-related problems and questions.

Spec# runs on a Virtual Machine, and Spec# has different purposes compared to D, so some of the design decisions of Spec# about nonnullables may be unfit for D, or we may not like them, or we may even decide to try something different just to be different and explore a different solution with different trade-offs. This is normal. But after seeing the amount of design work done on that language, it's wise to refuse those decisions only after we know and understand them, and we know why we refuse them.

The article talks about the relation between arrays and nonnullables from page 32, the section "4.1 Arrays of Non-Null Elements".

It says several things. It says that generally Spec# arrays have a type like T?[]! (T?[]@ in D syntax, I have replaced the ! with a trailing @, because in D the bang has enough purposes already).

An array like T?[]@ means it's a nonnullable array of nullable reference types.

This quotation is one of the things it says about arrays:

>Unlike fields of non-null types, whose initialization in the constructors of the class can be assured by syntactic definite-assignment rules, arrays of non-null elements are initialized by arbitrary code that follows the new allocation of the arrays. Until that initialization is completed, one cannot rely on the type of the array to accurately reflect the non-nullness of the array elements. For this reason, the Spec# type checker provides a special marker, in the form of a method NonNullType.AssertInitialized, which is used to indicate a program point where the initialization code has completed. The type checker will not give the array its declared non-null type until that point.<


Later it says, a quotation:

>Thus, before these arrays can be used as having type string[], the code must call AssertInitialized. At that call site, the program verifier checks that every array element is non-null. (At run time, AssertInitialized performs a dynamic check that the array elements are not null. The time needed to do so is proportional to the length of the array, but that is no worse than the time required to initialize the array in the first place.)<

Even later, a quotation:

>If a program tries to use the array element before the array has been given its declared type, the compiler will complain. For example, if the assignment to series[2] in Fig. 13 is replaced by series[2] = series[1], the following type error results:
Fig13.ssc(13,17): Cannot store delayed value into non(or incompatibly)delayed location
despite the fact that the right-hand side of the assignment actually does have a non-null value at that time.
Also, if the code does not include a call to AssertInitialized for an array of non-null elements, the type checker complains:
Fig13.ssc(10,14): Variable ’series’, a nonnull element array, may not have been initialized. Did you forget to call NonNullType.AssertInitialized()?
Perhaps confusingly, the source location mentioned in the error message points to where the array is declared, but this does not mean that AssertInitialized has to be called there.<


(This design maybe works, but it doesn't look wonderful. I am able to think about better ideas, like using a kind of loop variant to prove to the compiler that an array has a monotonically increasing number of nonnull items. But while this may be doable in Spec# with its advanced inferencer, it sounds not fit and maybe not doable in D).


Walter:


> Consider non-nullable type T:
> 
>    T[] a = new T[4];
>    ... time goes by ...
>    T[1] = foo;
>    T[3] = bar;
>    ... more time goes by ...
>    bar(T[2]);
> 
> In other words, I create an array that I mean to fill in later, because I don't
> have meaningful data for it in advance. What do I use to default initialize it
> with non-nullable data? And once I do that, should bar(T[2]) be an error? How
> would I detect the error?

I think that if you want to fill items of your array later, you may use a growable array (so there are never empty items in it), or you just use an array of nullable references. Nonnull isn't meant ot replace all usage cases. You use it only when you need it. If you have different needs, then you use nullable references.

Keep in mind that in this discussion has not come up another problem with nullables, that Spec# faces and solves, regarding partially initialized objects. I have shown it up a bit in my bug report:
http://d.puremagic.com/issues/show_bug.cgi?id=4571

This is an example in D-like syntax:


class Foo {}

class A {
    Foo@ name;
    this(Foo@ s) {
        this.name = s;
        this.m();
    }

    void m() { /*...*/ }
}

class B : A {
    Foo@ path;
    this(Foo@ p, Foo@ s) {
        super(s);
        this.path = p;
    }

    override void m() {
        // here this.path is null despite it's a non-null
        assert(this.path !is null);
    }
}

void main() {
    new B(new Foo, new Foo);
}


I have adapted that example from this paper, it discusses about partially uninitialized objects too:
http://research.microsoft.com/pubs/67461/non-null.pdf

A comment about that program from the paper:

>The problem with the code is that during the base call to A's constructor, the virtual method B.m may be invoked. At this time, field path of the object under construction has not yet been initialized. Thus, accesses of this.path in method B.m may yield a possibly-null value, even though the field has been declared as being non-null.<

Bye,
bearophile