Type Systems: Reachability and Exhaustiveness analysis explained

Please do not link to this article on Reddit or Hacker News.

I thought I’d start writing about some of the different terms that come up in discussions of Flow fairly often as a way to teach the concepts within type systems.

Two things that come up fairly often and frequently go hand in hand are reachability and exhaustiveness.

Reachability

function method(value: "A") {
  if (value === "B") {
    // unreachable
  }
}

In this code example, comparing value against "B" is unnecessary because we’ve stated that value can only ever be an "A”.

The ability for a static type checker to be able tell that the if statement will never be truthy and that the inner block is unreachable is known as reachability analysis.

Exhaustiveness

function method(value: "A" | "B") {
  switch (value) {
    case "A" : // value is A...
    case "B" : // value is B...
    default  : // unreachable
  }
}

In this code example, we’ve handled both the "A" and "B" scenarios, and we know that value can only ever be "A" or "B”, so we know that the default is unnecessary because there is no other possibility.

The ability for a static type checker to be able to tell that all of the possibilities have been exhausted and that the default case is unreachable known as exhaustiveness analysis.

The Flow team is working on both of these features in the type checker. Flow does support some reachability errors but neither of the above examples are going to error today. In future versions of Flow more reachability and exhaustiveness errors will be reported.

Follow James Kyle on twitter. Follow Flow on twitter too.