# Mathias Jean Johansen

# Type-Level Programming in TypeScript

The TypeScript type system is immensely powerful, and while the language itself is, of course, Turing complete, so is the type system itself. This allows us to implement types that are far more sophisticated than what is possible in most popular programming languages, as we can do computations on a type-level which is, essentially, what characterizes type-level programming.

In the following, I will demonstrate how we can utilize features of the TypeScript type system such as conditional types, indexed array types, and more to implement a type that computes a given Fibonacci number.

It should be pointed out that while it is possible to implement this, you should consider it merely an academic exercise and not a recommendation for how to use the type system in your production applications.

Before we can implement anything, we need to have a notion of what a number is. In type-level programming, this is most commonly modeled using Peano numbers. We can define our Peano numbers in the following manner:

```
type Zero = "zero"
type Succ<N> = { n: N }
```

First, we define the number 0 with our type `Zero`

. Here, it is a type alias for the string `"zero"`

, but it could be anything. Next, we define `Succ`

which is a parameterized type (or generic type) that we will use for any number above 0. With these two types, we can now define 1 as `Succ<Zero>`

, 2 as `Succ<Succ<Zero>>`

, and so forth.

For convenience, we will create the following types for the numbers 1 through 10 which we will use later:

```
type One = Succ<Zero>
type Two = Succ<One>
type Three = Succ<Two>
type Four = Succ<Three>
type Five = Succ<Four>
type Six = Succ<Five>
type Seven = Succ<Six>
type Eight = Succ<Seven>
type Nine = Succ<Eight>
type Ten = Succ<Nine>
```

Correspondingly, we will define variables that match our types above. We will use the variables later when we are going to test that our `Fibonacci`

type works.

```
const zero: Zero = "zero"
const one: One = { n: zero }
const two: Two = { n: { ...one } }
const three: Three = { n: { ...two } }
const four: Four = { n: { ...three } }
const five: Five = { n: { ...four } }
// ...
const thirteen: Succ<Succ<Succ<Ten>>> = { n: { ...twelve } }
```

We now have a notion of what a number is which allows us to move on to the next part of our implementation.

To implement our `Fibonacci`

type, we need a few essential building blocks. We will start by defining the simplest types first.

For addition to work, we need to be able to *decrement* numbers. It will shortly become clearer why decrementing a number is important when we want to sum two numbers. We can define a `Decrement`

type in this way:

```
type Decrement<N> = N extends Succ<infer R> ? R : Zero
```

TypeScript supports inferring within conditional types which means that we can extract types from parameterized types. If `N`

extends `Succ`

, we extract the type `R`

and return it, and, otherwise, we return `Zero`

. `Decrement<Succ<Succ<Zero>>>`

would thus be equivalent to `Succ<Zero>`

.

Similarly, to check if a type is `Zero`

, we will need a type `IsZero`

that we define as such:

```
type IsZero<N> = N extends Zero ? true : false
```

With this type, `const typeChecks: IsZero<Zero> = true`

would type check while `const doesNotTypeCheck: IsZero<Succ<Zero>> = true`

would not.

Next, we need to have a way to do `if/else`

expressions so we can return types based on a given condition:

```
type IfElse<C extends boolean, T, F> = C extends true ? T : F
```

Here, `C`

can be either `true`

or `false`

, and if it is true, we return the type `T`

, and, otherwise, the type `F`

. So a variable with the type `IfElse<true, "foo", "bar">`

would only type check if it was assigned to the value `"foo"`

.

Three types are missing at this point: `Equals`

, `Add`

, and the `Fibonacci`

type. We define `Equals`

this way:

```
type Equals<A, B> =
A extends Succ<infer SA>
? B extends Succ<infer SB>
? Equals<SA, SB>
: false
: A extends Zero
? B extends Zero
? true
: false
: false
```

Checking for equality on a type-level in TypeScript is difficult to do elegantly, so the type definition above may be less clear than the types defined earlier in the blog post.

With this definition, two types are only equal if they are both `Zero`

. If `A`

and `B`

extends `Succ`

, then we recursively use our `Equals`

type with the extracted types `SA`

and `SB`

until both of the extracted types are `Zero`

, or one of them does not extend `Succ`

meaning that the two types are not equal.

Lastly, we need the `Add`

type to make computing Fibonacci numbers possible. The definition for this type is:

```
type Add<A, B> = {
acc: B
n: A extends Succ<infer _> ? Add<Decrement<A>, Succ<B>> : never
}[IfElse<IsZero<A>, "acc", "n">]
```

`Add`

works by recursively decrementing the first number, `A`

, and incrementing the second number, `B`

, until the `A`

is `Zero`

. So to add 2 and 3, the steps would be:

```
Step 1. Add<Succ<Succ<Zero>>, Succ<Succ<Succ<Zero>>>> // 2 + 3
Step 2. Add<Succ<Zero>, Succ<Succ<Succ<Succ<Zero>>>>> // 1 + 4
Step 3. Add<Zero, Succ<Succ<Succ<Succ<Succ<Zero>>>>>> // 0 + 5
```

Once we reach `Zero`

, we return the type `B`

by indexing the property `"acc"`

which is our result. In this case, `Succ<Succ<Succ<Succ<Succ<Zero>>>>>`

or simply 5.

All that is left now is to implement the `Fibonacci`

type which is defined as follows:

```
type Fibonacci<N, F0 = Zero, F1 = One> = {
acc: F0
n: N extends Succ<infer _> ? Fibonacci<Decrement<N>, F1, Add<F0, F1>> : never
}[IfElse<Equals<Zero, N>, "acc", "n">]
```

In our type parameter list, we first have `N`

which represents the nth number in the Fibonacci sequence we want to find. This type parameter is then followed by `F0`

and `F1`

which have the default types `Zero`

and `One`

, respectively. We use these two types to match the formal definition of the Fibonacci sequence which states that the first two numbers in the sequence should be 0 and 1.

The `Fibonacci`

type is similar to the `Add`

type in that it returns the result stored in our accumulator `"acc"`

once a type is `Zero`

(in this case, `N`

). Until we reach our base case, we keep recursing by indexing the property `"n"`

. For every step, we decrement `N`

, replace `F0`

with `F1`

, and calculate a new type for `F1`

by adding `F0`

and `F1`

together. Eventually, `N`

will become `Zero`

, and we have calculated our nth Fibonacci number.

Now we can finally put our newly defined `Fibonacci`

type to use and check that it works:

```
const fib0: Fibonacci<Zero> = zero
const fib1: Fibonacci<One> = one
const fib2: Fibonacci<Two> = one
const fib3: Fibonacci<Three> = two
const fib4: Fibonacci<Four> = three
const fib5: Fibonacci<Five> = five
const fib6: Fibonacci<Six> = eight
const fib7: Fibonacci<Seven> = thirteen
```

If you are testing this out yourself, you will see that the code only type checks if the value assigned to the variable matches to corresponding Fibonacci number. So if we change the value of `fib4`

to, say, `eight`

, our code will no longer type check.

Two things are worth pointing out here, though: a) TypeScript gives us an error stating that the “type instantiation is excessively deep and possibly infinite” once we try to compute any Fibonacci number larger than eight, and, b) any number from `Fibonacci<Five>`

and above will type check as long it is above five. Admittedly, it is unclear to me whether this is a limitation of the TypeScript type checker or an issue with my implementation, but it clearly shows that while it is possible to implement this, issues will likely occur sooner or later.

I hope you have found this blog post insightful. If you are curious and want to play around with the `Fibonacci`

type, you can find the code in a TypeScript playground here and a repository with more examples here.