Eight Queens Puzzle in TypeScript’s Type System

TypeScript’s type system is powerful enough to find a solution to complex problems without ever writing a value. Let’s look how!

This article will show some advanced use of TypeScript’s type system, and how we can translate runtime algorithms to type level algorithms, and let the compiler find a solution to our problem.

All the code below was tested with TypeScript v4.7.0

The complete solution at type level can be found here.

What is the Eight Queens puzzle?

The Eight Queens Puzzle is a problem described as follow:

Given a 8x8 chessboard, find a way to place 8 queens on the board safely.

A value level solution to this problem could be:

/* Generate an array containing number belows `n` */
function range(n: number): number[] {
  return Array(n)
    .fill(0)
    .map((_, i) => i);
}

/* Ensure the last queen in the passed array is safe from the other queens.*/
function validate(queens: number[]): boolean {
  const lastPos = queens.length - 1;
  const last = queens[lastPos];

  return !range(lastPos).some((pos) => {
    const stepVal = queens[pos];

    return stepVal == last || 
           Math.abs(lastPos - pos) == Math.abs(last - stepVal);
  });
}

function findSolution(queens: number[], step: number, tableSize: number): number[] | false {
  if (step === tableSize) {
    return queens;
  } else {
    return range(tableSize)
      .map((i) => [...queens, i + 1])
      .filter((q) => validate(q))
      .reduce<number[] | false>((acc, newQueens) => {
        return acc || findSolution(newQueens, step + 1, tableSize);
      }, false);
  }
}


console.log(findSolution([], 0, 8)) // display `[1, 5, 8, 6, 3, 7, 2, 4]`

This solution is written in a functional way — no mutability, no for - to simplify the translation to the type system.

Natural numbers

The first thing we’ll need are natural numbers . We could use types like 1 or 8 directly, but we cannot do any operation on them, and we'll need to be able to subtract those numbers. So, instead, we will re-implement natural number using Peano axioms;

type Z = { kind: 'Z' } // Represents 0
type S<T> = { kind: 'S', succ: T } // Represents the successor of the natural number T

type N0 = Z     // 0
type N1 = S<N0> // 1
type N2 = S<N1> // 2
type N3 = S<N2> // 3
type N4 = S<N3> // 4
type N5 = S<N4> // 5
type N6 = S<N5> // 6
type N7 = S<N6> // 7
type N8 = S<N7> // 8

Operation on natural numbers

In the type system, the equivalent of a function with n arguments is a type with n generic parameters. We'll start implementing the basic operations we need on natural numbers to solve our problem.

Subtraction

We will need to subtract 2 natural numbers.

At value level, we could implement the function like this:

// returns n - m,  or 0 if m > n
function sub(n: number, m: number): number {
  /* Obviously we could also write `return n - m` 
     But the goal is to have something translatable at type level, 
     and `-` doesn't exist at type level. */
  if ( m > 0 ) {
    if ( n > 0 ) {
      return sub(n -1, m -1);	
    } else {
      return 0;		
    } 
  } else {
    return n;
  }
}

At type level, conditional types are analogous to a form of pattern matching, like a if or a switch/case, but declaring a new variable at the same time (with the keyword infer) ;

So we can translate the above function at type level:

// Returns N - M, returns 0 if M > N
type Sub<N, M> = 
  M extends S<infer PM>?N extends S<infer PN>?Sub<PN, PM>:Z:N;

Other Nat operators

We will need an equality comparator. We can use the one described in this article

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

From there, we will also need to check if one number is greater than another. We’ll use the same logic than previously, ie: if A and B are not equal to 0 , then A will be greater than B implies that (A — 1) is greater than (B — 1)

type GT<A, B> = A extends S<infer PA> ? (B extends S<infer PB> ? GT<PA, PB> : true) : false;

Finally, in our original (value level) code, a subtraction is done inside Math.abs. Because Sub can never return a negative number, we need to implement at the type level a function equivalent to (a: number, b:number) => Math.abs(a - b)

type AbsSub<A, B> = GT<A, B> extends true ? Sub<A, B> : Sub<B, A>;

Boolean logic

TypeScript already supports true and false types, so we don't need to reimplement them. We need to define some simple operations on those types though:

type Or<A extends boolean, B extends boolean> = A extends true ? true : B;
type Not<A extends boolean> = A extends true ? false : true;

Implementing range function

TypeScript supports tuple types and we’ll use that to represent a range.

We’ll create a generic type generating a tuple type of the size specified in the generic.

At value level, we could write something like

function range(n: number): number[] {
  if ( n > 0 ) {
    return [...range(n -1), n - 1]
  } else {
    return [];
  }
}

We can translate that directly in the type system, as the spread operator ... is also working on tuple at type level.

type RangeTuple<N> = N extends S<infer PN> ? [...RangeTuple<PN>, PN] : [];

If we “test” this tuple we can see for example:

type Test1 = RangeTuple<Z> // Test1 is []
type Test2 = RangeTuple<N3> // Test2 is [Z, N1, N2]

In TypeScript playground, you can hover the code with your mouse to see the computed result type.

Operations on Tuples

Because we don’t use the number literal types from TypeScript, we have to reimplement a size and at operation on tuples to works with our natural number type:

type Size<ARR> = ARR extends [infer HEAD, ...infer TAIL] ? S<Size<TAIL>> : Z;

Here we see another trick we will use at a lot of places: we’re testing if the tuple is made of a first element (the HEAD), followed by another tuple (the TAIL). So the code above is a way to traverse the tuple recursively at type level: if ARR has a HEAD and TAIL, it's not empty, and its size is 1 + the size of the tail. Otherwise, it's the empty tuple ([]) and its size is 0.

Now, we need a at function to get the nth element of the tuple.

