From 90608fd0f6db3f9932678f120982a827cc6760fd Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 20 Apr 2023 20:47:03 -0500
Subject: [PATCH] not worth it

---
 test.ts          | 107 ++++++++++++++++++++++++++++++++++++++---------
 tsconfig.json    |   7 ++++
 typeLevelNats.ts |  44 +++++++++++++++----
 3 files changed, 130 insertions(+), 28 deletions(-)
 create mode 100644 tsconfig.json

diff --git a/test.ts b/test.ts
index a86845b..2c4d0dd 100644
--- a/test.ts
+++ b/test.ts
@@ -1,11 +1,11 @@
-import {} from "./typeLevelNats";
+import { Nat, NatOf, Suc, Zero, suc, zero } from "./typeLevelNats";
 
 type GenericFunction = (...x: never[]) => unknown;
 type Assume<T, U> = T extends U ? T : U;
 
-abstract class TypeFunc<Arg, Ret> {
-  readonly _1?: unknown;
-  new: (_: Arg) => Ret;
+abstract class TypeFunc<Arg, Ret, Param = unknown> {
+  readonly _1?: Param;
+  abstract new: (_: Arg) => Ret;
 }
 
 type Apply<Arg, Ret, F extends TypeFunc<Arg, Ret>, _1> = ReturnType<
@@ -26,10 +26,6 @@ interface ConstNat extends TypeFunc<any, Nat> {
   new: (_: any) => Nat;
 }
 
-interface DoubleSuc extends TypeFunc<Nat, Nat> {
-  new: (arg: Assume<this["_1"], Nat>) => Suc<Suc<typeof arg>>;
-}
-
 type NatElim0<
   M extends TypeFunc<Nat, any>,
   ZCase,
@@ -56,9 +52,91 @@ type NatElim0<
       >
     : never;
 
-interface DoubleNat extends TypeFunc<Nat, Nat> {
-  new: (arg: Nat) => NatElim0<ConstNat, Zero, DoubleSuc, typeof arg>;
+/*
+export interface DoubleSuc extends TypeFunc<Nat, Nat> {
+  new: (arg: Assume<this["_1"], Nat>) => Suc<Suc<typeof arg>>;
 }
+*/
+
+interface ExampleM extends TypeFunc<Nat, null[]> {
+  new: (
+    arg: Nat
+  ) => typeof arg extends Suc<infer Prev>
+    ? ["x", ...Apply<Nat, null[], ExampleM, Prev>]
+    : [];
+}
+export const _1: Apply<Nat, null[], ExampleM, Zero> = [];
+export const _2: Apply<Nat, null[], ExampleM, Zero> = [null];
+
+/**
+ * M is the type family being mapped over
+ * M : (n : N) -> U
+ * M zero = Nat
+ */
+interface DoubleNat_M extends TypeFunc<Nat, any> {
+  new: (arg: Nat) => Nat;
+  /*
+    typeof arg extends Suc<infer Prev>
+    ? Suc<Suc<Apply<Nat, Nat, DoubleNat_M, Prev>>>
+    : Zero; */
+}
+
+/**
+ * DoubleNat_SCase_App1 is what happens after applying 1 arg to DoubleNat_SCase
+ * (given n : N in the context)
+ * SCase_App1 : (prev : M n) -> M (suc n)
+ * SCase_App1 prev = prev + 2
+ */
+interface DoubleNat_SCase_App1<
+  M extends TypeFunc<Nat<any>, Nat<any>, any>,
+  N extends Nat<P>,
+  P = unknown
+> extends TypeFunc<
+    Apply<Nat<P>, Nat<any>, M, N>,            // (prev : M n)
+    Apply<Nat<Suc<P>>, Nat<any>, M, Suc<N>>,  // -> M (suc n)
+    Nat<unknown>
+  > {
+  new: (prev: Assume<this["_1"], Nat<P>>) => Suc<Suc<typeof prev>>;
+}
+
+/**
+ * This is the suc case for DoubleNat:
+ *   SCase : (n : N) -> (prev : M n) -> M (suc n)
+ */
+interface DoubleNat_SCase<M extends TypeFunc<Nat, Nat>>
+  extends TypeFunc<Nat, TypeFunc<Nat, Nat>> {
+  new: (arg: Nat) => DoubleNat_SCase_App1<M, typeof arg>;
+}
+export const _3: Apply<
+  Nat,
+  Nat,
+  Apply<Nat, TypeFunc<Nat, Nat>, DoubleNat_SCase<DoubleNat_M>, NatOf<4>>,
+  NatOf<4>
+> = suc(suc(suc(suc(suc(suc(zero))))));
+
+function isNatOfFour<T extends NatOf<4>>(_: T) {}
+/* 3 */ isNatOfFour(undefined as unknown as Suc<Suc<Suc<Zero>>>);
+/* 4 */ isNatOfFour(undefined as unknown as Suc<Suc<Suc<Suc<Zero>>>>);
+/* 5 */ isNatOfFour(undefined as unknown as Suc<Suc<Suc<Suc<Suc<Zero>>>>>);
+
+interface DoubleNat extends TypeFunc<Nat, Nat> {
+  new: (
+    arg: Nat
+  ) => NatElim0<ConstNat, Zero, DoubleNat_SCase<ConstNat>, typeof arg>;
+}
+
+type Two = Suc<Suc<Zero>>;
+function isTwo<F extends Two>(_: F) {}
+isTwo(suc(zero));
+isTwo(suc(suc(zero)));
+isTwo(suc(suc(suc(zero))));
+
+const realThree: Suc<Suc<Suc<Zero>>> = suc(suc(suc(zero)));
+const realFour: Suc<Suc<Suc<Suc<Zero>>>> = suc(suc(suc(suc(zero))));
+
+function isFour<F extends Apply<Nat, Nat, DoubleNat, Two>>(_: F) {}
+isFour(realThree);
+isFour(realFour);
 
 /*
 interface NatElim<
@@ -70,15 +148,6 @@ interface NatElim<
   _unused: (_1: ZCase, _2: SCase) => never;
   new: (arg: Assume<this["_1"], Nat>) => Apply<M, typeof arg>;
 }
-
-type Two = S<S<Z>>;
-
-const realThree: S<S<S<Z>>> = S.s();
-const realFour: S<S<S<S<Z>>>> = S.s();
-
-function isFour<F extends Apply<DoubleNat, Two>>(_: F) {}
-isFour(realThree);
-isFour(realFour);
 */
 
 /////
diff --git a/tsconfig.json b/tsconfig.json
new file mode 100644
index 0000000..63d3866
--- /dev/null
+++ b/tsconfig.json
@@ -0,0 +1,7 @@
+{
+    "compilerOptions": {
+        "strict": true,
+        "lib": ["esnext"],
+        "noUnusedLocals": false
+    }
+}
diff --git a/typeLevelNats.ts b/typeLevelNats.ts
index 852af15..e8fe8b2 100644
--- a/typeLevelNats.ts
+++ b/typeLevelNats.ts
@@ -1,8 +1,9 @@
 export type Zero = { tag: "Zero" };
 export type Suc<Prev> = { tag: "Suc"; prev: Prev };
+export type Nat<P = never> = Zero | Suc<P>;
 
-const zero: Zero = { tag: "Zero" };
-function suc<Prev>(p: Prev): Suc<Prev> {
+export const zero: Zero = { tag: "Zero" };
+export function suc<Prev>(p: Prev): Suc<Prev> {
   return { tag: "Suc", prev: p };
 }
 
@@ -27,22 +28,47 @@ type LengthOfTail<L extends any[]> = Length<Tail<L>>;
 const _10: LengthOfTail<[3, 4, 5]> = 2;
 const _11: LengthOfTail<[3, 4, 5]> = 3;
 
-type Nat<Num extends number> = BuildTuple<Num> extends ["x", ...infer rest]
-  ? Suc<Nat<Length<rest>>>
+export type NatOf<Num extends number> = BuildTuple<Num> extends [
+  "x",
+  ...infer rest
+]
+  ? Suc<NatOf<Length<rest>>>
   : Zero;
+
 const _15: ["x"] extends ["x", ...infer _] ? "true" : "false" = "true";
 const _16: ["x"] extends ["x", ...infer _] ? "true" : "false" = "false";
 
 const _17: [] extends ["x", ...infer _] ? "true" : "false" = "true";
 const _18: [] extends ["x", ...infer _] ? "true" : "false" = "false";
 
-const _1: Nat<0> = zero;
+const _1: NatOf<0> = zero;
 
-const _3: Nat<1> = suc(zero); // should pass
-const _2: Nat<1> = zero; // should fail
+const _3: NatOf<1> = suc(zero); // should pass
+const _2: NatOf<1> = zero; // should fail
 
-const _5: Nat<4> = suc(suc(suc(suc(zero)))); // should pass
-const _4: Nat<4> = suc(suc(suc(zero))); // should fail
+const _5: NatOf<4> = suc(suc(suc(suc(zero)))); // should pass
+const _4: NatOf<4> = suc(suc(suc(zero))); // should fail
+
+export {
+  _1,
+  _2,
+  _3,
+  _4,
+  _5,
+  _6,
+  _7,
+  _8,
+  _9,
+  _10,
+  _11,
+  _12,
+  _13,
+  _14,
+  _15,
+  _16,
+  _17,
+  _18,
+};
 
 type RealNats = [
   0,