Type Systems: Refinements explained

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

Refinements are a frequently used aspect of any type system. They are so ingrained in the way that we program and even the way that we think you might not even notice them.

In the code below, value can either be “A” or “B” and an if statement

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

Inside of the if block we know that value must be “A” because that’s the only time the if-statement will be truthy.

The ability for a static type checker to be able to tell that the value inside the if statement must be “A” is known as a refinement.

Next we’ll add an else block to our if statement.

function method(value: "A" | "B") {
  if (value === "A") {
    // value is "A"
  } else {
    // value is "B"
  }
}

Inside of the else block we know that value must be “B” because it can only be “A” or “B” and we’ve removed “A” from the possibilities.

Refinements also includes the ability for a static type checker to be able to eliminate options from a group as they are refined away.

You can expand this infinitely:

function method(value: "A" | "B" | "C" | "D") {
  if (value === "A") {
    // value is "A"
  } else if (value === "B") {
    // value is "B"
  } else if (value === "C") {
    // value is "C"
  } else {
    // value is "D"
  }
}

Refinements can also come in other forms other than testing for equality:

function method(value: boolean | Array<string> | Event) {
  if (typeof value === "boolean") {
    // value is a boolean
  } else if (Array.isArray(value)) {
    // value is an Array
  } else if (value instanceof Event) {
    // value is an Event
  }
}

Or you could refine on the shape of objects

type A = { type: "A" };
type B = { type: "B" };
function method(value: A | B) {
  if (value.type === "A") {
    // value is A
  } else {
    // value is B
  }
}

It is also possible to invalidate refinements, for example:

type A = { type: "A" };
type B = { type: "B" };
function method(value: A | B) {
  if (value.type === "A") {
    // value is A
    otherMethod();
    // value is A | B
  }
}

The reason for this is that we don’t know that otherMethod() hasn’t done something to our value. Imagine:

var value = { type: "A" };
function otherMethod() {
  value.type = "B";
}
function method(value: A | B) {
  if (value.type === "A") {
    // value is A
    otherMethod();
    // value has become a B
  }
}
method(value);

Not all type systems that support refinements will recognize this and will optimistically assume that the value has not changed (i.e. TypeScript), other languages might not allow this sort of mutation at all so their type systems don’t need to be concerned with it (i.e. Reason).

Flow supports refinements as well as refinement invalidations in order to make JavaScript type safe. Check it out in the documentation.

Next see how refinements are used for reachability and exhaustiveness analysis.

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