aboutsummaryrefslogtreecommitdiff
path: root/src/index.ts
diff options
context:
space:
mode:
Diffstat (limited to 'src/index.ts')
-rw-r--r--src/index.ts43
1 files changed, 43 insertions, 0 deletions
diff --git a/src/index.ts b/src/index.ts
new file mode 100644
index 0000000..bd93300
--- /dev/null
+++ b/src/index.ts
@@ -0,0 +1,43 @@
+export type Op = string | { op: string; a: Op; b: Op };
+
+export type Rewrite<left extends Op, right extends Op> = {
+ type: 'rewrite';
+ left: left;
+ right: right;
+};
+export type RewriteKind = Rewrite<Op, Op>;
+
+export type Flip<R extends RewriteKind> = Rewrite<R['right'], R['left']>;
+
+export type ApplyRewrite<O extends Op, R extends RewriteKind> =
+ O extends R['left'] ? R['right']
+ : O extends string ? O
+ : O extends { a: Op, b: Op, op: string } ? (
+ ApplyRewrite<O['a'], R> extends O['a']
+ ? Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> }
+ : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
+ )
+ : never;
+
+export type Add<a extends Op, b extends Op> = { op: '+'; a: a; b: b };
+
+export type Identity<A extends Op> = Rewrite<Add<A, '0'>, A>;
+export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
+
+// type _x = ApplyRewrite<Add<'A', '1'>, Identity<'0'>>;
+
+// type Assoc<A extends Op, B extends Op> =
+
+/*
+
+Assoc: (a + b) + c = a + (b + c)
+
+For a = 0,
+(0 + b) + c
+= b + c
+= 0 + (b + c)
+
+For a = succ(),
+
+*/
+