Compute the Ackermann function using TS types

ackermann.ts

// Natural Numbers
interface Zero {
  isZero: true;
}
interface Successor<N extends Nat> {
  prev: N;
  isZero: false;
}
type Nat = Zero | Successor<Nat>;

// Helpers
type One = Successor<Zero>;
type Two = Successor<One>;
type Three = Successor<Two>;
type Four = Successor<Three>;
type Five = Successor<Four>;
type Six = Successor<Five>;
type Seven = Successor<Six>;
type Eight = Successor<Seven>;
type Nine = Successor<Eight>;
type Ten = Successor<Nine>;
type Eleven = Successor<Ten>;

// Operators
type Pred<N extends Nat> = N extends Successor<infer U> ? U : Zero;

type Add<N1 extends Nat, N2 extends Nat> = N1 extends Zero
  ? N2
  : N1 extends Successor<infer U>
  ? Successor<Add<U, N2>>
  : never;

type Times<N1 extends Nat, N2 extends Nat> = N1 extends Zero
  ? N1
  : N2 extends Successor<infer U2>
  ? Successor<N1 extends Successor<infer U1> ? Add<U2, Times<U1, N2>> : never>
  : Zero;

type Sub<N1 extends Nat, N2 extends Nat> = {
  0: N1;
  1: N2 extends Successor<infer U> ? Sub<Pred<N1>, U> : never;
}[N2 extends Zero ? 0 : 1];

// Ackermann Function
// This uses explicit boxing/unboxing on the second argument to fly under TS's circular reference radar.
type Acker<M extends Nat, N extends Nat> = FlattenBox<Acker_<M, Box<N>>>;
type Acker_<M extends Nat, N extends Box<any>> = M extends Zero
  ? Box<Successor<FlattenBox<N>>>
  : M extends Successor<infer PM>
  ? FlattenBox<N> extends Zero
    ? Box<Acker_<PM, Box<One>>>
    : FlattenBox<N> extends Successor<infer PN>
    ? Box<Acker_<PM, Acker_<M, Box<PN>>>>
    : never
  : never;

// Another version of Ackermann that uses an explicit Continuation Passing Style. TS types don't have
// first class "functions", so we pass closure data around in a nested data structure
type AckerCPS<M extends Nat, N extends Nat> = Acker_Tail<M, N, Closure<Zero, Nil>>;
type Acker_Tail<
  M extends Nat,
  N extends Nat,
  Fr extends Closure<Nat, Frame>
> = M extends Zero
  ? Fr extends Closure<infer ClosureM, infer LastClosure>
    ? LastClosure extends Closure<Nat, Frame>
      ? Acker_Tail<ClosureM, Successor<N>, LastClosure>
      : Successor<N>
    : never
  : M extends Successor<infer PM>
  ? N extends Zero
    ? Acker_Tail<PM, One, Fr>
    : N extends Successor<infer PN>
    ? Acker_Tail<M, PN, Closure<PM, Fr>>
    : never
  : never;
type Frame = Nil | Closure<Nat, Frame>;
interface Closure<M extends Nat, Past extends Frame> {
  m: M;
  prev: Past;
}

// Utils

interface Box<T> {
  val: T;
}
type FlattenBox<T> = {
  0: never;
  1: T extends Box<infer U> ? FlattenBox<U> : T;
}[T extends object ? 1 : 0];
// This cleaner alternative works in TS >= 4.1.x
//type FlattenBox<T> = T extends Box<infer U> ? FlattenBox<U> : T

// helper that flattens and subtracts one
type PredFlattenBox<NB extends Box<any>> = FlattenBox<NB> extends Successor<
  infer U
>
  ? Box<U>
  : Box<Zero>;

// Hyperoperation, a version of the Ackermann function that can perform +,x,^, ect. operations
type Hyper<N extends Nat, A extends Nat, B extends Nat> = FlattenBox<
  Hyper_<N, A, Box<B>>
>;
type Hyper_<N extends Nat, A extends Nat, B extends Box<any>> = N extends Zero
  ? Box<Successor<FlattenBox<B>>>
  : FlattenBox<B> extends Zero
  ? N extends One
    ? Box<A>
    : N extends Two
    ? Box<Zero>
    : N extends Successor<Nat>
    ? Box<One>
    : never
  : Box<Hyper_<Pred<N>, A, Hyper_<N, A, PredFlattenBox<B>>>>;

// Tests
// Simple operators
type TestAdd2And3 = Add<Two, Three>;
type TestAdd1And0 = Add<One, Zero>;
type TestAdd0And2 = Add<Zero, Two>;

type TestSub = Sub<Zero, Two>;
type TestSub2 = Sub<Two, Two>;
type TestSub3 = Sub<Five, Two>;
type TestSub4 = Sub<Five, Zero>;

