# Refinement Types

## What are they?

_TLDR: type + predicate = refinement type_

We have a type called _**T**_ and a
[predicate](<https://en.wikipedia.org/wiki/Predicate_(mathematical_logic)>) on
_**T**_ called _**P**_.

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

```tsx twoslash include brand
type Even = number & { _brand: "Even" };
```

```tsx twoslash include def
type T = number;

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

// - 1

type Even = number & { _brand: "Even" };
```

```tsx twoslash
// @include: def-1
```

<style>{`.zaduma-prose pre { padding-top: 0; padding-bottom: 0;}`}</style>

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`:

{/* prettier-ignore */}
```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...

<figure>

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

<figcaption>

<div class="p-1" />

[Wikipedia, "Refinement type"](https://en.wikipedia.org/wiki/Refinement_type)

</figcaption>
</figure>

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.

[value object]: https://en.wikipedia.org/wiki/Value_object
[nominal]:
  https://michalzalecki.com/nominal-typing-in-typescript/#approach-4-intersection-types-and-brands
[typing]: https://github.com/hasparus/nom-ts

```tsx twoslash
// @include: brand
```

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 twoslash
// @include: brand
// ---cut---
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 twoslash
//
// @include: def
// ---cut---

const anyNumber: number = 4;
let evenNumber: Even;
// @errors: 2322
if (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](https://www.typescriptlang.org/docs/handbook/advanced-types.html#using-type-predicates)
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 twoslash include new-def
// @errors: 2552
function isEven(x: number): x is Even {
  return x % 2 === 0;
}
```

```tsx twoslash
// @include: brand
// ---cut---
// @include: new-def
```

Now our predicate will narrow the type of its argument.

```tsx twoslash
// @include: brand
// @include: new-def
const anyNumber: number = 4;
let evenNumber: Even;
// ---cut---

// @errors: 2322
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 twoslash
// @include: def
// ---cut---

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

- 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](https://github.com/fthomas/refined) for Scala sounds really
  interesting and with [ScalaJs](https://www.scala-js.org/) I could target the
  same platforms as TypeScript.

- "[A taste of dependent types](http://kmcallister.github.io/talks/rust/2015-dependent-types/slides.html)"
  by Keegan McAllister

- "[Refinement Types for TypeScript](https://goto.ucsd.edu/~pvekris/docs/pldi16.pdf)"

  > 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) }
  > ```
  >
  > describe (the set of values corresponding to) non-negative 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.

- [WrocTypeScript Sept 2019](https://www.meetup.com/WrocTypeScript/events/sjzhvqyzmbhc/),
  [slides](https://github.com/hasparus/refinement-types-in-typescript),
  [notes](https://paper.dropbox.com/doc/Refinement-Types-in-TypeScript--AtRTxIb1NxWvFpBv3oxBx9jpAg-cZxqOn3c6GkVCONvPTjtE)

- [Kraków TUG Feb 2022](https://www.meetup.com/typescript-krakow/events/266226393/),
  [slides](https://github.com/hasparus/refinement-types-in-typescript/tree/extended-15-minutes),
  (bad) [video](https://youtu.be/4ccCeAbwmbU)

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

- **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