dependent.ts

type Zero = [];
type Nat = [Nat] | Zero;
type NonZeroNat = [NonZeroNat] | [Zero];

type Inc<A extends Nat> = [A];
type Dec<A extends NonZeroNat> = A[0];
type Add<A extends Nat, B extends Nat> = Add_<A, B>;

// This trick taken from https://github.com/Microsoft/TypeScript/pull/24897
type Add_<A extends Nat, B extends Nat> = {
  1: B;
  2: A extends NonZeroNat ? Add_<Dec<A>, Inc<B>> : never;
}[A extends NonZeroNat ? 2 : 1];

type One = Inc<Zero>;
const zero: Zero = [];
const one: One = [[]];
const two: Add<One, One> = [[[]]];

const inc = <N extends Nat>(n: N): Inc<N> => [n];
const dec = <N extends NonZeroNat>(n: N): Dec<N> => n[0];

const add = <A extends Nat, B extends Nat>(a: A, b: B): Add<A, B> => {
  // Sadly this doesn't work as the type checker overflows
  return a === [] as Zero ? b : add(a[0] as Dec<A>, [b] as Inc<B>);
};