ettolrach
(she/her)ettolrach
(she/her)Written by ettolrach, 2026-09-08.
This article uses JavaScript to render maths and to load comments. I don't use it for anything else, so I would appreciate it if you could activate JavaScript for this page :)
No LLMs were used to write this blog post.
Rust recently added the empty type to the language (waffle, 2026). In Rust, it's called ! or never. Although you could use ! for function return types before, you couldn't use it for other type annotations. The pull request which enabled this for all type annotations was merged on 25th August 2026 and is scheduled to be added to Rust 1.100 as of the time of writing.
It mostly works as you may expect it would, but there's an interesting detail which surprises most people who learn about it: expressions which have ! as part of their type don't necessarily coerce to any other type. Also, the empty and bottom types are, in fact, not necessarily the same for any language, including Rust.
We define the empty type to have no values and no constructors. We also have a function to go with it: fn absurd<A>(x: !) -> A. This function takes in any value whose type is ! and returns something of the type of your choosing (technically, it doesn't return something since it's never called because you can't ever have something of type ! to call it with, but it makes much more conceptual sense to be able to construct 'anything').
The bottom type also has no values and no constructors. However, instead of having this absurd function, we use subtyping and make it the subtype of all types. This means, thanks to how inheritance works, we can use it in place of anything else (remember that if the type A is a subtype of the type B, then we can use A whenever the code requires B).
The reason why they're different should be obvious: the empty type doesn't need our language to have subtyping while the bottom type does! Rust doesn't have subtyping for all types (it does for lifetimes, but that's irrelevant here), so it cannot have the bottom type. But there's another more practical difference between them.
First, we'll use a language with proper subtyping: Scala. Scala calls the empty type (and since it's got subtyping, the bottom type) Nothing. To make use of Nothing, we'll throw an exception. Although a thrown exception can be caught, it won't return a value to the current, local code, like how panic! works in Rust. Thus, it returns Nothing.
val f: Int => Nothing = (_) => throw Error() val g: Int => Int = f @main def main() = ()
Because of subtyping rules and a concept called variance, we don't need to do anything special here and can just specify g to use f.
In Rust, similar to Scala, we'll use panic! to not return any value (and thus returning the type !). Since Rust doesn't have subtyping, we need to make use of the absurd function. Rust implicitly puts a call to absurd around any expression whose type is !; in fact, Rust doesn't have an absurd function (I find it helpful to think that way, though), it simply implicitly typecasts an expression of type ! to any type as required. This implicit typecasting is called coercion in Rust. Importantly! If a type contains ! somewhere in it as part of a different type, such as the function type, then the coercion does not happen. That's why the below code fails to typecheck:
fn f() -> fn(i32) -> ! { |_| panic!() } fn g() -> fn(i32) -> i32 { f() } fn main() { }
This outputs the following error:
error[E0308]: mismatched types
--> src/main.rs:6:5
|
5 | fn g() -> fn(i32) -> i32 {
| -------------- expected `fn(i32) -> i32` because of return type
6 | f()
| ^^^ expected `i32`, found `!`
|
= note: expected fn pointer `fn(_) -> i32`
found fn pointer `fn(_) -> !`
Unlike with the bottom type, we can only typecast from ! to any other type. We can't do the same if it's nested in a different type. So we need to write something like the below code instead:
fn f() -> fn(i32) -> ! { |_| panic!() } fn g() -> fn(i32) -> i32 { |x| { let never: ! = f()(x); // coerces here, in other languages we would write ~absurd(never)~. never // to be more explicit, we could write: // let number: i32 = never; // return number; } } fn main() { }
And this compiles without any errors (though you'll get some unused warnings, so you'll need #[allow(unused)])! Thus, Rust isn't any less powerful than Scala. It's just a bit more awkward to use.
I hope you can see why there's a real and practical difference between the two types and why I think it's important to compare Rust's ! to the empty type, not the bottom type.
I suspect, as with many things, from Wikipedia! The page for Bottom type (Wikipedia contributors, 2026) says:
If a type system is sound, the bottom type is uninhabited and a term of bottom type represents a logical contradiction. In such systems, typically no distinction is drawn between the bottom type and the empty type, and the terms may be used interchangeably.
This is quite misleading because it looks like the only precondition of that statement is that the type system is sound. In fact, we also require the type system to have a subtyping relation, because that's how the bottom type works, by definition (which I will elaborate on below). Now, to be fair, the page for Bottom type does mention subtyping throughout, so you could forgive it and say that it's 'obvious' from surrounding context. But the page for Empty type (Wikipedia contributors, 2026) doesn't mention 'subtype' anywhere and says:
If a type system contains an empty type, the bottom type must be uninhabited too, so no distinction is drawn between them and both are denoted \(\bot\).
Again, it blue-links 'bottom type', so you could expect the reader to assume the language needs subtyping, too. But I don't think that's how most people read that sentence. This, I think, is what's been misleading people.
Sure! The following isn't really necessary to know if you're not interested in programming language theory, but if you're curious, then we should probably give a proper definition.
We define the empty type as the type with no constructors, usually denoted as \(\mathbf{0}\). We usually use \(\mathbf{0}\) for the empty type and \(\mathbf{1}\) for the unit type (which is () in Rust). The only rule the empty type has (in a non-dependently typed language) is the elimination rule:
$$ \dfrac {\Gamma \vdash L \colon \mathbf{0}} {\Gamma \vdash \texttt{case} \; L \; \texttt{\{ \}} \colon A } \quad \text{or} \quad \dfrac {\Gamma \vdash L \colon \mathbf{0}} {\Gamma \vdash \texttt{absurd}(L) \colon A } $$
As shown above, there are two ways to write this rule. In the first, we make use of pattern matching. Note how there are no cases to cover, that means there are no patterns we need to match. In the second, we make use of the function which is commonly known as absurd, whose type is \(\forall A. \mathbf{0} \to A\)1.
A quick refresher on subtypes: we define the subtyping relation \(<:\) (read as 'subtype of') such that, if \(A <: B\) for some types \(A\) and \(B\), whenever the code needs a \(B\), we may use an \(A\) instead. For example, in Java, we have that ArrayList <: AbstractList, which means we can use an ArrayList in all places where the code requires an AbstractList.
Subtyping forms a preorder (Pierce, p. 185, 2002)2. We define the bottom type, usually denoted as \(\bot\), by declaring it without constructors, too, but instead of an inference rule, we simply make it a minimal type of the subtyping preorder. In fact, we make it the least type such that \(\bot <: A\) for any type \(A\). The same can be done to define the top type, just with the \(<:\) going the other way (for all types \(A\), we have \(A <: \top\)).
Both of these definitions allow you to typecast the bottom type to any type you need. If the language has subtyping, then the empty and bottom types are the same.
How did that Scala code work, how do we know that (Int => Nothing) is a subtype of (Int => Int)? Well, the subtyping rule for functions is as follows:
$$ \dfrac {C <: A \qquad B <: D} {A \to B <: C \to D} $$
This is called being covariant in the return type. Note how the subtyping relation goes the other way for the argument, that's called being contravariant in the argument type. For more on variance, I highly recommend The Fourth Type of Variance by Benjamin Hodgson (2019). Because Nothing is a subtype of Int, the return types are indeed covariant, and this rule allows us to have (Int => Nothing) <: (Int => Int).
Having said all that, we now need to ask ourselves a question that you should always ask yourself:
Haskell has lazy evaluation, famously. There is a particularly funny combination which allows you to play with the empty type, which it calls Void, a bit more than you can in other languages:
module Main where import Data.Void import Control.Exception (assert) nameSide :: Either Void Int -> String nameSide (Left _) = "left" nameSide (Right _) = "right" main :: IO () main = do assert (nameSide leftVoid == "left") $ assert (length voidList == 2) $ return () where voidList :: [Void] -- ~undefined~ is like ~panic!()~ in Rust. voidList = [undefined, undefined] leftVoid :: Either Void Int leftVoid = Left undefined
Even though we've "created" Void, as long as we don't evaluate it, the program runs fine. In Rust, this wouldn't work because panic!() is immediately evaluated and exits the program (well, the local code at least). This is an example where laziness produces different values to strict evaluation.
Another effect of laziness is that we need to keep track of which variant of Either is currently occupied. Is it Left Void or Right Int? In Rust, we don't need to do that. We know for a fact that we cannot have a value of Ok(<something as !>). Thus, std::mem::size_of::<Result<!, i32>>() will return 4: the same size as just i32.
the two types are not the same, and Rust does not have a bottom type (currently, though I will go out on a limb and claim that such a type will never be added to Rust). But that doesn't mean that Rust isn't as expressive as a language with \(\bot\) and subtyping.
Choose a type (apart from the function type) which contains another type (using a generic) that exists in Rust and another object-oriented programming language. Let that type be A<T>. Then, like above, show how typecasting the type A<!> to A<X> for a type X of your choice is different in the object-oriented language compared to Rust.
Result (a.k.a. Either).
def getEitherNothing(): Either[Nothing, Nothing] = Left(throw Error()) // just like before, we can just use a term of type Either[Nothing, Nothing]. def getEitherRegular(): Either[Int, String] = getEitherNothing() @main def main() = ()And in Rust,
fn get_result_never() -> Result<!, !> { Ok(panic!()) } fn get_result_regular() -> Result<i32, String> { // but in Rust, we need to pattern match. match get_result_never() { Ok(n) => n, Err(n) => n, }; } fn main() {}
We know that Result<!, !> is always uninhabited, so we ought to be able to coerce it to any other type. Using subtyping, we can simply use the fact that Nothing <: Int and Nothing <: String and then conclude Either[Nothing, Nothing] <: Either[Int, String] because both type parameters of Either are covariant. In Rust, we first need to get a single ! value (which we can because both variants of Result are !), and then return that, coercing it to the required type.
abort for absurd, such as Pfenning in his lecture notes (Pfenning and Platzer, 2024) and Harper in the first edition of PFPL (Harper, 2013). However, Harper would go on to say that he regrets this and prefers the pattern matching syntax case L of { } (which he would go on to use in his second edition of PFPL) because 'abort' sounds too much like 'panic/exit the program' (Harper, 2026). Edinburgh (where I first learnt programming language theory) generally uses pattern matching, though absurd is used, too. In any case, I really like having the function absurd because it doesn't require you to have pattern matching in your language. ↑1{ x: Int, y: Int } and { y: Int, x: Int } which we could declare to be subtypes of one another, but which are not equal. ↑2