TypeScript type-level Peano arithmetic

main.ts

type Zero = [];
type NN = number[];

type GetNN<N extends NN> = N['length'];
type NextNN<N extends NN> = [...N, N['length']];
type PrevNN<N extends NN> = N extends [...infer Init, infer _] ? Init : never;

type EqualNN<A extends NN, B extends NN> =
  GetNN<A> extends GetNN<B> ? true : false;

type Make<N extends number, Base extends NN = Zero> =
  N extends GetNN<Base> ? Base : Make<N, NextNN<Base>>;

type AddNN<A extends NN, B extends NN> = B extends Zero
  ? A
  : B extends NextNN<infer Prev>
    ? NextNN<AddNN<A, Prev>>
    : never;

type MultiplyNN<A extends NN, B extends NN> = B extends Zero
  ? Zero
  : B extends NextNN<infer Prev>
    ? AddNN<A, MultiplyNN<A, Prev>>
    : B;