From b4f5c537ef8c1820e135c71d6936db6c2da82920 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 20 Apr 2023 18:14:48 -0500
Subject: [PATCH] initial

---
 .gitignore |   1 +
 test.ts    | 108 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 109 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 test.ts

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..3c3629e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+node_modules
diff --git a/test.ts b/test.ts
new file mode 100644
index 0000000..ba53524
--- /dev/null
+++ b/test.ts
@@ -0,0 +1,108 @@
+type GenericFunction = (...x: never[]) => unknown;
+type Assume<T, U> = T extends U ? T : U;
+
+abstract class TypeFunc {
+  readonly _1?: unknown;
+  new: GenericFunction;
+}
+
+type Apply<F extends TypeFunc, _1> = ReturnType<
+  (F & {
+    readonly _1: _1;
+  })["new"]
+>;
+
+class Z {
+  private constructor() {}
+  static z(): Z {
+    return new Z();
+  }
+}
+
+class S<Prev extends Z | S<any>> {
+  public prev: (_: Prev) => Prev;
+  private constructor() {}
+  static s<Prev extends Z | S<any>>(): S<Prev> {
+    return new S();
+  }
+}
+
+type Nat = Z | S<Nat>;
+
+interface NatElim<M extends TypeFunc, ZCase extends Apply<M, Z>, SCase extends TypeFunc>
+  extends TypeFunc {
+  _unused: (_1: ZCase, _2: SCase) => never;
+  new: (arg: Assume<this["_1"], Nat>) => Apply<M, typeof arg>;
+}
+
+interface ConstNat extends TypeFunc {
+  new: (_: unknown) => Nat;
+}
+
+interface DoubleSuc extends TypeFunc {
+  new: (arg: Assume<this["_1"], Nat>) => S<S<typeof arg>>;
+}
+
+interface DoubleNat extends TypeFunc {
+  new: (
+    arg: Assume<this["_1"], Nat>
+  ) => Apply<NatElim<ConstNat, Z, DoubleSuc>, 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);
+
+/////
+
+type Length<T extends any[]> = T extends { length: infer L } ? L : never;
+
+type BuildTuple<L extends number, T extends any[] = []> = T extends {
+  length: L;
+}
+  ? T
+  : BuildTuple<L, [...T, any]>;
+
+type Add<A extends number, B extends number> = Length<
+  [...BuildTuple<A>, ...BuildTuple<B>]
+>;
+
+type Equals<T, T1 extends T, T2 extends T> = { eq: [T1, T2] };
+
+type Seven = Add<3, 4>; // 7
+
+function isSeven(s: Seven) {}
+isSeven(6);
+isSeven(7);
+
+///
+
+class Eq<A, B> {
+  private a: (_: A) => A;
+  private b: (_: B) => B;
+  private constructor() {}
+  static refl<T>(): Eq<T, T> {
+    return new Eq();
+  }
+}
+
+function isEqual1(_: Eq<3, 3>) {}
+isEqual1(Eq.refl());
+function isEqual2(_: Eq<3, 4>) {}
+isEqual2(Eq.refl());
+function isEqual3(_: Eq<Add<3, 4>, 7>) {}
+isEqual3(Eq.refl());
+function isEqual4(_: Eq<Add<3, 4>, 8>) {}
+isEqual4(Eq.refl());
+
+///
+
+type Commutative<A extends number, B extends number> = Eq<Add<A, B>, Add<B, A>>;
+function comm<A extends number, B extends number>(): Commutative<A, B> {
+  return Eq.refl();
+}