3 ms·
Could you please explain the difference between f: X -> void and f: X -> Bottom? If there was a void type in C, would void be Bottom?
by eithed 6y ago
Could you please explain the difference between f: X -> void and f: X -> Bottom? If there was a void type in C, would void be Bottom?
- masklinn 6y agoConceptually, void is a singleton type: it has one value. So a function which returns void does return, just without anything useful. Bottom has no value, so a function which “returns” bottom can not terminate. Practically, this means it either loops forever or “breaks” e.g. panics or exits the program.
- contravariant 6y agoNo the Bottom type has no values, while the void type has exactly 1 (which doesn't have a name, but you can return it by writing `return;`). So a function f: X -> void returns the only (nameless) value in void, depending on the programming language it will return null or equivalent or it'll just return no data (but it'll still return). A function f: X -> Bottom is different, the type Bottom has no values so it is impossible for the function to ever return. This is not always useful, but in some strongly typed you need it to assign a value to an infinite loop.
- eithed 6y agoOh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood. Thanks for the explanation!
- masklinn 6y ago> Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood. The second function terminates, same as the first one, there's no real difference between them. A bottom-returning function would be something like function foo() { for(;;) {} } that genuinely never terminates and thus never exits.