One Div Zero - Getting to the Bottom of Nothing At All

This is an interesting article about programming that basically argues that we can think of not coming back from a function call as a special type that is the sub-type of all other types. That is, if function f promises to return a string, we should really think of this as f promising either to return a string or to get stuck calculating until the end of time or to crash altogether.

Conclusion

I somehow don’t think anybody will be running into the office saying “I just read an article on the bottom type, so now I know how to solve our biggest engineering challenge.” But the bottom type is still interesting. It’s a kind of hole in your static type system that follows inevitably from the Turing Halting Problem. It says that a function can’t promise to compute a string, it can only promise to not compute something that isn’t a string. It might compute nothing at all. And that in turn leads to the conclusion that in a Turing complete language static types don’t classify values (as much as we pretend they do) they classify expressions.

Nothingness is so beautiful because it seeps in through even the strongest of iron doors.