<p>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 <code>_Nonnull</code> and <code>_Nullable</code>. However these hints do not really do much besides raise compiler warnings in only a few of the many possible misuse cases.</p>
<p>I would like to add a stronger <code>nonnull</code> keyword to my C-style programming language (no <code>nullable</code> counterpart because <code>nullable</code> is just designated by the absence of <code>nonnull</code>). The behavior is simple: <code>NULL</code> is a trap representation for <code>nonnull</code> pointers. That is, if a pointer qualified with <code>nonnull</code> contains <code>NULL</code> and is <em>read</em>, immediate undefined behavior is invoked. Compilers would warn if a non <code>nonnull</code> pointer is dereferenced, because then <code>NULL</code> might be being dereferenced (also undefined behavior). This could prevent common mistakes such as not checking <code>malloc()</code>/<code>fopen()</code> for <code>NULL</code>, and also help avoid redundant checks on pointers that will already never be <code>NULL</code>.</p>
<p>What are the semantic options for users to convert a non <code>nonnull</code> to a <code>nonnull</code>? A basic option would be:</p>
<pre><code>void *ptr = malloc(size);
if (ptr) {
    void *nonnull nnptr = ptr; // Conversion is valid because the code is unreachable if ptr is NULL
}
</code></pre>
<p>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 <code>nonnull</code> in a way that is ergonomic and can be correctly and easily checked by the compiler. What are my options?</p>

