Spec#, nullables and more

[bearophile]

Walter:

> Suppose, for example, you are appending prime numbers to the array, and
> somehow appended a 25. Many moons later, something crashes because the 25 was
> not prime.

There are two main ways to avoid this bug:
- Put some test in the code, such test may be an explicit test at the point where you add items to the array (and test that this test works in the unittest of this function), or add a precondition (Contract) that tests the array contents are calling time of the function that inserts the data. Generally in D I now use both unittests and DbC.
- Wrap your data inside a struct (that contains an alias this) that has a invariant that makes sure your wrapped numbers are prime (there are type systems that allow you to attach a run-time function like isPrime() to the type system, to allow you to define a type that allows only prime numbers).


> I see it more as an argument for any restricted subset of a data type. It could
> be that you want just odd numbers in the array, and an even one crept in.

If I understand what you are meaning, you are trying to say that:
nonnulls aren't a general solution, because in general what are "correct" and "wrong" items for an array is a generic predicate, like isPrime(), so having a built-in feature to enforce isNotNull() on a type is useless because it's just a special case.

In theory this is true. But it's not the best way to design a language. Experience shows that while your items may need to satisfy a generic predicate, there are many many many situations where the predicate you want to enforce is isNotNull(Sometype) (or isIntegerInsideBound(x,low,hi)). If such enforcement is so common in programs (and if you look at Java code you may see several if == null tests), then the wise thing to do is to put in the language handy shortcuts that allow the programmer this specific case. This means adding the ?/@ type annotations I have proposed.

As you say, in some situations those ?/@ type annotations are useless because you must assure your integer numbers inside the array are prime, but practice shows this is a less common case in a Object Priented language, and even if it's not common, you can't define a simple syntax to enforce it.

You may create a syntax to attach generic predicates to a subset type, using a kind of invariant, similar to this (this is syntax sugar for a struct with alias this + struct invariant):

typedef int PrimeInt invariant() { return isPrime(this); }

This may be useful, but it's not as handy and simple as the isNull() enforcemenet managed by ?/@ suffixes. If Spec# if you have a nullable type there are several ways to use it as nonnullable.

If (x == null) {
  // in this branch you do something
} else {
  // in this branch the compiler assumes x is a nonnull type!
}

Or you may add an explicit assert:

// some code...
assert(x != null);
// here the compiler seex x as a nonnullable type
// more code...


Or even a cast, that performs a run-time test:

(cast(@)x).someMethod();

Where cast(@)x is syntax sugar for cast(typepof(x)@)x.

Bye,
bearophile