How could I implement a non-null pointer qualifier in a C-style language?

Question

In C currently, pointers just are, and there are no qualifiers to tell programmers whether they can be null or not. Objective-C kind of solves this problem by adding _Nonnull and _Nullable. However these hints do not really do much besides raise compiler warnings in only a few of the many possible misuse cases.

I would like to add a stronger nonnull keyword to my C-style programming language (no nullable counterpart because nullable is just designated by the absence of nonnull). The behavior is simple: NULL is a trap representation for nonnull pointers. That is, if a pointer qualified with nonnull contains NULL and is read, immediate undefined behavior is invoked. Compilers would warn if a non nonnull pointer is dereferenced, because then NULL might be being dereferenced (also undefined behavior). This could prevent common mistakes such as not checking malloc()/fopen() for NULL, and also help avoid redundant checks on pointers that will already never be NULL.

What are the semantic options for users to convert a non nonnull to a nonnull? A basic option would be:

void *ptr = malloc(size);
if (ptr) {
    void *nonnull nnptr = ptr; // Conversion is valid because the code is unreachable if ptr is NULL
}

However, a dumb compiler may still warn at this, and this still creates redundant variables. There needs to be a syntactic way to 'convert' regular to nonnull in a way that is ergonomic and can be correctly and easily checked by the compiler. What are my options?

Answer 1

Refinement Types

NonNull is a function of type (a: PointerType) → { n ∈ a | n ≠ NULL }.
Refinement types are types whose inhabitants may be described by predicates. Other examples include

• Positive (a: Numeric) = { n ∈ a | n ⩾ 0 }
• Even (a: Numeric) = { n ∈ a | rem n 2 = 0 }
• Identifier = { s ∈ String | matches s "/[_\p{L}][_\p{L}\p{N}\xB7]*/" }

Languages supporting this include LiquidHaskell and Scala.
Dependent Types are another similar and more general candidate supported by Idris, Agda, Coq, F* and ATS.

Many languages also limit support to "non-null pointer" types, including Rust, Scala and Haskell, as well as other kinds of pointers as in Cyclone.

Automatic Type Narrowing, or Smart Casts

This is the ability to infer narrowing from supertypes to subtypes from context - in your example, from control flow analysis.
In particular, automatic narrowing to a refinement type requires proving the context satisfies that type's predicate. How "smart" a compiler has to be then depends on what kind of refinements you allow: builtin non-null pointer support is trivial compared to arbitrary predicates.

This feature is notably popular among Object-Oriented languages such as Kotlin and Ceylon for the gained ability to downcast object references based on conditions.
eg.

base class A {}
class B : A { int x; }
class C : A { float y; }
fn f(o: A)
{
    if(o is B) {
        println(o.x + 2);
    }
    else if(o is C) {
        println(o.y.ceil());
    }
}

Ceylon goes further with its if(is), if(exists) and if(nonempty) operations.
TypeScript is another popular language supporting this with the goal of representing dynamic type checks in ECMAScript, and therefore supports a range of narrowing checks such as x instanceof y, "x" in y, or x.hasOwnProperty("y"), and extends them to downcasting of union types.

Segmentation Fault (core dumped)

NULL is a trap representation for nonnull pointers. That is, if a pointer qualified with nonnull contains NULL and is read, immediate undefined behavior is invoked.

As far as actually dereferencing NULL, C already works exactly how you are describing it.
That said, note that C does not actually require NULL to represent virtual address 0, and on systems where that address is mappable, "undefined behaviour" is to be understood literally: segmentation faults and NullPointerExceptions may not exist, and only nasal demons are guaranteed.

Meanwhile Zig offers a precedent where null is required to be address 0, and where special allowzero pointer types have to carry an additional flag to represent null.