www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Re: Spec#, nullables and more

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

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:

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 ...
 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
Nov 05 2010