Type Driven Development: Exhaustiveness Checking

Part 13 – Exhaustiveness Checking

This is a series of posts I’m writing about using types as another tool in software development, Continuous Delivery, & keeping LLM’s honest. They’re also a design & refactoring tool, a communication tool, and reduce how many tests you have to write.

Parts

1. Part 1 – Branded Types
2. Part 2 – Product Types
3. Part 3 – Union & Discriminated Unions
4. Part 4 – Non-Empty Collections
5. Part 5 – Indexed Types
6. Part 6 – unknown vs any
7. Part 7 – Result
8. Part 8 – Schema
9. Part 9 – Total Function
10. Part 10 – Errors as Values
11. Part 11 – Property Tests
12. Part 12 – Type Proofs
13. Part 13 – Exhaustiveness Checking
14. Part 14 – Parse, Don’t Validate
15. Part 15 – Anti-Corruption Layer
16. Part 16 – Opaque Types
17. Part 17 – Maybe
18. Part 18 – Smart Constructors
19. Part 19 – Pipeline
20. Part 20 – Railway Oriented Programming
21. Part 21 – Typestate
22. Part 22 – Capabilities
23. Part 23 – Immutability
24. Part 24 – Making Impossible States Impossible
25. Part 25 – Type Driven Development: How to do it
26. Part 26 – Final Thoughts

Enums, Unions, & Discriminated Unions enable Exhaustiveness Checking; all variants are handled.

This means if a DU has 3 possibilities:

type State = 'loading' | 'success' | 'error'Code language: JavaScript (javascript)

All 3 must be handled, else the code won’t compile:

switch(state) {
  case 'loading': ...
  case 'success': ...
  // ❌ forgot error, won't compileCode language: PHP (php)

This has numerous benefits. You completely avoid impossible situations:

switch(state) {
  case 'loading': ...
  case 'success': ...
  case 'error': ...
  default:
    return "shouldn't happen"Code language: PHP (php)

You don’t need default; there is only 3 states, default can never happen. In JavaScript, you’d end up in weird states when state was typed as a string and you misspelled “Success” with a capital S. Worse, you’d get undefined somewhere else, completely far from where the bug was caused.

You learn you need to add a cancel button from your Designer, so you can now confidently add a cancel state:

type State = ... | 'cancelled'Code language: JavaScript (javascript)

And the compiler will tell you all the places to update; powerful refactoring tool. Types have a knack for high coupling, and this is a situation where that coupling can help.

You completely negate fall through bugs, such as React components:

function render(state) {
  if(state == 'loading') { return <Loading />
  if(state == 'success') { return <Success />
  return "shouldn't happen"Code language: JavaScript (javascript)

If later you add “unauthorized”, in JavaScript, you’ll see “shouldn’t happen”. in TypeScript w/DU’s, that can’t ever happen.

Type narrowing is built-in, meaning you can only access data on the DU variant when correct, again making “Impossible Situations, Impossible” (e.g. accidentally using data in the Err state, and error in the Success state):

type State
  = { tag: 'loading' }
  | { tag: 'err', error: string }
  | { tag: 'success', data: Array<string> }

switch(state.tag) {
  case 'loading': ...
  case 'success':
    // ❌ fails to compile, error is on err, not success
    return <Error error={state.error} />
  case 'err':
    // ❌ fails to compile, data is on success, not err
    return <Success data={state.data} />Code language: JavaScript (javascript)

Caveat: Functional Programming languages call this switch “pattern matching”, and Discriminated Unions are MUCH easier to write & read in those languages. Plus they have equality checking built-in (e.g. ok(1) == ok(1) would be true vs. instance / memory pointer checking saying it’s false). Pattern matching has much richer querying functionality in the cases as well. So Discriminated Unions are particularly awkward to write & learn in TypeScript both having to manually create a tag and constructor functions/Opaque types, but _worth it_ for Exhaustiveness Checking’ benefits.