Refinement Types
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
typeT = number;letisEven = (x :T ): boolean => {returnx % 2 === 0;}
tsx
typeT = number;letisEven = (x :T ): boolean => {returnx % 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…
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.
 Full OOP, make a new class
Even
and extend aNumber
.  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.
 My favorite — use nominal typing and leave no runtime trail.
tsx
typeEven = number & {_brand : "Even" };
tsx
typeEven = 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
constevenNumber :Even = 3 asEven ;
tsx
constevenNumber :Even = 3 asEven ;
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
constanyNumber : number = 4;letevenNumber :Even ;if (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"; }'.isEven (anyNumber ))= evenNumber anyNumber ; // oops
tsx
constanyNumber : number = 4;letevenNumber :Even ;if (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"; }'.isEven (anyNumber ))= evenNumber anyNumber ; // oops
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
functionisEven (x : number):x isEven {returnx % 2 === 0;}
tsx
functionisEven (x : number):x isEven {returnx % 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
functionparseEven (x : number):Even  null {returnisEven (x ) ? (x asEven ) : null;}functionEven (x : number) {if (isEven (x )) {returnx asEven ;} else {throw newError (`${x } is not even`);}}constevenNumber :Even =Even (4);
tsx
functionparseEven (x : number):Even  null {returnisEven (x ) ? (x asEven ) : null;}functionEven (x : number) {if (isEven (x )) {returnx asEven ;} else {throw newError (`${x } is not even`);}}constevenNumber :Even =Even (4);
Takeaways
 Refinements are not implemented in TypeScript, but you can make them in userspace.
 You can use nominal typing to make sure your refinements have no runtime trail (except predicate checks).
 You can use them to encode facts about your data in the type system.
Further reading
This is mostly a reading list for future me, but I hope you can also find it interesting.

refined for Scala sounds really interesting and with ScalaJs I could target the same platforms as TypeScript.

“A taste of dependent types” by Keegan McAllister

“Refinement Types for TypeScript”
A basic refinement type is a basic type, e.g. number, refined with a logical formula from an SMT decidable logic.
For example, the types:type nat = { v: number  0 ≤ v }type pos = { v: number  0 < v }type natN<n> = { v: nat  v = n }type idx<a> = { v: nat  v < len(a) }type nat = { v: number  0 ≤ v }type pos = { v: number  0 < v }type natN<n> = { v: nat  v = n }type idx<a> = { v: nat  v < len(a) }describe (the set of values corresponding to) nonnegative numbers, positive numbers, numbers equal to some value n, and valid indexes for an array a, respectively…
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 livecode a userland refinement type you can already use in your codebase.

How? Lightning talk with VSCode, Quokka and browser as software.

What? Refinement types are easy. Use them to encode more info on the type level.

Why? Encoding information on the type level helps you write less bugs.
Outline:
 Why and when should I type stronger?
 JS without JSDoc vs Idris proofs
 Refinement types are one step further into bulletproof programs.
 Refined TypeScript
 It’s not rocket science
 You can do it yourself
 Live demo
 Libraries with refinements