patternModerate
Is there any use case for the bottom type as a function parameter type?
Viewed 0 times
casetheanyfunctionbottomtypeforthereparameteruse
Problem
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?
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?
Solution
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
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}:E\to\bot$. In the $A$ case, I'll use $f:A\to 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
That said, there's not a whole lot of reason to define your own functions of $\bot\to A$. By definition, they would necessarily be instances of
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.
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}:E\to\bot$. In the $A$ case, I'll use $f:A\to 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 $\bot\to 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 $\bot\to 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.
Context
StackExchange Computer Science Q#109897, answer score: 17
Revisions (0)
No revisions yet.