Crosscut

In addition to the unit type, there's another special type to consider in the type system: a type that has no value, which represents "this can not happen". This is often called the empty type, but I actually prefer the term "never type" (which Rust also uses). It relates more closely to what this type means for the behavior of the program.

Why is it useful, to allow the type system to express that something could never happen? For example, if you have a function that never returns because it calls itself recursively (an endless loop). Saying such a function returns "nothing" would be misleading, because it actually doesn't return. Or not all cases that generic code handles might be possible, given a concrete use of it.

As I write this, I realize there's a lot more to say and explain here. But that might be a better topic for a future series. For now, I just want to relate this concept to the type system that I've presented. And there's something in there, that can represent the never type: The empty variant, variant {}. Because you couldn't actually construct, nor sensibly handle it.