Type Level Tricks in TypeScript

Introduction

TypeScript has a Turing complete type system . This means there are all sorts of compile time invariants that we can enforce with the type system that we couldn't otherwise. I haven't seen some of these patterns explicitly outlined elsewhere so I'm going to outline one trick that I've discovered while trying to encode various properties with TypeScript's type system.

Equality

The most useful trick, in my opinion, is testing equality between two types so I'm going to explain it first

type Eq<A, B> = [A] extends [B] ? ([B] extends [A] ? true : never) : never;

When I first wrote this it reminded me of set equality but structural types are slightly more complicated than sets so it's just a useful analogy. Things get tricky when recursive types are involved and I didn't pursue the analogy to its logical conclusion.

So what is going on in the above type? The easiest way to make sense of it is probably to substitute some concrete types. I'm going to use some literal types like numbers and strings but more complicated types will also work (assuming there are no bugs in the compiler when it comes to checking [A] extends [B] ).

If you're following along then I recommend trying things out in the TypeScript playground so that you can see the compiler errors and warnings.

Let's substitute some types and verify that things are working as we expect

type NumEq = Eq<1, 1>;
type NumNotEq = Eq<1, 2>;

If you mentally perform the substitutions then the above declarations are equivalent to

type NumEq = true;
type NumNotEq = never;

There are no values for the type true other than the literal value true and never is a type that indicates divergence

const neverValue: never = (() => { throw 'Error'; })();

If we try to use these types incorrectly then the compiler will yell at us

// These are fine
let numEq1: NumEq = true;
let numNotEq1: NumNotEq = neverValue;

// These are not fine
let numEq2: NumEq = false;
let numNotEq2: NumNotEq = null;

It is kinda annoying to pepper the code with assignments to verify that type equalities are actually equalities. The way to get around this is to use a function with an empty body and a single argument

function isTrue<T extends true>(t: T) { }

Now using this function we can enforce compile time restrictions by calling the function instead of assigning values

// These are fine
isTrue<Eq<1, 1>>(true);
isTrue<Eq<2, 2>>(true);

// These are not fine
isTrue<Eq<1, 2>>(true);
isTrue<Eq<2, 3>>(true);

Here's an example of how I've used Eq and isTrue in a small workflow library

// ...
// Now specify all the invariants that the messages must satisfy
{
  // Dispatcher messages must implement all the message types
  isTrue<Eq<DispatcherMessage["type"], MessageType>>(true);
  // Client mapping must represent every message type
  isTrue<Eq<keyof ClientMapping, MessageType>>(true);
  // Client mapping keys and types must actually match so we don't accidentally map 'work' to 'done'
  isTrue<KeyTypeEq<ClientMapping>>(true);
}
// ...

Whenever you have types that must match up in some non-trivial ways then you can use Eq and isTrue to enforce those constraints by making sure some types are equal to other types.

Conclusion

There are a few more tricks that I have come across but this is probably the most important one when it comes to the amount of leverage it provides for enforcing various consistency properties with the TypeScript compiler.

If you know of other tricks then let me know. I'm pretty sure there is a way to encode a Prolog interpreter with TypeScript's type system but it sounds like a daunting task so I haven't tried it. If you know how to do it then let me know.