type At<ARR extends unknown[], N> = 
  ARR extends [infer HEAD, ...infer TAIL]
    ? N extends S<infer PN>
      ? At<TAIL, PN>
      : HEAD
    : never;

Here we see that in case of an invalid value (trying to access an element of an empty array), we will return never which we will consider as an error at type level.

Implementing validate function

This function checks if a position is valid. We will follow the initial implementation and translate it at runtime:

stepVal == last || Math.abs(lastPos - pos) == Math.abs(last - stepVal);

Can be represented by:

type ValidateOnePoint<POS, STEP_VAL, LAST_POS, LAST> = Or<
  Eq<STEP_VAL, LAST>,
  Eq<AbsSub<LAST_POS, POS>, AbsSub<LAST, STEP_VAL>>
>;

I’ve kept same naming to help understand the translation.

But, as we can deduce STEP_VAL and LAST from the tuple passed in parameter, we can create a type taking only POS, LAST_POS and the tuple QUEENS as parameter:

type ValidateOnePointFromArr<POS, LAST_POS, QUEENS extends unknown[]> = ValidateOnePoint<
  POS,
  At<QUEENS, POS>,
  LAST_POS,
  At<QUEENS, LAST_POS>
>;

We now need to implement an equivalent of some methods of array. some can defined recursively like that:

function some<A>(arr: A[], predicate: (a:A) => boolean): boolean {
   if(arr.length > 0) {
      const [head, ...tail] = arr;
      if (predicate(head)) {  
          return true;
       } else {
           return some(tail, predicate)
       }
   } else {
      return false
   }
}

some is a higher order function - a function taking a function as parameter. At type level, the analogous of higher order functions are Higher-Kinded Types. TypeScript doesn't support Higher-Kinded types, so we'll have to workaround this problem by creating a non generic version of some, specialized for our validate problem.

type SomeInvalidPoint<RANGE, QUEENS extends unknown[]> = RANGE extends [infer HEAD, ...infer TAIL]
  ? ValidateOnePointFromArr<HEAD, Sub<Size<QUEENS>, N1>, QUEENS> extends true
    ? true
    : SomeInvalidPoint<TAIL, QUEENS>
  : false;

and finally, we can create our Validate type like that:

type Validate<QUEENS extends unknown[]> = Not<SomeInvalidPoint<RangeTuple<Sub<Size<QUEENS>, N1>>, QUEENS>>;

it can be tested like that

type TestValidate1 = Validate<[N1, N2]> // equivalent to false
type TestValidate2 = Validate<[N1, N5]> // equivalent to true

Implementing findSolution

To implement findSolution, we'll need an equivalent of map, filter and reduce methods. They can be implemented like this at value level:

function filter<A>(arr: A[], predicate: (a:A) => boolean): A[] {
  if(arr.length > 0) {
      const [head, ...tail] = arr;
      if(predicate(head)) {  
          return [head, ...filter(tail, predicate)];
       } else {
           return filter(tail, predicate);
       }
   } else {
      return false;
   }
}

function map<A, B>(arr: A[], fn: (a:A) => B): B[] {
  if(arr.length > 0) {
    const [head, ...tail] = arr; 
    return [fn(head), ...map(tail, fn)]; 
  } else {
    return [];
  }
}

function reduce<A,B>(arr: A[], fn: (b:B, a:A) => B, init: B): B {
  if (arr.length > 0) {
    const [head, ...tail] = arr;
    return reduce(tail, fn, fn(init, head));	
  } else {
    return init;
  }
}

Once again, as they are higher-order functions, we won’t be able to implement a generic version of those, and we’ll need to implement a map, a filter, and a reduce specialized for our need.

type FilterValidArr<QUEENS extends unknown[][]> = QUEENS extends [infer HEAD extends unknown[], ...infer TAIL extends unknown[][]]
      ? Validate<HEAD> extends true
        ? [HEAD, ...FilterValidArr<TAIL>]
        : FilterValidArr<TAIL>
  : [];

type MapPossiblePositions<QUEENS extends unknown[], TABLE_SIZE> = TABLE_SIZE extends S<infer PN>
  ? [...MapPossiblePositions<QUEENS, PN>, [...QUEENS, TABLE_SIZE]]
  : [];


type ReduceToOneSolution<INIT, ARR, STEP, TABLE_SIZE> = ARR extends [infer HEAD extends unknown[], ...infer TAIL]
    ? ReduceToOneSolution<
        INIT extends false ? FindSolution<HEAD, S<STEP>, TABLE_SIZE> : INIT,
        TAIL,
        STEP,
        TABLE_SIZE
      >
  : INIT;

As the reduce function calls recursively the FindSolution type, we need to finally create this type:

type FindSolution<QUEENS extends unknown[], STEP, TABLE_SIZE> = Eq<STEP, TABLE_SIZE> extends true
  ? QUEENS
  : ReduceToOneSolution<false, FilterValidArr<MapPossiblePositions<QUEENS, TABLE_SIZE>>, STEP, TABLE_SIZE>;

Checking the result

We can now check that our algorithm works:

type Result = FindSolution<[], Z, N8>

and we’ll see, after a few seconds, that Result holds the type [N1, N5, N8, N6, N3, N7, N2, N4] which is a valid solution of the eight queen problem.

So in conclusion: we were able to solve this puzzle without ever writing a value.

Should you do that?

Quick answer: no. Not in a professional project anyway. Even if TypeScript’s type system is able to compute this kind of things, the compiler is very slow to do so, and the code is hard to read and error prone: in a sense, the language defined by the type system of TypeScript is a slow dynamically typed language :). This kind of exercise must be taken only as an exercise to better understand how the TypeScript’s type checker works — and maybe be amazed at the available features of this language!

Thanks to Aphyr and this post for the idea behind this article.