Typed arrays of fixed length with Typescript

vector.ts

/* Naturals using Peano numbers. See https://ostro.ws/2019/12/09/taking-types-too-far/ */

type Zero = { prev: never };
type Nat = { prev: Nat };
type Succ<N extends Nat> = { prev: N };
type Prev<N extends Nat> = N["prev"];

type Nats = {
    0: Zero;
    1: Succ<Zero>;
    2: Succ<Succ<Zero>>;
    3: Succ<Succ<Succ<Zero>>>;
    // ....
};

type MkNat<N extends keyof Nats> = Nats[N];

/* Vector */

type Cons<H, T extends any[]> = ((h: H, ...t: T) => void) extends ((...u: infer U) => void)
    ? U
    : never;

type VectorTailRec<T, Length extends Nat, Output extends any[]> = {
    0: Output;
    1: VectorTailRec<T, Prev<Length>, Cons<T, Output>>;
}[Length extends Zero ? 0 : 1];

type Vector<T, Length extends Nat> = VectorTailRec<T, Length, []>;

/* Example */

type V3 = Vector<number, MkNat<3>>;
const vectorOfThree: V3 = [1, 2, 3];