Are there disadvantages of including a never type?

Question

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?

Answer 1

The C standard specifies that infinite loops with no side-effects are undefined behaviour¹, 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!

---

¹ 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.

Answer 2

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.

Answer 3

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.

Answer 4

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.

Answer 5

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.

Answer 6

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)

Answer 7

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")
    ).

Answer 8

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.

Answer 9

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.