← back

Refinement Types

4 min read ·

What are they?

TLDR: type + predicate = refinement type

We have a type called T and a predicate on T called P.

Even numbers are a nice example. Our T is number, our P is isEven.

tsx
type T = number;
 
let isEven = (x: T): boolean => {
  return x % 2 === 0;
}
 
tsx
type T = number;
 
let isEven = (x: T): boolean => {
  return x % 2 === 0;
}
 

We can say that P refines T into a type PT, where PT is a subtype of T containing all values x of type T for which P(x) === true.

Our PT is made from the type number and refined with the predicate isEven:

tsx
type Even = 0 | 2 | 4 | 6 | 8 | //...
tsx
type Even = 0 | 2 | 4 | 6 | 8 | //...

Problem is, we can’t just list out all the even numbers, and even if we could have an infinite type that would work in this case, our complex business domains often deal with types we cannot represent in the typesystem, like AuthorizedUser.

We have some understanding of refinement types, maybe we’ve even skimmed the Wikipedia article…

In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type.

Wikipedia, “Refinement type”

But it doesn’t seem very practical yet, right? Let’s get leave the theory for a bit, and implement the missing pieces.

How can I use them?

There are a few ways we can go about it. Pick your poison.

  1. Full OOP, make a new class Even and extend a Number.
  2. In cases like AuthorizedUser or ValidEmail, we may not even need a subtype of the original type, so we can wrap it in a value object. It’s just important that the refinement type isn’t assignable to the original type, because want the validation to happen.
  3. My favorite — use nominal typing and leave no runtime trail.
tsx
type Even = number & { _brand: "Even" };
tsx
type Even = number & { _brand: "Even" };

Now Even is a number with a big “Even” string sprayed on it. We’ll never assign anything to the _brand property. It exists only on the type level.

tsx
const evenNumber: Even = 3 as Even;
tsx
const evenNumber: Even = 3 as Even;

If we use a type assertion, we can pretend 3 is an even number, but we won’t be doing it. Ensuring that the name means something is up to our predicate function.

tsx
const anyNumber: number = 4;
let evenNumber: Even;
if (isEven(anyNumber)) evenNumber = anyNumber; // oops
Type 'number' is not assignable to type 'Even'.
  Type 'number' is not assignable to type '{ _brand: "Even"; }'.2322Type 'number' is not assignable to type 'Even'.
  Type 'number' is not assignable to type '{ _brand: "Even"; }'.
tsx
const anyNumber: number = 4;
let evenNumber: Even;
if (isEven(anyNumber)) evenNumber = anyNumber; // oops
Type 'number' is not assignable to type 'Even'.
  Type 'number' is not assignable to type '{ _brand: "Even"; }'.2322Type 'number' is not assignable to type 'Even'.
  Type 'number' is not assignable to type '{ _brand: "Even"; }'.

Any number isn’t assignable to our special branded type, and that’s what we wanted. However, we didn’t let TypeScript know that isEven and Even are connected.

We’ll use user defined type guards to tell the compiler that our predicate checks the type. It’s exactly what we need in this case.

Let’s empower our isEven predicate by changing its return type.

tsx
function isEven(x: number): x is Even {
  return x % 2 === 0;
}
tsx
function isEven(x: number): x is Even {
  return x % 2 === 0;
}

Now our predicate will narrow the type of its argument.

tsx
if (isEven(anyNumber)) evenNumber = anyNumber;
tsx
if (isEven(anyNumber)) evenNumber = anyNumber;

We can call the predicate once and if returns true, we remember this fact in the type system to avoid accidental errors.

In languages without type guards, we can create a constructor function.

tsx
function parseEven(x: number): Even | null {
  return isEven(x) ? (x as Even) : null;
}
 
function Even(x: number) {
  if (isEven(x)) {
    return x as Even;
  } else {
    throw new Error(`${x} is not even`);
  }
}
 
const evenNumber: Even = Even(4);
tsx
function parseEven(x: number): Even | null {
  return isEven(x) ? (x as Even) : null;
}
 
function Even(x: number) {
  if (isEven(x)) {
    return x as Even;
  } else {
    throw new Error(`${x} is not even`);
  }
}
 
const evenNumber: Even = Even(4);

Takeaways

Further reading

This is mostly a reading list for future me, but I hope you can also find it interesting.

Past Meetup Talks

I gave two short talks on refinement types in the past.

Pitch: I’m gonna explain what refinement types are, geek out about a research paper that adds them to the TypeScript type system, and live-code a userland refinement type you can already use in your codebase.

Outline: