Arithmetic with No Numbers

/**
 * Arithmetic with no numbers in it, performed entirely by the type checker.
 * Nothing below runs. All of it is computed before the program exists.
 */

/** A tuple of exactly N members: counting, done by building a thing to count. */
type Tally<N extends number, T extends unknown[] = []> =
  T["length"] extends N ? T : Tally<N, [...T, unknown]>;

/** Addition. Lay two tallies end to end and ask how long the result is. */
type Add<A extends number, B extends number> =
  [...Tally<A>, ...Tally<B>]["length"];

/** Subtraction. Take A apart until what remains is exactly B long. */
type Sub<A extends number, B extends number> =
  Tally<A> extends [...infer Rest, ...Tally<B>] ? Rest["length"] : never;

/** Multiplication is repeated addition, so it is repeated concatenation. */
type Mul<A extends number, B extends number, Acc extends unknown[] = []> =
  B extends 0 ? Acc["length"] : Mul<A, Sub<B, 1>, [...Acc, ...Tally<A>]>;

/** True only when the two types are exactly each other. */
type Is<X, Y> = X extends Y ? (Y extends X ? true : never) : never;

// Each of these is a proof. Break the arithmetic and the file stops compiling.
const three_and_four: Is<Add<3, 4>, 7> = true;
const ten_less_four: Is<Sub<10, 4>, 6> = true;
const six_sevens: Is<Mul<6, 7>, 42> = true;

// And one deliberate lie, to show the checker is awake rather than agreeable.
// @ts-expect-error three and four are not eight
const wrong_on_purpose: Is<Add<3, 4>, 8> = true;

export { three_and_four, ten_less_four, six_sevens, wrong_on_purpose };