Typescript Shenanigans

type-shenanigans.ts

// type Unary = 'Z' | `S${Unary}`; // considered circular

// Can implement unary addition and multiplication with template literal types
type Plus<T extends string, U extends string> = T extends `S${infer X}` ? `S${Plus<X, U>}` : U;
type Times<T extends string, U extends string> = T extends `S${infer X}` ? Plus<U, Times<X, U>> : 'Z';


// Trying to do length-aware vectors as dependent types
module Attempt1 {
  type Vector<T, LEN> = LEN extends `S${infer X}` ? [T, ...Vector<T, X>] : [];
  const exactly_three_strings: Vector<string, 'SSSZ'> = ['a', 'b', 'c'];

  function cons<T, LEN extends string>(h: T, tl: Vector<T, LEN>): Vector<T, `S${LEN}`> {
    const z: [T, ...typeof tl] = [h, ...tl];
    // Sadly Vector<T, `S${LEN}`> and [T, ...Vector<T, LEN>] don't unify, even
    // though they are equal for every particular instantiation of LEN
    return z as any as Vector<T, `S${LEN}`>;
  }
}

// Maybe represent numbers at the type-level as arrays of zeroes of the appropriate length?
module Attempt2 {
  type Vector<T, LEN> = LEN extends [0, ...infer X] ? [T, ...Vector<T, X>] : [];
  const exactly_four_strings: Vector<string, [0, 0, 0, 0]> = ['d', 'e', 'f', 'g'];

  function cons<T, LEN extends 0[]>(h: T, tl: Vector<T, LEN>): Vector<T, [0, ...LEN]> {
    const z: [T, ...typeof tl] = [h, ...tl];
    // Sadly Vector<T, [0, ...LEN]> and [T, ...Vector<T, LEN>] still don't unify!
    return z as any as Vector<T, [0, ...LEN]>
  }
}

// If I avoid ... in the type indexes, it seems to go ok
module Attempt3 {
  type Vector<T, LEN> = LEN extends [0, infer X] ? [T, ...Vector<T, X>] : [];
  const exactly_four_strings: Vector<string, [0, [0, [0, [0, []]]]]> = ['d', 'e', 'f', 'g'];

  function cons<T, LEN extends any[]>(h: T, tl: Vector<T, LEN>): Vector<T, [0, LEN]> {
    return [h, ...tl];
  }

  const empty: Vector<string, []> = [];
  // can't figure out how to convince generic argument inference to be smart here
  const vec = cons<string, [0, [0, []]]>('mumble', cons<string, [0, []]>('ho', cons('hi', empty)));
}