| What is “reasonable”? Suppose we take your argument to its logical conclusion—a type system ought to be able to statically detect any property we desire. In general, this would amount to predicting exactly which value each variable contains at each point during the program’s execution. This is obviously not tractable. Statically tracking information has a cost. As the article describes, tracking certain properties can require changing the way information is represented and manipulated, sometimes in ways that are meaningfully less pleasant. Static tracking can provide a lot of benefits, so often the tradeoff is worth it, and we choose to play the typechecker’s game, but we are selective about which properties we track because it’s easier to not track something if we don’t need to. One thing that the blog post doesn’t really call out explicitly enough is that the information you track in the type system ought to be driven by what your application actually needs. The goal is to eliminate the need to write things like throw new Error("this should never happen")
as much as possible. Null pointer dereferences, divisions by zero, and attempts to add a number to a string are all examples of this kind of situation. Fundamentally, the program needs to produce a value to continue—the expression has to evaluate to something—but there isn’t any way to get any reasonable output from the given inputs. The only option is to crash.Strengthening the types allows us to avoid these kinds of situations. For example, suppose we write a function that takes a list of source spans in a file and returns a single source span that covers all of them, and we realize “wait, what do I return if I’m given no source spans?” There’s no reasonable value to return. So you can strengthen the type to accept only non-empty lists, then follow the type errors up the call chain until you find a place where you can report a reasonable error to the user if no values are provided (or avoid the error from ever happening in the first place). But it’s not helpful to strengthen the types to track properties we don’t actually care about. For example, in theory, we could give our “combine source spans” function a really precise type that guarantees that the resulting source span’s starting location is always equal to the starting location of the earliest source span in the input list. That property ought to always be true. But proving it to the type system would be more complicated, and it wouldn’t actually get us anything: we wouldn’t avoid any “this should never happen” cases by doing that work. (Of course, if that changed, and we would, then we might go back and figure out how to strengthen the types.) Type systems can continue to grow more sophisticated, able to capture increasingly many properties with less effort from the programmer, and that’s great! But they won’t ever be able to magically detect everything automatically. And that’s really what this blog post is all about: in the situations where you find you’re writing a function that can’t handle a particular case, and the type system doesn’t have any native support for ruling it out, you might be able to rearrange your data representation so that the case can’t be represented and therefore doesn’t need to be handled. Most applications don’t take a lot of square roots, so most applications aren’t negatively impacted by coarse-grained typing of the square root function. Some type systems make different choices—Typed Racket, for example, puts a lot of effort into fine-grained typing just like you describe[1]—but those choices can impact other parts of the type system, sometimes in negative ways. (Subtyping, for example, makes some other extensions to the type system much, much harder.) So static typing is fundamentally about tradeoffs, and sadly, there are no silver bullets. There won’t ever be one “best” type system (though I think we can still argue that some are better than others). [1]: https://www2.ccs.neu.edu/racket/pubs/padl12-stff.pdf |