<p>Some languages (Rust is the first one that comes to mind) have a &quot;never&quot; type. This is represented in Rust as <code>!</code>, and represents a function that never returns a value (i.e. by throwing an exception or entering an infinite loop). Are there any circumstances in which it would be useful to <em>return</em> (presumably an instance of) the &quot;never&quot; type from a function, or is it safe to write syntax such that it can only be used in a type signature?</p>

<syntax><types><never-type>
Are there any situations in which it would make sense to return a never type?
CC BY-SA 4.0
2023-11-07T14:15:29.300Z
I mean, wouldn't returning a "never" type then be equivalent to exiting/crashing? Otherwise, I can't really see a use for throwing the value around.
Someone
CC BY-SA 4.0
2023-11-07T14:22:59.997Z
@Someone Not necessarily; see infinite loops.
Ginger
CC BY-SA 4.0
2023-11-07T15:24:24.643Z
I'm not 100% sure what you're trying to ask, but Swift's `Never` adopts a lot of protocols like `Error`, `Comparable`, etc -- is that a useful answer? The idea is that `Never` can be used in generic contexts, such as causing a function to return `Result<T, Never>` if you know it can't fail.
Bbrk24
CC BY-SA 4.0
2023-11-07T15:25:40.033Z
@Bbrk24 I'm asking if there would ever be a situation in which `return never()` or the like would be useful, or if I'm safe to write my grammar in a way that forbids this.
Ginger
CC BY-SA 4.0
2023-11-07T16:10:47.133Z
You could have a parametrized function like `<T>(f: () -> T) -> T { return f() }` where the return type is instantiated with `never`. But there's no need to accept a concrete `never` type like in `return never()` (your analysis could simply accept `never()` as the last line of a function which returns anything)
tarzh
CC BY-SA 4.0
2023-11-07T17:24:53.753Z
@Ginger If you're in a known contradictory situation, like a pattern match branch that is known to be unreachable, then it is ok (and even useful). If it's possible to construct a `never` value in *reachable* situations, however, then you will likely break type safety. This is because, usually, a defining characteristic of an empty type is that you can obtain value of any type you want if you're given a value of an empty type (this is sometimes called "false elimination," "ex falso" or "the principle of explosion").
David Young
CC BY-SA 4.0
2023-11-07T19:03:39.757Z
When you talk about a function returning some type, normally we consider the return type as a static declaration, i.e. the type written in the function's declaration. But here you are talking about the "never" type as representing *"a function that never returns a value"*, which is really a runtime property, since it's about the value returned, not just the declared type. If you're asking if it makes sense for a function to *declare* a return type of "never" then the answer is quite different to if it makes sense for a function to return a *value* of type "never". So, please clarify.
kaya3
CC BY-SA 4.0
2023-11-09T17:40:20.550Z
The question seems to be equally applicable to `void` (as in C and C++), which is also un-inhabited, but I gather that `void` is different from `Never` (in that `void` functions do return control, but `Never` functions don't). ¿Are you asking for both?
Pablo H
CC BY-SA 4.0
2023-11-09T21:09:27.990Z
If by a “never type” you mean the bottom type, it does not make sense to return an actual instance of it because by definition, there *is* no actual instance of it.
xigoi
<p>This would commonly be used in a branching logic to show that a branch should never be reached. For example, in a <code>CASE</code> expression:</p>
<pre><code>function X(value: ABCEnumeration): int
{
  case(value)
  {
    when ABCEnumeration.A: return 1;
    when ABCEnumeration.B: return 2;
    when ABCEnumeration.C: return 3;
    default:               return never;
  }
}
</code></pre>
<p>It allows the author to explicitly state that assuming that the input to the function meets the contract for the function (which is particularly relevant for untyped languages <a href="https://typing.readthedocs.io/en/latest/source/unreachable.html" rel="noreferrer">such as Python</a>) that there is a branch that could be considered but will never actually be reached.</p>
<p>It also assists static analysis and coverage tools to know that all branches have been considered.</p>
<p>Depending on how your language was written, the syntax could be <code>return never;</code> (if a <code>return</code> statement is expected from each branch of the logic) or using just <code>never;</code> or <code>assert_never(value);</code> (as per <a href="https://typing.readthedocs.io/en/latest/source/unreachable.html#assert-never-and-exhaustiveness-checking" rel="noreferrer">python</a>) if the syntax supports not having return statements on some branches.</p>

CC BY-SA 4.0
2023-11-08T09:22:01.863Z
2023-11-08T09:37:42.727Z
2023-11-08T09:37:42.727Z
MT0
CC BY-SA 4.0
2023-11-09T17:49:17.780Z
`never` could be "an expression of type `Never`" (that doesn't get executed; and akin to a function of type `Never`), to avoid having values of type `Never.
Pablo H
CC BY-SA 4.0
2023-11-10T14:38:26.153Z
If you could prove at compile-time that the default branch is impossible to reach, then you could just as well allow the developer to omit it in that case.  If you can't prove it, then you need to define the behavior that happens if that branch gets reached regardless. You can't actually return `never`, so you would have to throw a runtime error. So why not make the default branch throw a runtime error in the first place?
Philipp
<p>&quot;Never types&quot; (also called empty types) are extremely useful in proof assistants. Here's an example in Agda.</p>
<p>What does it look like to &quot;return&quot; a never type in a programming language like Agda? What does it mean and what sort of syntax is used for this? We will see soon!</p>
<p>In short, I will prove that a non-empty list type always has a non-zero length. This proof will be a function that returns a never type. In general, you prove a negation by writing a function that produces the never type. If that function type checks, then you know your proof is correct.</p>
<p>Such a proof can be useful inside actual programs as well (not just proving things to prove things). This is outside the scope of this answer, though.</p>
<p>I'll also set up this answer where if you copy all the code blocks and put them into an Agda file together, it will work.</p>
<p>Here's an outline of what I'm about to do:</p>
<ul>
<li>Define a type for natural numbers (non-negative integers)</li>
<li>Define a type for &quot;size indexed&quot; non-empty lists. This means the size of the list is &quot;tracked&quot; as a type parameter for the list type. This is <em>somewhat</em> like C++'s <code>std::array</code> (in the sense that the size is a kind of type parameter in both).</li>
<li>To show the basic syntax of Agda, I will write an <code>extract</code> function which will returns the head of the list. This is okay to do because the list always has at least one element.</li>
<li>Because these lists are non-empty, the size will never be zero. I will write a function that proves this by taking a &quot;non-empty list with size zero&quot; and giving back the &quot;never type&quot;</li>
</ul>
<p>Now to the code. First, an import:</p>
<pre><code>open import Data.Empty
</code></pre>
<p>This is just importing the empty type from the standard library. In Agda, this type is called <code>⊥</code> and can be pronounced &quot;bottom&quot;. It has no constructors. There is no way to make a value of type <code>⊥</code> unless we are in a (provably) contradictory situation.</p>
<pre><code>data Nat : Set where
  Z : Nat
  S : Nat → Nat
</code></pre>
<p>Our natural number type has two constructors: One for zero (<code>Z</code>) and one for successor (<code>S</code>). The <code>Z</code> constructor doesn't take any arguments. The <code>S</code> constructor takes one argument: a <code>Nat</code>. So, 0 is <code>Z</code> and 3 is <code>S (S (S Z))</code>. This kind of representation is nice for most proof assistant purposes because you can very straightforwardly do induction on it.</p>
<p>Now, the definition of size-indexed non-empty lists:</p>
<pre><code>data NonEmpty (A : Set) : Nat → Set where
  One : A → NonEmpty A (S Z)
  Cons : {n : Nat} → A → NonEmpty A n → NonEmpty A (S n)
</code></pre>
<p>You can ignore the <code>A</code>s. This is just the &quot;usual&quot; type parameter: That is, the type of <em>elements</em> of the list. <code>NonEmpty</code> has two type parameters: the first is the type of elements and the second is the list size.</p>
<p>We have two cases: the case for lists with exactly one element (<code>One</code>) and the case for a cons-cell (<code>Cons</code>). In the first case, we have exactly one element and our size parameter is <code>S Z</code> (the successor of 0, aka 1). In the second case, we have a head element and a tail list. In the <code>Cons</code> case, the tail list has size <code>n</code>, so the overall list has size <code>S n</code>.</p>
<p>The curly braces means that the <code>n</code> in the <code>Cons</code> case is an implicit parameter. You do not really need to pay attention to that part.</p>
<p>Now, the <code>extract</code> function:</p>
<pre><code>extract : ∀ {A} →
  (n : Nat) →
  NonEmpty A n →
  A
extract n (One x) = x
extract n (Cons x xs) = x
</code></pre>
<p>We take in a element type <code>A</code> (again, implicit parameter in curly braces), a natural number <code>n</code>, a non-empty list of size <code>n</code> and we give back something of type <code>A</code>. We handle the two <code>NonEmpty</code> cases using a pattern match. In both cases, we just give back the first element.</p>
<p>Finally, we get to something with the never type!</p>
<pre><code>nonempty-nonzero : ∀ {A} →
  NonEmpty A Z →
  ⊥
nonempty-nonzero ()
</code></pre>
<p>Our function takes a non-empty list where the size parameter is <code>Z</code>. This is never possible, since <code>One</code> and <code>Cons</code> both have size parameters that are successors of some natural number. 0 is not the successor of a natural number. We give back <code>⊥</code>, the never type.</p>
<p>Since we know that the <code>NonEmpty A Z</code> value we were given can never exist (and this follows immediately from the definition of <code>NonEmpty</code>), we write <code>()</code> for the pattern match on our non-empty argument. Note that we didn't even give a function body here, unlike with <code>extract</code>.</p>
<p><code>()</code> is Agda's syntax for an &quot;absurd pattern match&quot;. It will only type check if Agda can immediately see that this pattern match case is impossible. And it does type check here, so Agda <em>does</em> see that this is impossible!</p>
<p>So, we didn't <em>exactly</em> &quot;return&quot; a <code>⊥</code> value, at least not using the &quot;usual&quot; syntax to return something. We proved to Agda that we are in an impossible situation, so we didn't <em>have</em> to return anything at all! Which is great, because we cannot build a value of type <code>⊥</code>. Although, changing subjects slightly, if we happened to already have <code>⊥</code> value that we got from somewhere, we could absolutely return it. But that would be a different example.</p>
<h1>Further Reading</h1>
<ul>
<li><a href="https://plfa.github.io/" rel="nofollow noreferrer">Programming Language Foundations in Agda</a>: This is a free online book that goes over both the basics of Agda and introduces its use in studying programming languages. The section in Part 1 titled &quot;Negation&quot; is particularly relevant, though the empty type does appear in other places as well.</li>
</ul>

CC BY-SA 4.0
2023-11-09T17:43:17.180Z
2023-11-09T23:37:45.003Z
2023-11-09T23:37:45.003Z
David Young
<p>It can be useful to allow expressions of type <code>Never</code> where something else would be expected. For example, the following code is type-safe, but Swift doesn't allow it:</p>
<pre class="lang-swift prettyprint-override"><code>func yeet(_ error: Error) throws -&gt; Never {
  throw error
}

func unwrapOrThrow&lt;T&gt;(_ value: T?) throws -&gt; T {
  return value ?? try yeet(MyError(&quot;Expected value&quot;))
}
</code></pre>
<p>I had originally tried this to work around the fact that Swift lacks <code>throw</code>-expressions. (It is still possible if you make <code>yeet</code> itself generic, but there's no conceptual reason that making it return <code>Never</code> shouldn't also work.)</p>

CC BY-SA 4.0
2023-11-07T15:37:23.263Z
2023-11-07T15:37:23.263Z
Bbrk24
<p>Some languages have the NaN - like concept that can be used to chain multiple calls:</p>
<pre><code>  value = object.method1(...).method2(...).method3(....);
  if value == std::wrong then ...
</code></pre>
<p>If <code>method1</code> returns something like <code>wrong</code>, further calls do not evaluate at all and the final result is <code>wrong</code> that can be checked. This removes the need to check the success of calling <code>method1</code>, <code>method2</code> and <code>method3</code> individually, if the handling is identical regardless which one of them fails. It is not the same as <em>null</em> that would throw null pointer exception if <code>method1</code> or <code>method2</code> fails.</p>
<p>And, generally, I think NaN is also that you are talking about. The rationale is that mathematical expression may be very complex, and something like 0 is a likely valid result. If one does not want to work with exceptions, the alternative way is to calculate everything wrong as NaN, and then cascade this assuming that any operator of NaN returns NaN as well. NaN would be safely calculated for the whole expression, regardless where something went wrong.</p>

CC BY-SA 4.0
2023-11-09T08:11:41.200Z
2023-11-09T08:11:41.200Z
Audrius Meškauskas
CC BY-SA 4.0
2023-11-09T16:35:20.123Z
NaN is more like the "nothing case" of an optional type (like ML's `NONE` for the `option` type, Haskell's `Nothing` for the `Maybe` type). On the other hand, an *empty type* is a type that literally has no values. It is not possible to *actually* construct a value of an empty type. You can only "construct" a value of such a type when you are in a branch that you know will never be reached. For example, in the body of something like `if (1 == 0) { ... }`. That's a very artificial example, but there are situations where that can actually be very useful. Also, NaN is usually specific to `float`s
David Young
CC BY-SA 4.0
2023-11-09T17:46:58.787Z
Similar to the null object (nil?) in Smalltalk, that accepts every message, mostly returning itself.
Pablo H
<p>I could imagine there being a language where a function that never returns can throw an exception, and the exception handler returning something to the block that contains it.</p>

CC BY-SA 4.0
2023-11-08T10:50:38.353Z
2023-11-12T17:36:57.963Z
2023-11-12T17:36:57.963Z
Davislor
<p>If you have a function <code>f1()</code> that returns <code>Never</code>,</p>
<p>and you are writing a function <code>f2()</code> that also returns <code>Never</code>,</p>
<p>and the last thing <code>f2</code> does is call <code>f1</code>,</p>
<p>then it is conceivable that you write the last statement of <code>f2</code> as <code>return f1()</code>, therefore returning <code>Never</code>.</p>
<p>Note that we are returning the <code>Never</code> type, but we are not returning an <em>instance</em> of <code>Never</code>, because <code>Never</code> does not and cannot have any instance.</p>
<p>We are simply proving to the compiler that our function <code>f2</code> never returns, and the proof is expressed like this: <code>f2</code> doesn't return because <code>f1</code> doesn't.</p>

CC BY-SA 4.0
2023-11-07T17:44:44.220Z
2023-11-07T17:56:03.247Z
2023-11-07T17:56:03.247Z
Eldritch Conundrum
CC BY-SA 4.0
2023-11-10T00:43:27.343Z
This pattern is very useful in templated code.  Often one does not know whether f1() returns Never or some other type.  Permitting `return f1()` when f1 returns Never is a syntactic convenience that can earn its keep quite quickly.  This syntax is used in C++
Cort Ammon
<p>The <code>never</code> type is often an <a href="https://cs.stackexchange.com/q/134215/6729"><em>un-inhabited type</em></a>, i.e., a type that is not inhabited by any value. Therefore, there is no value you could return.</p>
<p>For example, in Scala, I cannot imagine any way to make <a href="https://scastie.scala-lang.org/JoergWMittag/Iy2DgZnyRFiixYnfpvWziw" rel="noreferrer">something like the following</a> compile:</p>
<pre class="lang-scala prettyprint-override"><code>def foo: Nothing = return
</code></pre>
<p>This will result in a type error.</p>
<p>You can, of course, return the result of evaluating an expression that has the <code>never</code> type, e.g., <a href="https://scastie.scala-lang.org/JoergWMittag/NrZAwmx2S3yeTWVay3XEDw" rel="noreferrer">something like this</a>:</p>
<pre class="lang-scala prettyprint-override"><code>def foo: Nothing = ???
</code></pre>
<p>This compiles because <a href="https://scala-lang.org/api/3.3.1/scala/Predef$.html#???-0" rel="noreferrer"><code>???</code></a> is itself <a href="https://github.com/scala/scala/blob/2.13.x/src/library/scala/Predef.scala#L340-L344" rel="noreferrer">defined like this</a>:</p>
<pre class="lang-scala prettyprint-override"><code>def ??? : Nothing = throw new NotImplementedError
</code></pre>
<p>But in the end, you will never return a value, since, no matter how many levels of indirection you chain, <em>there is no value</em>.</p>

CC BY-SA 4.0
2023-11-07T14:31:27.847Z
2023-11-07T14:41:17.453Z
2023-11-07T14:41:17.453Z
Jörg W Mittag
CC BY-SA 4.0
2023-11-09T22:17:57.847Z
@DrPhil Are you sure that cast doesn't throw? I'd expect a `ClassCastException` or something. (In most type systems, the never type behaves like a universal subclass: you can cast it to anything, but nothing can be cast to it, ever.)
wizzwizz4
CC BY-SA 4.0
2023-11-09T22:21:28.247Z
@wizzwizz4: Indeed: https://scastie.scala-lang.org/JoergWMittag/8njCuMqEQPi4jvWWo5gqjQ But of course, that is a runtime error, not a type error.
Jörg W Mittag
CC BY-SA 4.0
2023-11-09T22:26:15.407Z
`java.lang.ClassCastException: Cannot cast to scala.Nothing` I guessed right! :-)
wizzwizz4
CC BY-SA 4.0
2023-11-10T08:54:30.290Z
You are completely right! Removed my comment to not spread misinformation. :) (My original comment thought that you could trick the compiler with casting, but that just creates an exception at runtime. I tested that the code compiled, but never tested to run it.)
DrPhil
# Are there any situations in which it would make sense to return a never type?
Posted by: username_0 on 2023-11-07
Some languages (Rust is the first one that comes to mind) have a "never" type. This is represented in Rust as `!`, and represents a function that never returns a value (i.e. by throwing an exception or entering an infinite loop). Are there any circumstances in which it would be useful to *return* (presumably an instance of) the "never" type from a function, or is it safe to write syntax such that it can only be used in a type signature?
**Tags:** syntax types never-type
> **Comments:**
> **username_1**: I mean, wouldn't returning a "never" type then be equivalent to exiting/crashing? Otherwise, I can't really see a use for throwing the value around.  
> **username_0**: @Someone Not necessarily; see infinite loops.  
> **username_2**: I'm not 100% sure what you're trying to ask, but Swift's `Never` adopts a lot of protocols like `Error`, `Comparable`, etc -- is that a useful answer? The idea is that `Never` can be used in generic contexts, such as causing a function to return `Result<T, Never>` if you know it can't fail.  
> **username_0**: @Bbrk24 I'm asking if there would ever be a situation in which `return never()` or the like would be useful, or if I'm safe to write my grammar in a way that forbids this.  
> **username_3**: You could have a parametrized function like `<T>(f: () -> T) -> T { return f() }` where the return type is instantiated with `never`. But there's no need to accept a concrete `never` type like in `return never()` (your analysis could simply accept `never()` as the last line of a function which returns anything)  
> **username_4**: @Ginger If you're in a known contradictory situation, like a pattern match branch that is known to be unreachable, then it is ok (and even useful). If it's possible to construct a `never` value in *reachable* situations, however, then you will likely break type safety. This is because, usually, a defining characteristic of an empty type is that you can obtain value of any type you want if you're given a value of an empty type (this is sometimes called "false elimination," "ex falso" or "the principle of explosion").  
> **username_5**: When you talk about a function returning some type, normally we consider the return type as a static declaration, i.e. the type written in the function's declaration. But here you are talking about the "never" type as representing *"a function that never returns a value"*, which is really a runtime property, since it's about the value returned, not just the declared type. If you're asking if it makes sense for a function to *declare* a return type of "never" then the answer is quite different to if it makes sense for a function to return a *value* of type "never". So, please clarify.  
> **username_6**: The question seems to be equally applicable to `void` (as in C and C++), which is also un-inhabited, but I gather that `void` is different from `Never` (in that `void` functions do return control, but `Never` functions don't). ¿Are you asking for both?  
> **username_7**: If by a “never type” you mean the bottom type, it does not make sense to return an actual instance of it because by definition, there *is* no actual instance of it.  
---
## 7 answers
### Answer by username_12 on 2023-11-07. Score: 19
If you have a function `f1()` that returns `Never`,

and you are writing a function `f2()` that also returns `Never`,

and the last thing `f2` does is call `f1`,

then it is conceivable that you write the last statement of `f2` as `return f1()`, therefore returning `Never`.

Note that we are returning the `Never` type, but we are not returning an *instance* of `Never`, because `Never` does not and cannot have any instance.

We are simply proving to the compiler that our function `f2` never returns, and the proof is expressed like this: `f2` doesn't return because `f1` doesn't.
> **Comments:**
> **username_13** (2023-11-10): This pattern is very useful in templated code.  Often one does not know whether f1() returns Never or some other type.  Permitting `return f1()` when f1 returns Never is a syntactic convenience that can earn its keep quite quickly.  This syntax is used in C++  
---
### Answer by username_14 on 2023-11-07. Score: 15
The never type is often an un-inhabited type, i.e., a type that is not inhabited by any value. Therefore, there is no value you could return.
For example, in Scala, I cannot imagine any way to make something like the following compile:
def foo: Nothing = return

This will result in a type error.
You can, of course, return the result of evaluating an expression that has the never type, e.g., something like this:
def foo: Nothing = ???

This compiles because ??? is itself defined like this:
def ??? : Nothing = throw new NotImplementedError

But in the end, you will never return a value, since, no matter how many levels of indirection you chain, there is no value.
> **Comments:**
> **username_15** (2023-11-09): @DrPhil Are you sure that cast doesn't throw? I'd expect a `ClassCastException` or something. (In most type systems, the never type behaves like a universal subclass: you can cast it to anything, but nothing can be cast to it, ever.)  
> **username_14** (2023-11-09): @wizzwizz4: Indeed: https://scastie.scala-lang.org/JoergWMittag/8njCuMqEQPi4jvWWo5gqjQ But of course, that is a runtime error, not a type error.  
> **username_15** (2023-11-09): `java.lang.ClassCastException: Cannot cast to scala.Nothing` I guessed right! :-)  
> **username_16** (2023-11-10): You are completely right! Removed my comment to not spread misinformation. :) (My original comment thought that you could trick the compiler with casting, but that just creates an exception at runtime. I tested that the code compiled, but never tested to run it.)  
---
### Answer by username_8 on 2023-11-08. Score: 7
This would commonly be used in a branching logic to show that a branch should never be reached. For example, in a CASE expression:
function X(value: ABCEnumeration): int
{
  case(value)
  {
    when ABCEnumeration.A: return 1;
    when ABCEnumeration.B: return 2;
    when ABCEnumeration.C: return 3;
    default:               return never;
  }
}

