Why does Rust have a "Never" primitive type?

Question

Rust's std::process::exit has the type

pub fn exit(code: i32) -> !

where ! is the "Never" primitive type.

Why does Rust need a special type for this?

Compare this with Haskell where the type of System.Exit.exitWith is

exitWith :: forall a. Int -> a

The corresponding Rust signature would be

pub fn exit<T>(code: i32) -> T

There is no need to monomorphize this function for different T's because a T is never materialized so compilation should still work.

Answer 1

Just make some supplement:

Never in Rust is the bottom type, and Haskell also has its bottom type, just with another name.

In type theory, a theory within mathematical logic, the bottom type is the type that has no values. It is also called the zero or empty type, and is sometimes denoted with the up tack (⊥) symbol.

https://en.wikipedia.org/wiki/Bottom_type

Most commonly used languages don't have a way to explicitly denote the empty type, but they implicitly have it, because code can have panic or infinite loop.

and site more content:

Most commonly used languages don't have a way to explicitly denote the empty type. There are a few notable exceptions.

Since Haskell2010, Haskell supports empty data types. Thus, it allows the definition data Empty (with no constructors). The type Empty is not quite empty, as it contains non-terminating programs and the undefined constant. The undefined constant is often used when you want something to have the empty type, because undefined matches any type (so is kind of a "subtype" of all types), and attempting to evaluate undefined will cause the program to abort, therefore it never returns an answer.

In Scala, the bottom type is denoted as Nothing. Besides its use for functions that just throw exceptions or otherwise don't return normally, it's also used for covariant parameterized types. For example, Scala's List is a covariant type constructor, so List[Nothing] is a subtype of List[A] for all types A. So Scala's Nil, the object for marking the end of a list of any type, belongs to the type List[Nothing].

In Rust, the bottom type is called the never type and is denoted by !. It is present in the type signature of functions guaranteed to never return, for example by calling panic!() or looping forever. It is also the type of certain control-flow keywords, such as break and return, which do not produce a value but are nonetheless usable as expressions.[4]

In TypeScript, the bottom type is never.[7][8]

In JavaScript with Closure Compiler annotations, the bottom type is !Null (literally, a non-null member of the Null unit type).

In PHP, the bottom type is never.

In Python, the bottom type is typing.NoReturn.[9]

Answer 2

TL;DR: Because it enables local reasoning, and composability.

Your idea of replacing exit() -> ! by exit<T>() -> T only considers the type system and type inference. You are right that from a type inference point of view, both are equivalent. Yet, there is more to a language than the type system.

Local reasoning for nonsensical code

The presence of ! allows local reasoning to detect nonsensical code. For example, consider:

use std::process::exit;

fn main() {
    exit(3);
    println!("Hello, World");
}

The compiler immediately flags the println! statement:

warning: unreachable statement
 --> src/main.rs:5:5
  |
5 |     println!("Hello, World");
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: #[warn(unreachable_code)] on by default
  = note: this error originates in a macro outside of the current crate
          (in Nightly builds, run with -Z external-macro-backtrace for more info)

How? Well, exit's signature makes it clear it will never return, since no instance of ! can ever be created, therefore anything after it cannot possibly be executed.

Local reasoning for optimizations

Similarly, rustc passes on this information about the signature of exit to the LLVM optimizer.

First in the declaration of exit:

; std::process::exit
; Function Attrs: noreturn
declare void @_ZN3std7process4exit17hcc1d690c14e39344E(i32) unnamed_addr #5

And then at the use site, just in case:

; playground::main
; Function Attrs: uwtable
define internal void @_ZN10playground4main17h9905b07d863859afE() unnamed_addr #0 !dbg !106 {
start:
; call std::process::exit
  call void @_ZN3std7process4exit17hcc1d690c14e39344E(i32 3), !dbg !108
  unreachable, !dbg !108
}

Composability

In C++, [[noreturn]] is an attribute. This is unfortunate, really, because it does not integrate with generic code: for a conditionally noreturn function you need to go through hoops, and the ways to pick a noreturn type are as varied as there are libraries using one.

In Rust, ! is a first-class construct, uniform across all libraries, and best of all... even libraries created without ! in mind can just work.

The best example is the Result type (Haskell's Either). Its full signature is Result<T, E> where T is the expected type and E the error type. There is nothing special about ! in Result, yet it can be instantiated with !:

#![feature(never_type)]

fn doit() -> Result<i32, !> { Ok(3) }

fn main() {
    doit().err().unwrap();
    println!("Hello, World");
}

And the compiler sees right through it:

warning: unreachable statement
 --> src/main.rs:7:5
  |
7 |     println!("Hello, World");
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^
  |
  = note: #[warn(unreachable_code)] on by default
  = note: this error originates in a macro outside of the current crate
          (in Nightly builds, run with -Z external-macro-backtrace for more info)

Composability (bis)

The ability to reason about types that cannot be instantiated also extends to reasoning about enum variants that cannot be instantiated.

For example, the following program compiles:

#![feature(never_type, exhaustive_patterns)]

fn doit() -> Result<i32, !> {
    Ok(3)
}

fn main() {
    match doit() {
        Ok(v) => println!("{}", v),
        // No Err needed
    }

    // `Ok` is the only possible variant
    let Ok(v) = doit();
    println!("{}", v);
}

Normally, Result<T, E> has two variants: Ok(T) and Err(E), and therefore matching must account for both variants.

Here, however, since ! cannot be instantiated, Err(!) cannot be, and therefore Result<T, !> has a single variant: Ok(T). The compiler therefore allows only considering the Ok case.

Conclusion

There is more to a programming language than its type system.

A programming language is about a developer communicating its intent to other developers and the machine. The Never type makes the intent of the developer clear, allowing other parties to clearly understand what the developer meant, rather than having to reconstruct the meaning from incidental clues.

Answer 3

I think the reasons why Rust needs a special type ! include:

1. The surface language doesn't offer any way to write type Never = for<T>(T) analogous to type Never = forall a. a in Haskell.

   More generally, in type aliases, one cannot use type variables (a.k.a. generic parameters) on the RHS without introducing them on the LHS, which is precisely what we want to do here. Using an empty struct/enum doesn't make sense because we want a type alias here so that Never can unify with any type, not a freshly constructed data type.

   Since this type cannot be defined by the user, it presents one reason why adding it as a primitive may make sense.

2. If one is syntactically allowed to assign a non-monomorphizable type to the RHS (such as forall a. a), the compiler will need to make an arbitrary choice w.r.t. calling conventions (as pointed out by trentcl in the comments), even though the choice doesn't really matter. Haskell and OCaml can sidestep this issue because they use a uniform memory representation.