1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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(),
*/
|
