21
$\begingroup$

A never type represents an expression that is never evaluated or the type of an expression that represents an unreachable point in a program. The return value of an exit() or abort() function could be of such a type. C partially implements this for functions only as _Noreturn but this is only a specifier and not a distinct type.

A more useful implementation would include semantics such as:

  • Being a type: never_type abort(void); instead of a specifier _Noreturn void abort().
  • Being implicitly convertible to any type: int x = abort();. The function never returns, so matching the nonexistent return 'value' to the expected type of the expression is irrelevant.
  • unreachable() or __builtin_unreachable() would have this type. These are used to designate points of the program that will never be reached during execution by the program control flow. In C these are just void typed and invoke undefined behavior if reached.

Rust has a 'never' type but many languages do not. Are there any disadvantages to including this type?

$\endgroup$
1
  • $\begingroup$ Is this concept coherent in dynamically typed languages, or only in statically typed ones? $\endgroup$ Jul 7, 2023 at 23:00

9 Answers 9

18
$\begingroup$

The C standard specifies that infinite loops with no side-effects are undefined behaviour1, and LLVM follows this, so the LLVM optimiser sometimes "optimises away" such infinite loops (by deleting them).

If the type of an infinite loop is inferred as never, then the LLVM optimiser removes the infinite loop, then you may have accidentally "produced a value" of type never, leading to unsoundness. This problem occurred in early versions of Rust, for example: see this issue.

This bug might recur if your language uses LLVM and has a never type, so be careful!


1 The reason for this is so that the compiler can delete a loop, if nothing that loop computes is ever used afterwards: now the compiler doesn't need to check that the loop terminates (which is undecidable in general) before applying this optimisation.

$\endgroup$
4
  • $\begingroup$ while(1); seems to be equivalent to *(int *)NULL = 0; or __builtin_unreachable(); $\endgroup$
    – CPlus
    May 16, 2023 at 21:30
  • $\begingroup$ One of the weird things you can do with this "optimization" is to "disprove" Fermat's Last Theroem, as long as you don't try to print the counterexample. $\endgroup$
    – dan04
    Jul 5, 2023 at 15:43
  • 1
    $\begingroup$ @dan04: A much more interesting thing one can do is cause a compiler to transform something like while(x != (uint16_t)i) i*=3; if (x < 65536) array[x] = 1; into an unconditional array[x] = 1; that will get executed even if x exceeds 65536. I doubt the Standard was ever intended to be seen as inviting such dangerous nonsense, but the authors of clang and gcc seem to think it was. $\endgroup$
    – supercat
    Nov 8, 2023 at 20:41
  • 1
    $\begingroup$ @dan04: I disagree with that blog authors' claim that compilers should be forbidden from reordering loops across following code which has no data dependencies unless they can prove the loops terminate. What should be forbidden, however, is for compilers to generate downstream code which relies upon a loop's termination condition having been satisfied, without regarding that as a data dependency upon a computation within the loop. $\endgroup$
    – supercat
    Nov 8, 2023 at 20:45
9
$\begingroup$

Transitively uninhabitable types

Swift considers all these types to behave as Never does:

  • an enum with no cases, e.g. enum Never {} itself
  • a struct or tuple with an uninhabitable field, e.g. struct Foo { var bar: Never }
  • an enum whose cases are all uninhabitable, e.g. enum E { case a(Never), b(Foo) }

This adds significant complexity to the type checker. Without being able to see type definitions, you can’t know whether My<Deeply<Nested<Struct<Type>>>> is equivalent to Never.

$\endgroup$
3
  • $\begingroup$ It would be considered 'incomplete' in a C-style language. You could not have a never typed member in a struct. $\endgroup$
    – CPlus
    May 16, 2023 at 19:50
  • $\begingroup$ Swift lets you write it. There’s not much reason to explicitly do so, but sometimes it happens with generic types. $\endgroup$
    – Bbrk24
    May 16, 2023 at 19:51
  • $\begingroup$ These rules may look complex, but if you replace struct by product, enum by sum, and Never by zero, you get "Zero can be either: the sum of zero naturals, any product that includes a zero, or a sum of numbers that are all zeros." $\endgroup$ Jul 23, 2023 at 19:57
7
$\begingroup$

If your language supports sum types, then it would be a bit duplicative to include another never type, unless it's a definition in the standard library. Because any empty sum type (like enum Never {} in Rust) is a never type.

$\endgroup$
6
$\begingroup$

never in Typescript can sometimes cause error messages to be more difficult to understand. For example:

type Foo = {a: number, b: string}

function copyField(foo1: Foo, foo2: Foo, key: 'a' | 'b'): void {
    foo2[key] = foo1[key];
}

The assignment fails with the error:

Type 'string | number' is not assignable to type 'never'.

A more useful error message might be something like:

Type 'string | number' cannot be assigned to a property of narrower type 'string & number'.

The error is that the property being assigned could either be a string or a number, so the value must be both in order to be assignable to either property. Because Typescript has a never type, the intersection string & number gets reduced to never before the error has a chance to be reported. In principle it would be possible to keep never while also improving error messages in cases like this, but it adds complexity to the compiler backend.


Another issue with never in Typescript is that a statement which produces a value of type never cannot (soundly) complete normally, so e.g. fail(); console.log("unreachable"); will never log. But this means the control-flow graph of a program depends on the types, when the types also depend on control-flow (when type guards or other narrowing conditions are checked).

This means in practice that type-checking and control-flow resolution must be done together in the same pass, because each depends on information from the other ─ again adding complexity to the compiler backend.