It allows the author to explicitly state that assuming that the input to the function meets the contract for the function (which is particularly relevant for untyped languages such as Python) that there is a branch that could be considered but will never actually be reached.
It also assists static analysis and coverage tools to know that all branches have been considered.
Depending on how your language was written, the syntax could be return never; (if a return statement is expected from each branch of the logic) or using just never; or assert_never(value); (as per python) if the syntax supports not having return statements on some branches.
> **Comments:**
> **username_6** (2023-11-09): `never` could be "an expression of type `Never`" (that doesn't get executed; and akin to a function of type `Never`), to avoid having values of type `Never.  
> **username_9** (2023-11-10): If you could prove at compile-time that the default branch is impossible to reach, then you could just as well allow the developer to omit it in that case.  If you can't prove it, then you need to define the behavior that happens if that branch gets reached regardless. You can't actually return `never`, so you would have to throw a runtime error. So why not make the default branch throw a runtime error in the first place?  
---
### Answer by username_4 on 2023-11-09. Score: 6
"Never types" (also called empty types) are extremely useful in proof assistants. Here's an example in Agda.
What does it look like to "return" a never type in a programming language like Agda? What does it mean and what sort of syntax is used for this? We will see soon!
In short, I will prove that a non-empty list type always has a non-zero length. This proof will be a function that returns a never type. In general, you prove a negation by writing a function that produces the never type. If that function type checks, then you know your proof is correct.
Such a proof can be useful inside actual programs as well (not just proving things to prove things). This is outside the scope of this answer, though.
I'll also set up this answer where if you copy all the code blocks and put them into an Agda file together, it will work.
Here's an outline of what I'm about to do:

Define a type for natural numbers (non-negative integers)
Define a type for "size indexed" non-empty lists. This means the size of the list is "tracked" as a type parameter for the list type. This is somewhat like C++'s std::array (in the sense that the size is a kind of type parameter in both).
To show the basic syntax of Agda, I will write an extract function which will returns the head of the list. This is okay to do because the list always has at least one element.
Because these lists are non-empty, the size will never be zero. I will write a function that proves this by taking a "non-empty list with size zero" and giving back the "never type"

Now to the code. First, an import:
open import Data.Empty

This is just importing the empty type from the standard library. In Agda, this type is called ⊥ and can be pronounced "bottom". It has no constructors. There is no way to make a value of type ⊥ unless we are in a (provably) contradictory situation.
data Nat : Set where
  Z : Nat
  S : Nat → Nat

Our natural number type has two constructors: One for zero (Z) and one for successor (S). The Z constructor doesn't take any arguments. The S constructor takes one argument: a Nat. So, 0 is Z and 3 is S (S (S Z)). This kind of representation is nice for most proof assistant purposes because you can very straightforwardly do induction on it.
Now, the definition of size-indexed non-empty lists:
data NonEmpty (A : Set) : Nat → Set where
  One : A → NonEmpty A (S Z)
  Cons : {n : Nat} → A → NonEmpty A n → NonEmpty A (S n)

You can ignore the As. This is just the "usual" type parameter: That is, the type of elements of the list. NonEmpty has two type parameters: the first is the type of elements and the second is the list size.
We have two cases: the case for lists with exactly one element (One) and the case for a cons-cell (Cons). In the first case, we have exactly one element and our size parameter is S Z (the successor of 0, aka 1). In the second case, we have a head element and a tail list. In the Cons case, the tail list has size n, so the overall list has size S n.
The curly braces means that the n in the Cons case is an implicit parameter. You do not really need to pay attention to that part.
Now, the extract function:
extract : ∀ {A} →
  (n : Nat) →
  NonEmpty A n →
  A
extract n (One x) = x
extract n (Cons x xs) = x

We take in a element type A (again, implicit parameter in curly braces), a natural number n, a non-empty list of size n and we give back something of type A. We handle the two NonEmpty cases using a pattern match. In both cases, we just give back the first element.
Finally, we get to something with the never type!
nonempty-nonzero : ∀ {A} →
  NonEmpty A Z →
  ⊥
nonempty-nonzero ()

Our function takes a non-empty list where the size parameter is Z. This is never possible, since One and Cons both have size parameters that are successors of some natural number. 0 is not the successor of a natural number. We give back ⊥, the never type.
Since we know that the NonEmpty A Z value we were given can never exist (and this follows immediately from the definition of NonEmpty), we write () for the pattern match on our non-empty argument. Note that we didn't even give a function body here, unlike with extract.
() is Agda's syntax for an "absurd pattern match". It will only type check if Agda can immediately see that this pattern match case is impossible. And it does type check here, so Agda does see that this is impossible!
So, we didn't exactly "return" a ⊥ value, at least not using the "usual" syntax to return something. We proved to Agda that we are in an impossible situation, so we didn't have to return anything at all! Which is great, because we cannot build a value of type ⊥. Although, changing subjects slightly, if we happened to already have ⊥ value that we got from somewhere, we could absolutely return it. But that would be a different example.
Further Reading

Programming Language Foundations in Agda: This is a free online book that goes over both the basics of Agda and introduces its use in studying programming languages. The section in Part 1 titled "Negation" is particularly relevant, though the empty type does appear in other places as well.
---
### Answer by username_2 on 2023-11-07. Score: 6
It can be useful to allow expressions of type Never where something else would be expected. For example, the following code is type-safe, but Swift doesn't allow it:
func yeet(_ error: Error) throws -> Never {
  throw error
}

func unwrapOrThrow(_ value: T?) throws -> T {
  return value ?? try yeet(MyError("Expected value"))
}

I had originally tried this to work around the fact that Swift lacks throw-expressions. (It is still possible if you make yeet itself generic, but there's no conceptual reason that making it return Never shouldn't also work.)
---
### Answer by username_10 on 2023-11-09. Score: -1
Some languages have the NaN - like concept that can be used to chain multiple calls:
  value = object.method1(...).method2(...).method3(....);
  if value == std::wrong then ...

If method1 returns something like wrong, further calls do not evaluate at all and the final result is wrong that can be checked. This removes the need to check the success of calling method1, method2 and method3 individually, if the handling is identical regardless which one of them fails. It is not the same as null that would throw null pointer exception if method1 or method2 fails.
And, generally, I think NaN is also that you are talking about. The rationale is that mathematical expression may be very complex, and something like 0 is a likely valid result. If one does not want to work with exceptions, the alternative way is to calculate everything wrong as NaN, and then cascade this assuming that any operator of NaN returns NaN as well. NaN would be safely calculated for the whole expression, regardless where something went wrong.
> **Comments:**
> **username_4** (2023-11-09): NaN is more like the "nothing case" of an optional type (like ML's `NONE` for the `option` type, Haskell's `Nothing` for the `Maybe` type). On the other hand, an *empty type* is a type that literally has no values. It is not possible to *actually* construct a value of an empty type. You can only "construct" a value of such a type when you are in a branch that you know will never be reached. For example, in the body of something like `if (1 == 0) { ... }`. That's a very artificial example, but there are situations where that can actually be very useful. Also, NaN is usually specific to `float`s  
> **username_6** (2023-11-09): Similar to the null object (nil?) in Smalltalk, that accepts every message, mostly returning itself.  
---
### Answer by username_11 on 2023-11-08. Score: -1
I could imagine there being a language where a function that never returns can throw an exception, and the exception handler returning something to the block that contains it.
---