<semantics><nullability><undefined-behavior>
How could I implement a non-null pointer qualifier in a C-style language?
CC BY-SA 4.0
2023-05-22T20:24:10.357Z
Implementing the conversion check proposed in your example based on whether you're in the if-block or not may be trivial in this example, but in general its practically unsolvable because it's equivalent to the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)
chrysante
CC BY-SA 4.0
2023-05-22T20:27:47.807Z
You could make it some sort of explicit cast and say that casting a null pointer to a `nonnull` is UB. Then your compiler can implement a runtime check. But checking at compile time is (afaik) not possible in general
chrysante
CC BY-SA 4.0
2023-05-22T20:50:40.887Z
Checking at compile-time is absolutely possible, you just check conservatively and reject programs which aren't provably safe. Whenever someone invokes the halting problem to argue something is impossible, there are a hundred languages already doing it. In this case, there are two general approaches ─ control-flow type narrowing when the pointer is checked in a conditional branch (this is basically OP's suggestion), or having an [option type](https://en.wikipedia.org/wiki/Option_type) with an API for safe access.
kaya3
CC BY-SA 4.0
2023-05-22T20:53:18.207Z
@kaya3 There has to be a better way than control-flow analysis.
CPlus
CC BY-SA 4.0
2023-05-22T21:13:02.047Z
@kaya3 May I ask which languages implement such conservative control flow proofs? I'm genuinely curious, but it seems like it would be very unsatisfying to have the compiler reject perfectly valid programs because it's not able to proof their safety.
chrysante
CC BY-SA 4.0
2023-05-22T21:18:05.923Z
@chrysante Typescript is a notable example. In almost all real cases, there is no issue, and when there is it's usually straightforward to rewrite the code in a way that the compiler can recognise as valid. [The documentation](https://www.typescriptlang.org/docs/handbook/2/narrowing.html) lists exactly the conditions which can be used to narrow nullable types, so as long as your access is guarded by one of those conditions then you're fine.
kaya3
CC BY-SA 4.0
2023-05-22T21:31:10.980Z
@kaya3 Thank you, that is indeed interesting. But constructing a breaking example seems very trivial, especially since OP is implementing a C-like language where you can probably insulate code in different translation units. If the null pointer check is in a function that the compiler can't analyze it can only reject the code. I have no idea how code insulation in type script works or if it even exists but in a C-like language I feel like this would be a problem
chrysante
CC BY-SA 4.0
2023-05-22T21:35:04.233Z
@chrysante In Typescript, if the check is performed by a function then the function can be labelled as a type predicate. Typescript doesn't check the validity of type predicate functions, but the same logic used for narrowing could be used to do this (or if you're C, you could just not check them, and make it UB if a type predicate returns true when the argument doesn't satisfy the type it's supposed to check for). The goal is not to validate as many valid programs as possible, the goal is to give the programmer enough tools that it's not hard to write in a way the compiler can validate.
kaya3
CC BY-SA 4.0
2023-05-22T21:42:21.847Z
Even so, the halting problem is rarely relevant for compilers; all non-trivial static analyses (including type safety, definite assignment, and so on) can be reduced to the halting problem if the compiler must accept all valid programs and reject all invalid programs. In practice this just means compilers are written to accept most valid programs, and reject all invalid and some valid programs. For intuition, imagine a program which assigns `23` to a string variable if it finds a counterexample to Fermat's last theorem; this program is type-safe, but all real type-checkers reject it.
kaya3
CC BY-SA 4.0
2023-05-22T21:52:28.973Z
That's an interesting perspective on the topic. I only ever thought about type checking as a peephole analysis, i.e. when you encounter an int to string assignment you reject it regardless of the context. But still the idea of rejecting valid programs makes me feel uneasy somehow. But then again I had never considered your example with Fermats theorem as a valid program that I would cry over if it gets rejected, but technically it is valid of course.
chrysante
CC BY-SA 4.0
2023-05-23T01:45:10.817Z
"*if a pointer qualified with nonnull contains NULL and is read, immediate undefined behavior is invoked*" — so a valid implementation of the `nonnull` attribute would be to simply ignore it? Put `#define nonnull' at the top of any source, and you've already got what you asked for with all existing compilers. Or am I missing something?
Ray Butterworth
<h1>Refinement Types</h1>
<p><code>NonNull</code> is a function of type <code>(a: PointerType) → { n ∈ a | n ≠ NULL }</code>.<br />
<a href="https://en.wikipedia.org/wiki/Refinement_type" rel="nofollow noreferrer">Refinement types</a> are types whose inhabitants may be described by predicates.
Other examples include</p>
<ul>
<li><code>Positive (a: Numeric) = { n ∈ a | n ⩾ 0 }</code></li>
<li><code>Even (a: Numeric) = { n ∈ a | rem n 2 = 0 }</code></li>
<li><code>Identifier = { s ∈ String | matches s &quot;/[_\p{L}][_\p{L}\p{N}\xB7]*/&quot; }</code></li>
</ul>
<p>Languages supporting this include <a href="https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_03_Basic.html" rel="nofollow noreferrer">LiquidHaskell</a> and <a href="https://dotty.epfl.ch/docs/reference/other-new-features/opaques.html#bounds-for-opaque-type-aliases-1" rel="nofollow noreferrer">Scala</a>.<br />
<a href="https://en.wikipedia.org/wiki/Dependent_type" rel="nofollow noreferrer">Dependent</a> <a href="https://cs.stackexchange.com/questions/21728/dependent-types-vs-refinement-types">Types</a> are another similar and more general candidate supported by <a href="https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#dependent-types" rel="nofollow noreferrer">Idris</a>, <a href="https://agda.readthedocs.io/en/latest/language/function-definitions.html#function-definitions" rel="nofollow noreferrer">Agda</a>, Coq, F* and <a href="https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2243.html" rel="nofollow noreferrer">ATS</a>.</p>
<p>Many languages also limit support to &quot;non-null pointer&quot; types, including Rust, Scala and Haskell, as well as other kinds of pointers as in <a href="https://cyclone.thelanguage.org/wiki/Pointers/" rel="nofollow noreferrer">Cyclone</a>.</p>
<h1>Automatic Type Narrowing, or Smart Casts</h1>
<p>This is the ability to infer narrowing from supertypes to subtypes from context - in your example, from control flow analysis.<br />
In particular, automatic narrowing to a refinement type requires proving the context satisfies that type's predicate. How &quot;smart&quot; 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.</p>
<p>This feature is notably popular among Object-Oriented languages such as <a href="https://kotlinlang.org/docs/typecasts.html" rel="nofollow noreferrer">Kotlin</a> and Ceylon for the gained ability to downcast object references based on conditions.<br />
eg.</p>
<pre><code>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());
    }
}
</code></pre>
<p>Ceylon goes further with its <a href="http://web.archive.org/web/20211129230702/https://ceylon-lang.org/documentation/1.3/tour/types/#narrowing_the_type_of_an_object_reference" rel="nofollow noreferrer"><code>if(is)</code></a>, <a href="http://web.archive.org/web/20211129235401/https://ceylon-lang.org/documentation/1.3/tour/basics/#dealing_with_objects_that_aren_t_there" rel="nofollow noreferrer"><code>if(exists)</code></a> and <a href="http://web.archive.org/web/20211129230710/https://ceylon-lang.org/documentation/1.3/tour/sequences/#sequences" rel="nofollow noreferrer"><code>if(nonempty)</code></a> operations.<br />
TypeScript is another popular language supporting this with the goal of representing dynamic type checks in ECMAScript, and therefore supports <a href="https://www.typescriptlang.org/docs/handbook/2/narrowing.html" rel="nofollow noreferrer">a range of narrowing checks</a> such as <code>x instanceof y</code>, <code>&quot;x&quot; in y</code>, or <code>x.hasOwnProperty(&quot;y&quot;)</code>, and extends them to downcasting of union types.</p>
<h1>Segmentation Fault (core dumped)</h1>
<blockquote>
<p>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.</p>
</blockquote>
<p>As far as actually dereferencing NULL, C already works exactly how you are describing it.<br />
That said, note that C does not actually require <code>NULL</code> to represent virtual address 0, and on systems where that address is mappable, &quot;undefined behaviour&quot; is to be understood literally: segmentation faults and NullPointerExceptions may not exist, and only nasal demons are guaranteed.</p>
<p>Meanwhile Zig offers a <a href="https://github.com/ziglang/zig/issues/1953" rel="nofollow noreferrer">precedent</a> where <code>null</code> is <em>required</em> to be address 0, and where special <code>allowzero</code> pointer types have to carry an additional flag to represent null.</p>

CC BY-SA 4.0
2023-05-23T01:04:32.967Z
2023-05-23T02:16:30.133Z
2023-05-23T02:16:30.133Z
Longinus
CC BY-SA 4.0
2023-07-17T16:54:39.880Z
On most platforms where address zero is mappable, attempted dereference of a non-pointer would be expected to either trap in documented fashion (some compilers have an option to add code that compares pointers against zero before use in at least some cases) or else access address zero, with whatever semantics would be defined by the underlying platform.  The Standard's waiver of jurisdiction was never meant to invite gratuitously nonsensical behavior on in situations where processing code "in a documented manner characteristic of the environment" would be meaningful and useful.
supercat
# How could I implement a non-null pointer qualifier in a C-style language?
Posted by: username_0 on 2023-05-22
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?
**Tags:** semantics nullability undefined-behavior
> **Comments:**
> **username_1**: Implementing the conversion check proposed in your example based on whether you're in the if-block or not may be trivial in this example, but in general its practically unsolvable because it's equivalent to the [halting problem](https://en.wikipedia.org/wiki/Halting_problem)  
> **username_1**: You could make it some sort of explicit cast and say that casting a null pointer to a `nonnull` is UB. Then your compiler can implement a runtime check. But checking at compile time is (afaik) not possible in general  
> **username_2**: Checking at compile-time is absolutely possible, you just check conservatively and reject programs which aren't provably safe. Whenever someone invokes the halting problem to argue something is impossible, there are a hundred languages already doing it. In this case, there are two general approaches ─ control-flow type narrowing when the pointer is checked in a conditional branch (this is basically OP's suggestion), or having an [option type](https://en.wikipedia.org/wiki/Option_type) with an API for safe access.  
> **username_0**: @kaya3 There has to be a better way than control-flow analysis.  
> **username_1**: @kaya3 May I ask which languages implement such conservative control flow proofs? I'm genuinely curious, but it seems like it would be very unsatisfying to have the compiler reject perfectly valid programs because it's not able to proof their safety.  
> **username_2**: @chrysante Typescript is a notable example. In almost all real cases, there is no issue, and when there is it's usually straightforward to rewrite the code in a way that the compiler can recognise as valid. [The documentation](https://www.typescriptlang.org/docs/handbook/2/narrowing.html) lists exactly the conditions which can be used to narrow nullable types, so as long as your access is guarded by one of those conditions then you're fine.  
> **username_1**: @kaya3 Thank you, that is indeed interesting. But constructing a breaking example seems very trivial, especially since OP is implementing a C-like language where you can probably insulate code in different translation units. If the null pointer check is in a function that the compiler can't analyze it can only reject the code. I have no idea how code insulation in type script works or if it even exists but in a C-like language I feel like this would be a problem  
> **username_2**: @chrysante In Typescript, if the check is performed by a function then the function can be labelled as a type predicate. Typescript doesn't check the validity of type predicate functions, but the same logic used for narrowing could be used to do this (or if you're C, you could just not check them, and make it UB if a type predicate returns true when the argument doesn't satisfy the type it's supposed to check for). The goal is not to validate as many valid programs as possible, the goal is to give the programmer enough tools that it's not hard to write in a way the compiler can validate.  
> **username_2**: Even so, the halting problem is rarely relevant for compilers; all non-trivial static analyses (including type safety, definite assignment, and so on) can be reduced to the halting problem if the compiler must accept all valid programs and reject all invalid programs. In practice this just means compilers are written to accept most valid programs, and reject all invalid and some valid programs. For intuition, imagine a program which assigns `23` to a string variable if it finds a counterexample to Fermat's last theorem; this program is type-safe, but all real type-checkers reject it.  
> **username_1**: That's an interesting perspective on the topic. I only ever thought about type checking as a peephole analysis, i.e. when you encounter an int to string assignment you reject it regardless of the context. But still the idea of rejecting valid programs makes me feel uneasy somehow. But then again I had never considered your example with Fermats theorem as a valid program that I would cry over if it gets rejected, but technically it is valid of course.  
> **username_3**: "*if a pointer qualified with nonnull contains NULL and is read, immediate undefined behavior is invoked*" — so a valid implementation of the `nonnull` attribute would be to simply ignore it? Put `#define nonnull' at the top of any source, and you've already got what you asked for with all existing compilers. Or am I missing something?  
---
## 1 answers
### Answer by username_4 on 2023-05-23. Score: 5 | Accepted answer
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.
> **Comments:**
> **username_5** (2023-07-17): On most platforms where address zero is mappable, attempted dereference of a non-pointer would be expected to either trap in documented fashion (some compilers have an option to add code that compares pointers against zero before use in at least some cases) or else access address zero, with whatever semantics would be defined by the underlying platform.  The Standard's waiver of jurisdiction was never meant to invite gratuitously nonsensical behavior on in situations where processing code "in a documented manner characteristic of the environment" would be meaningful and useful.  
---