type TestMul = Times<Four, Two>;
type TestMul2 = Times<Zero, Two>;
type TestMul3 = Times<Two, Zero>;
type TestMul4 = NatToDecimal<Times<Ten, Eleven>>;

// Ackermann Function
type TestAcker00 = Acker<Zero, Zero>; // 1
type TestAcker01 = Acker<Zero, One>; // 2
type TestAcker10 = Acker<One, Zero>; // 2
type TestAcker11 = Acker<One, One>; // 3
type TestAcker12 = Acker<One, Two>; // 4
type TestAcker21 = Acker<Two, One>; // 5
type TestAcker22 = Acker<Two, Two>; // 7
type TestAcker23 = Acker<Two, Three>; // 9
type TestAcker24 = Acker<Two, Four>; // 11
type TestAcker31 = NatToDecimal<Acker<Three, One>>; // 13

type TestAckerCPS00 = AckerCPS<Zero, Zero>; // 1
type TestAckerCPS01 = AckerCPS<Zero, One>; // 2
type TestAckerCPS10 = AckerCPS<One, Zero>; // 2
type TestAckerCPS11 = AckerCPS<One, One>; // 3
type TestAckerCPS12 = AckerCPS<One, Two>; // 4
type TestAckerCPS21 = AckerCPS<Two, One>; // 5
//type TestAckerCPS22 = AckerCPS<Two, Two>; // 7 (too much recursion error)

// Hyperoperation
// Test base cases
type TestHyper0 = Hyper<Zero, Two, Two>; // b + 1 if n = 0 -> 3
type TestHyper1 = Hyper<One, Two, Zero>; // a if n = 1 and b = 0 -> 2
type TestHyper2 = Hyper<Two, Two, Zero>; // 0 if n = 2 and b = 0 -> 0
type TestHyper3 = Hyper<Three, Two, Zero>; // 1 if n >= 3 and b = 0 -> 1
type TestHyper3b = Hyper<Four, Two, Zero>; // 1 if n >= 3 and b = 0 -> 1
// Test operators
type TestHyperAdd = Hyper<One, Two, Three>; // H1(2, 3) = 2 + 3 = 5
type TestHyperTimes = Hyper<Two, Two, Three>; // H2(2, 3) = 2 * 3 = 6
type TestHyperExponent = Hyper<Three, Two, Three>; // H3(2, 3) = 2^3 = 8
type TestHyperTetration = NatToDecimal<Hyper<Four, Two, Three>>; // H4(2, 3) = 2^2^2 = 16

// Check value
const five: TestAcker21 = {
  isZero: false,
  prev: {
    isZero: false,
    prev: {
      isZero: false,
      prev: {
        isZero: false,
        prev: {
          isZero: false,
          prev: {
            isZero: true,
          },
        },
      },
    },
  },
};

// Pretty print natural numbers as number literal
const fiveDecimal: NatToDecimal<TestAcker21> = 5;

// Pretty Print Utils
type Unshift<U extends any[], T extends any> = ((
  a: T,
  ...t: U
) => void) extends (...t: infer R) => void
  ? R
  : never;

type NatToDecimal<
  N extends Nat,
  __acc extends { state: NatToTupleResult<Nat, any[]>; done: boolean } = {
    state: NatToTupleResult<N, []>;
    done: false;
  }
> = {
  0: NatToDecimal<N, NatToUnaryTuple_<__acc["state"], 1, []>>;
  1: __acc["state"]["tuple"]["length"];
}[__acc["done"] extends true ? 1 : 0];

type NatToUnaryTuple<
  N extends Nat,
  Fill extends any = 1,
  __acc extends { state: NatToTupleResult<Nat, any[]>; done: boolean } = {
    state: NatToTupleResult<N, []>;
    done: false;
  }
> = {
  0: NatToDecimal<N, NatToUnaryTuple_<__acc["state"], Fill, []>>;
  1: __acc["state"]["tuple"];
}[__acc["done"] extends true ? 1 : 0];

// Trampoline
type NatToUnaryTuple_<
  T extends NatToTupleResult<Nat, any[]>,
  Fill extends any = 1,
  NumberOfBounces extends any[] = []
> = {
  2: { state: NatToTupleResult<T["nat"], T["tuple"]>; done: false };
  0: { state: NatToTupleResult<T["nat"], T["tuple"]>; done: true };
  1: T["nat"] extends Successor<infer U>
    ? NatToUnaryTuple_<
        NatToTupleResult<U, Unshift<T["tuple"], Fill>>,
        Fill,
        Unshift<NumberOfBounces, any>
      >
    : never;
}[T["nat"] extends Successor<Nat>
  ? NumberOfBounces["length"] extends 5
    ? 2
    : 1
  : 0];

interface NatToTupleResult<L, T> {
  nat: L;
  tuple: T;
}