Hcfyk

If a function has return type of ⊥ (bottom type), that means it never returns. It can for example exit or throw, both fairly ordinary situations.

Presumably if a function had a parameter of type ⊥ it could never (safely) be called. Are there ever any reasons for defining such a function?

One of the defining properties of the $bot$ or empty type is that there exists a function $bot to A$ for every type $A$. In fact, there exists a unique such function. It is therefore, fairly reasonable for this function to be provided as part of the standard library. Often it is called something like absurd. (In systems with subtyping, this might be handled simply by having $bot$ be a subtype of every type. Then the implicit conversion is absurd. Another related approach is to define $bot$ as $forall alpha.alpha$ which can simply be instantiated to any type.)

You definitely want to have such a function or an equivalent because it is what allows you to make use of functions that produce $bot$. For example, let's say I'm given a sum type $E+A$. I do a case analysis on it and in the $E$ case I'm going to throw an exception using $mathtt{throw}:Etobot$. In the $A$ case, I'll use $f:Ato B$. Overall, I want a value of type $B$ so I need to do something to turn a $bot$ into a $B$. That's what absurd would let me do.

That said, there's not a whole lot of reason to define your own functions of $botto A$. By definition, they would necessarily be instances of absurd. Still, you might do it if absurd isn't provided by the standard library, or you wanted a type specialized version to assist type checking/inference. You can, however, easily produce functions that will end up instantiated to a type like $botto A$.

Even though there isn't much a reason to write such a function, it should generally still be allowed. One reason is that it simplifies code generation tools/macros.

To add to what has been said about the function absurd: ⊥ -> a I have a concrete example of where this function is actually useful.

Consider the Haskell data-type Free f a which represents a general tree structure with f-shaped nodes and leaves containing as:

data Free f a = Op (f (Free f a)) | Var a

These trees can be folded with the following function:

fold :: Functor f => (a -> b) -> (f b -> b) -> Free f a -> b

fold gen alg (Var x) = gen x

fold gen alg (Op x) = alg (fmap (fold gen alg) x)

Briefly, this operation places alg at the nodes and gen at the leaves.

Now to the point: all recursive datastructures can be represented using a Fixed-point datatype. In Haskell this is Fix f and it can defined as type Fix f = Free f ⊥ (i.e. Trees with f-shaped nodes and no leaves outside of the functor f). Traditionally this structure has a fold as well, called cata:

cata :: Functor f => (f a -> a) -> Fix f -> a

cata alg x = fold absurd alg x

Which gives a quite neat use of absurd: since the tree cannot have any leaves (since ⊥ has no inhabitants other than undefined), it is never possible to use the gen for this fold and absurd illustrates that!

The bottom type is a subtype of every other type, which can be extremely useful in practice. For example, the type of NULL in a theoretical type-safe version of C must be a subtype of every other pointer type, otherwise you couldn't e.g. return NULL where a char* was expected; similarly, the type of undefined in theoretical type-safe JavaScript must be a subtype of every other type in the language.

As a function return type, it's also very useful to have certain functions that never return. In a strongly-typed language with exceptions, for instance, what type should exit() or throw() return? They never return control flow to their caller. And since the bottom type is a subtype of every other type, it's perfectly valid for a function returning Int to instead return $bot$—that is, a function returning Int can also choose not to return at all. (Maybe it calls exit(), or maybe it goes into an infinite loop.) This is good to have, because whether a function ever returns or not is famously undecidable.

Finally, it's very useful for writing constraints. Suppose you want to constrain all parameters on "both sides", providing a type that must be a supertype of the parameter, and another type that must be a subtype. Since bottom is a subtype of every type, you can express "any subtype of S" as $bot prec T prec S$. Or, you can express "any type at all" as $bot prec T prec top$.

There is one use I can think of, and it's something that has been considered as an improvement to the Swift programming language.

Swift has a maybe Monad, spelled Optional<T> or T?. There are many ways to interact with it.

• 
  

  You can use conditional unwrapping like

  
  
  

  if let nonOptional = someOptional {
  
      print(nonOptional)
  
  }
  
  else {
  
      print("someOptional was nil")
  
  }
  
  

  
  



• You can use map, flatMap to transform the values



• The force unwrap operator (!, of type (T?) -> T) to forcefully unwrap the contents, otherwise triggering a crash


• 
  

  The nil-coalescing operator (??, of type (T?, T) -> T) to take its value or otherwise use a default value:

  
  
  

  let someI = Optional(100)
  
  print(someI ?? 123) => 100 // "left operand is non-nil, unwrap it.
  
  
  
  let noneI: Int? = nil
  
  print(noneI ?? 123) // => 123 // left operand is nil, take right operand, acts like a "default" value
  
  

  
  

Unfortunately, there was no concise way of saying "unwrap or throw an error" or "unwrap or crash with a custom error message". Something like

let someI: Int? = Optional(123)

let nonOptionalI: Int = someI ?? fatalError("Expected a non-nil value")

doesn't compile, because fatalError has type () -> Never (() is Void, Swift' unit type, Never is Swift's bottom type). Calling it produces Never, which isn't compatible with the T expected as a right operand of ??.

In an attempt to remedy this, Swift Evolution propsoal SE-0217 - The “Unwrap or Die” operator was put forth. It was ultimately rejected, but it raised interest in making Never be a subtype of all types.

If Never was made to be a subtype of all types, then the previous example will be compilable:

let someI: Int? = Optional(123)

let nonOptionalI: Int = someI ?? fatalError("Expected a non-nil value")

because the call site of ?? has type (T?, Never) -> T, which would be compatible with the (T?, T) -> T signature of ??.

Swift has a type "Never" which seems to be quite like the bottom type: A function declared to return Never can never return, a function with a parameter of type Never can never be called.

This is useful in connection with protocols, where there may be a restriction due to the type system of the language that a class must have a certain function, but with no requirement that this function should ever be called, and no requirement what the argument types would be.

For details you should have a look at the newer posts on the swift-evolution mailing list.