$\endgroup$
4
$\begingroup$

Nulls

If a language allows null to be a canonical instance of all types, then never is actually inhabited by null. You may say we can avoid this by adding a special rule, but consider the following example (with generics):

func addNull<T>(List<T> list) {
  list.add(null);
}

addNull<never>(new List<>());

In this case it's very hard to forbid null as an instance of never.

$\endgroup$
3
  • $\begingroup$ Well, if never is inhabited by null in a C-style language, then null would would just mean unreachable() and reaching it would be undefined behavior. $\endgroup$
    – CPlus
    May 16, 2023 at 21:03
  • 1
    $\begingroup$ @user16217248 This precludes null-checking. $\endgroup$
    – wizzwizz4
    May 16, 2023 at 21:53
  • 2
    $\begingroup$ Your answer makes it look like it's a downside of having a “never” type, but it's really not. Automatic null in types are a bad idea regardless. $\endgroup$ May 18, 2023 at 22:10
4
$\begingroup$

Bottom Types

I see no disadvantage in having a programming language match the mathematical theory.

What you and the answers describe as a Never type, is for me extremely close to the Bottom type, otherwise known as symbol ⊥ , or _ | _

It can symbolize abort or exit like the OP says, but for me more importantly it symbolises the indecidable/incompleteness, or impossibility to know if the computation will halt or not.

I think only programming languages that are scope-limited enough to guarantee that they will finish would benefit from not having a Bottom type.

Small calculators are probably guaranteed to finish their computations. But my culture is too limited to know many more other computing process that are sure to finish without infinite loop or crash-bug due to .... many things.

(Any correcting comment is welcome)

$\endgroup$
1
  • $\begingroup$ This seems to discuss the general topic, but not really attempt an answer. $\endgroup$ Jul 7, 2023 at 22:57
2
$\begingroup$

Mercury, being a logic language, has non-returning behaviour as part of the determinism system rather than the type system.

As well as "this has one solution" (deterministic or semideterministic) and "this may have multiple solutions" (multideterministic or nondeterministic), Mercury has two annotations which means "this has no solutions":

  • failure means that it has no solutions and it can fail. The goal fail has this determinism.
  • erroneous means that it has no solutions but it cannot fail. Goals that abort or raise an exception are examples.

The reason why this works is so that Mercury has strong modes (i.e. strong dataflow) as well. Code like this is just fine:

% semidet means that it will produce at most one solution,
% but can fail.
:- mode some_condition(in, out) is semidet.

% det means deterministic
:- mode generate_a_variable(in, out) is det.

% This never returns.
:- mode error(in) is erroneous.

:- mode p(in, out) is det.
p(X, Z) :-
    (if
        % The semantics of if-then-else is that
        % the "then" case is taken if the condition
        % succeeds, and the "else" case is taken if
        % it fails.
        some_condition(X, Y)
    then
        % Note that the variable Z here is returned from
        % the predicate.
        generate_a_variable(Y, Z)
    else
        % It doesn't matter that the variable Z is not
        % "produced" by the else case, because the compiler
        % knows this does not return.
        error("this case cannot occur")
    ).
$\endgroup$
1
$\begingroup$

Pointers

If you can cast a void* to a never* and dereference it, you have an expression of type never that doesn't actually end control flow! Consider this Swift code:

import Foundation

func unsafeAllocZeroed<T>(_: T.Type = T.self) -> UnsafeMutablePointer<T>? {
  calloc(1, MemoryLayout<T>.stride)?.bindMemory(to: T.self, capacity: 1)
}

if let ptr = unsafeAllocZeroed(Never.self) {
  print("ptr alloc'd, dereferencing")
  ptr.pointee // expression of type Never; logically, program flow may not pass here
  print("How did we get here?")
} else {
  print("that makes sense")
}

In my testing, this always prints "How did we get here?". SwiftFiddle link if you want to try it yourself.

For even more fun, you can throw the Never, and get a segfault.

$\endgroup$
4
  • 1
    $\begingroup$ This seems to be a problem with allowing this cast ─ and I don't see why the cast should be allowed. $\endgroup$
    – kaya3
    May 30, 2023 at 14:22
  • $\begingroup$ @kaya3 This is actually UB, but not for the reason you might think: ptr.pointee is referencing uninitialized memory. I also posted about this on the Swift forums, if you want to look: forums.swift.org/t/pointers-to-never/65257 $\endgroup$
    – Bbrk24
    May 30, 2023 at 17:18
  • $\begingroup$ Hmm. Unsafe code being unsafe, isn't really a disadvantage of Never. $\endgroup$ Nov 8, 2023 at 12:52
  • $\begingroup$ @EldritchConundrum In current Swift, it is possible to do this without ever typing the word Unsafe. I did it here for clarity. (Arguably that's a Swift issue and not a Never issue, but pointers being weird should still be considered.) $\endgroup$
    – Bbrk24
    Nov 8, 2023 at 22:40
1
$\begingroup$

It doesn’t play nice with cross-language interop

The C++ standard library includes a type that is exactly 1 byte, but not implicitly convertible to or from any integer or character type. It’s defined as follows:

namespace std {
enum class byte : unsigned char {};
}

If your language models sum types as enums, like in Swift or Rust, don’t assume other languages do the same. Swift made this exact mistake, so it’s perfectly legal to write

import CxxStdlib

func magic<T>(_ x: std.byte) -> T {
  switch x {}
}

and violate the memory safety rules Swift tries to maintain.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .