← back

Refinement Types

5 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.

type type T = numberT = number;

let let isEven: (x: T) => booleanisEven = (x: numberx: type T = numberT): boolean => {
  return x: numberx % 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:

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.
type 
type Even = number & {
    _brand: "Even";
}
Even = number & { _brand: "Even"_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.

const const evenNumber: EvenevenNumber: 
type Even = number & {
    _brand: "Even";
}
Even = 3 as 
type Even = number & {
    _brand: "Even";
}
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.


const const anyNumber: numberanyNumber: number = 4;
let let evenNumber: EvenevenNumber: 
type Even = number & {
    _brand: "Even";
}
Even;
if (let isEven: (x: T) => booleanisEven(const anyNumber: numberanyNumber)) evenNumber = const anyNumber: numberanyNumber; // oops
Type '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.

function function isEven(x: number): x is EvenisEven(x: numberx: number): x: numberx is 
type Even = number & {
    _brand: "Even";
}
Even {
  return x: numberx % 2 === 0;
}

Now our predicate will narrow the type of its argument.


if (function isEven(x: number): x is EvenisEven(const anyNumber: numberanyNumber)) let evenNumber: EvenevenNumber = const anyNumber: EvenanyNumber;

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.


function function parseEven(x: number): Even | nullparseEven(x: numberx: number): 
type Even = number & {
    _brand: "Even";
}
Even | null {
  return let isEven: (x: number) => booleanisEven(x: numberx) ? (x: numberx as 
type Even = number & {
    _brand: "Even";
}
Even) : null;
}

function function Even(x: number): EvenEven(x: numberx: number) {
  if (let isEven: (x: number) => booleanisEven(x: numberx)) {
    return x: numberx as 
type Even = number & {
    _brand: "Even";
}
Even;
  } else {
    throw new 
var Error: ErrorConstructor
new (message?: string | undefined, options?: ErrorOptions | undefined) => Error (+1 overload)
Error(`${x: numberx} is not even`);
  }
}

const const evenNumber: EvenevenNumber: 
type Even = number & {
    _brand: "Even";
}
Even = function Even(x: number): EvenEven(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: