Xjyuk

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 $mathttthrow: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.

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.

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$.