Advance Flow type #1: Exhaustive checking with empty type

Photo by Peter Lewicki on Unsplash

Advance Flow type: Table of Contents

This post is the first post in Advance Flow type series and might be the least advance one but I think it is quite useful.

From the title, there are two interesting terms: exhaustive checking and empty type. What are they? Why do I need to care?

Exhaustive Checking

When we do conditional branching like if else or switch you might end up leaving some branch unhandled. Consider this simple function:

const f = (x: 'A' | 'B') => {
  if (x === 'A') {
    return 0
  }
}

Flow will not complain you anything, even though the 'B' case is not handled. The return type will be infered to ?number since it implicitly return undefined.

We can add else block to handle the rest of the case like this

const f = (x: 'A' | 'B'): number => {
  if (x === 'A') {
    return 0
  } else {
    return 1
  }
}

I also specify number as return type of this function to make sure that it will never implicitly return undefined.

Moving forward, we need to extract type of x out to somewhere else like this.

// type.js
type X = 'A' | 'B'

And the function lives in another file.

// function.js
const f = (x: X): number => {
  if (x === 'A') {
    return 0
  } else {
    return 1
  }
}

Now, let’s assume that type X is being used by someone else as well. If one day we have to add 'C’ to the type.

type X = 'A' | 'B' | 'C'

You have to go back and find every branching on X to make sure that it handle 'C' correctly and not just fall into default case which is not expected behavior.

What if I told you that if we just add two more line of code and you can prevent this problem? What if when we add 'C' our beloved type system will just guide us back to where we need to care about rather than tracing back yourself?

Or to put it in another way, to exhaustively check if we have already handled every cases.

Empty Type

In order to do that in Flow, you need empty type.

What is empty type?

Empty type is the type that has no element at all. So if we assert (x: empty)

const f = (x: X): number => {
  if (x === 'A') {
    return 0
  } else if (x === 'B') {
    return 1
  } else {
    (x: empty)
    throw new Error(`${x} is not an element of type 'X'`)
  }
}

It will have type error since x is so far refined to 'C' which means it still not empty. So all you need to do is to add another case to handle 'C' and Flow will be happy.

const f = (x: X): number => {
  if (x === 'A') {
    return 0
  } else if (x === 'B') {
    return 1
  } else if (x === 'C') {
    return 2
  } else {
    (x: empty)
    throw new Error(`${x} is not an element of type X`)
  }
}

If you don’t throw you will have a problem of implicitly return undefined. Apart from avoiding the implicitly return undefined problem, it is also useful for the case that some part of the code is still not covered by Flow or the data comes from IO boundary (eg. API calls) and, for some reason, doesn’t match the type definition (which I would suggest validating it beforehand using something like io-ts).

I would recommend using throw so when such a case happens, it’s not failed silently.

But there is another way to avoid implicitly return undefined just to show you an interesting property of empty type.

Which is by returning emptiness.

const f = (x: X): number => {
  if (x === 'A') {
    return 0
  } else if (x === 'B') {
    return 1
  } else if (x === 'C') {
    return 2
  } else {
    return (x: empty)
  }
}

After x being refined to this point, its type is no longer anything. It will work without explicitly asserting that x is empty as well, but the error will be a little bit more confusing since it will check type of x against number instead of empty. So, by returning x, the return type of this function will be

number | empty

since it could be either number or empty.

But for any type T, T | empty = T and empty | T = T because empty has no element, that’s why if we handle all the case before that last return, there should be no type error.

And you might notice that it’s the same as logic, for all proposition p, we can say that p v False = p and False v p = p and it’s not just a coincidence because empty type is corresponded to falsity and type also has strong correspondence to logic.

If you would like to go down the rabbit hole, you can have a look at Bottom type and Curry-Howard correspondance.

More example

Let’s look at more practical example.

We are going to create a validator that consume rule as data and spit out the result and here is the shape of rules.

type MaxRule = {
  type: 'MAX',
  maxValue: number,
}
type MinRule = {
  type: 'MIN',
  minValue: number,
}
type ForAllRule = {
  type: 'FOR_ALL',
  rules: Rule[]
}
type ForSomeRule = {
  type: 'FOR_SOME',
  rules: Rule[]
}
type Rule = MinRule | MaxRule | ForAllRule | ForSomeRule

Every rule has property type so we can refine the type using that property.

const validate = (value: number, rule: Rule): boolean => {
  switch (rule.type) {
    case 'MAX':
      return value <= rule.maxValue
    case 'MIN':
      return value >= rule.minValue
    case 'FOR_ALL':
      return rule.rules
        .reduce((acc, nextRule) => acc && validate(value, nextRule), true)
    case 'FOR_SOME':
      return rule.rules
        .reduce((acc, nextRule) => acc || validate(value, nextRule), false)
    default:
      (rule.type: empty)
      throw Error(`rule ${rule.type} is not being handled properly`)
  }
}

So now if we remove some case then it should have a type error.

Conclusion

Even though exhaustive checking with Flow might not be so beautiful comparing to some other language that has native support for it (eg. Scala, Haskell, Elm, OCaml) but at least we can make it work in JavaScript and it help us being explicit about what should be handled and let type system guide us where to fix or add stuffs.

For empty type itself, it also has some other use cases which we will discuss about it later in this series.

Thank you for reading. Feedback and comment are welcome.

Follow me on twitter @ibossptk