exhaustiveness.md

id	title
exhaustiveness	Exhaustiveness Checking

Exhaustiveness checking is a feature of a language where the type checker guarantees that the programmer has covered all cases. It can be super useful at catching pesky edge cases before they become bugs, and Sorbet supports it as a first class feature.

tl;dr

If you already know what exhaustiveness checking is, you might just want to see the end result:

# typed: true
extend T::Sig

class A; end
class B; end
class C; end

# (1) Define a type alias as a union type of A, B, or C
AorBorC = T.type_alias {T.any(A, B, C)}

sig {params(x: AorBorC).void}
def foo(x)
  # (2) Use flow-sensitivity to cover each case separately
  case x
  when A
    # To re-iterate: within this branch, Sorbet knows x is an A
    T.reveal_type(x) # Revealed type: `A`
  when B
    T.reveal_type(x) # Revealed type: `B`
  else
    # (3) Use T.absurd to ask Sorbet to error when there are missing cases.
    T.absurd(x) # error: didn't handle case for `C`
  end
end

Otherwise, let's walk through an example explaining not only how we can get exhaustiveness checking, but also why it's useful:

Example

Let's say we have this setup:

# typed: true
extend T::Sig

class A; end
class B; end

sig {params(x: T.any(A, B)).void}
def foo(x)
  # ...
end

There are two classes (A and B), and our method foo takes either A or B.

In the body of foo, we'd like to do something different when given an A versus when given a B:

# ...

def do_a(a); puts 'Got an A!'; end
def do_b(b); puts 'Got a B!'; end

sig {params(x: T.any(A, B)).void}
def foo(x)
  # Problematic! We'll improve this shortly...
  case x
  when A
    do_a(x)
  when B
    do_b(x)
  end
end

There's no bug here yet, but consider that some time in the future, someone wants to update foo to work with class C:

# ...

class C; end
def do_c(c); puts 'Got a C!'; end

# ...

sig {params(x: T.any(A, B, C)).void}
def foo(x)
  # Bug! We forgot to update the body to handle C...
  case x
  when A
    do_a(x)
  when B
    do_b(x)
  end
end

In this case, there's a silent bug in our program. We've updated the signature of foo to accept instances of C, but we haven't updated the method body to actually do something with it!

Exhaustiveness checking is a feature that turns this kind of bug into a type error. It lets us catch the problem statically before causing all sorts of problems down the line.

We can enable exhaustiveness checking in Sorbet using T.absurd(...):

sig {params(x: T.any(A, B, C)).void}
def foo(x)
  case x
  when A
    do_a(x)
  when B
    do_b(x)
  else
    # We're not handling all the cases, so Sorbet will report an error:
    T.absurd(x) # error: didn't handle case for `C`
  end
end

In this case, Sorbet is telling us that by the time we got to the else case, we were missing a case: both B and C needed to be handled, but we were only handling B. T.absurd should be the same variable that the case statement discriminates on.

And as one last tip, we can use Type Aliases to give a name to T.any(A, B, C) and reuse it throughout our codebase. This means we can update the alias in one place, instead of at every individual method!

AorBorC = T.type_alias {T.any(A, B, C)}

sig {params(x: AorBorC).void}
def foo(x)
  # ...
end

Notes

1. Given all the above, it should be clear that exhaustiveness checks are opt-in, i.e., not the default. This is primarily to make it easier to adopt Sorbet in existing projects. That being said, it's still possible that a future version of Sorbet will have exhaustiveness checks enabled by default, with a way to opt out of checking them.

2. T.absurd(...) is implemented both statically and at runtime. Statically Sorbet will report an error, and at runtime Sorbet will raise an exception.

3. Sorbet will error statically if the condition to a case statement using T.absurd is T.untyped. This prevents against losing exhaustiveness checking due to a change in the code that weakens static type information.

4. Exhaustiveness checks are powered by Sorbet's Flow-Sensitive Typing constructs. Specifically, this is also a valid use of T.absurd:

   # Will error if `x` ever becomes nilable or untyped due to a refactoring
   T.absurd(x) if x.nil?

What's next?

• Flow-Sensitive Typing

  Sorbet implements a control flow-sensitive type system, which means it tracks the flow of control through a program and narrows or widens the types of variables in response. Flow-sensitive typing is the feature that ultimately powers exhaustiveness.

• Sealed Classes and Modules

  The form of exhaustiveness checking seen here relied on simultaneously updating a type alias when adding a new case to consider. An alternative to this is to use sealed classes, which effectively make exhaustiveness a property of the definition not the usage site.

• Abstract Classes and Interfaces

  The form of exhaustiveness we've seen here is structural—Sorbet checks that each case of a particular structure have been handled. An alternative is to describe an abstract method (i.e., behavior) and require that all subclasses implement that method (a form of "behavioral exhaustiveness"). This doc describes how to use Sorbet's abstract classes and methods to enforce those guarantees.