13
$\begingroup$

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?

$\endgroup$
9
  • 1
    $\begingroup$ 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. $\endgroup$
    – Someone
    Commented Nov 7, 2023 at 14:15
  • 1
    $\begingroup$ @Someone Not necessarily; see infinite loops. $\endgroup$
    – Ginger
    Commented Nov 7, 2023 at 14:22
  • 1
    $\begingroup$ 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. $\endgroup$
    – Bbrk24
    Commented Nov 7, 2023 at 15:24
  • $\begingroup$ @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. $\endgroup$
    – Ginger
    Commented Nov 7, 2023 at 15:25
  • 2
    $\begingroup$ @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"). $\endgroup$ Commented Nov 7, 2023 at 17:24

7 Answers 7

19
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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++ $\endgroup$
    – Cort Ammon
    Commented Nov 10, 2023 at 0:43
15
$\begingroup$

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.

$\endgroup$
4
  • 2
    $\begingroup$ @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.) $\endgroup$
    – wizzwizz4
    Commented Nov 9, 2023 at 22:17
  • 2
    $\begingroup$ @wizzwizz4: Indeed: scastie.scala-lang.org/JoergWMittag/8njCuMqEQPi4jvWWo5gqjQ But of course, that is a runtime error, not a type error. $\endgroup$ Commented Nov 9, 2023 at 22:21
  • 1
    $\begingroup$ java.lang.ClassCastException: Cannot cast to scala.Nothing I guessed right! :-) $\endgroup$
    – wizzwizz4
    Commented Nov 9, 2023 at 22:26
  • $\begingroup$ 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.) $\endgroup$
    – DrPhil
    Commented Nov 10, 2023 at 8:54
7
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ 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. $\endgroup$
    – Pablo H
    Commented Nov 9, 2023 at 17:49
  • $\begingroup$ 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? $\endgroup$
    – Philipp
    Commented Nov 10, 2023 at 14:38
6
$\begingroup$

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<T>(_ 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.)

$\endgroup$
6
$\begingroup$

"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.
$\endgroup$
-1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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 floats $\endgroup$ Commented Nov 9, 2023 at 16:35
  • $\begingroup$ Similar to the null object (nil?) in Smalltalk, that accepts every message, mostly returning itself. $\endgroup$
    – Pablo H
    Commented Nov 9, 2023 at 17:46
-1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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