michael/ts-nat-comm
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

type level nats

Browse source
This commit is contained in:
Michael Zhang 2023-04-20 19:51:20 -05:00
parent b4f5c537ef
commit f6c3c6cf11
Signed by: michael
GPG key ID: BDA47A31A3C8EE6B
2 changed files with 359 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

85
test.ts
View file

@ -1,54 +1,76 @@
import {} from "./typeLevelNats";
type GenericFunction = (...x: never[]) => unknown;
type Assume<T, U> = T extends U ? T : U;
abstract class TypeFunc {
abstract class TypeFunc<Arg, Ret> {
readonly _1?: unknown;
new: GenericFunction;
new: (_: Arg) => Ret;
}
type Apply<F extends TypeFunc, _1> = ReturnType<
type Apply<Arg, Ret, F extends TypeFunc<Arg, Ret>, _1> = ReturnType<
(F & {
readonly _1: _1;
})["new"]
>;
class Z {
private constructor() {}
static z(): Z {
return new Z();
}
interface GetPrev<N extends Nat> extends TypeFunc<Suc<N>, N> {
new: (arg: Suc<N>) => N;
}
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();
}
// nat-elim : (M : T -> U) -> (cz : M z) -> (sz : (n : N) -> M n -> M (suc n)) -> (n : N) -> M n
// (M : T -> U) -> (cz : M z) -> (sz : (n : N) -> M n -> M (suc n)) -> (n : N) -> M n
//
interface ConstNat extends TypeFunc<any, Nat> {
new: (_: any) => Nat;
}
type Nat = Z | S<Nat>;
interface DoubleSuc extends TypeFunc<Nat, Nat> {
new: (arg: Assume<this["_1"], Nat>) => Suc<Suc<typeof arg>>;
}
interface NatElim<M extends TypeFunc, ZCase extends Apply<M, Z>, SCase extends TypeFunc>
extends TypeFunc {
type NatElim0<
M extends TypeFunc<Nat, any>,
ZCase,
SCase extends TypeFunc<
Nat,
TypeFunc<Apply<Nat, any, M, Nat>, Apply<Nat, any, M, Suc<Nat>>>
>,
N
> =
/** --------------------------------------------------------------- */
N extends Zero // // if N matches Zero
? ZCase // return ZCase
: N extends Suc<infer Prev> // if N matches Suc(Prev)
? Apply<
any /* TODO: */,
any /* TODO: */,
Apply<
Nat,
TypeFunc<Apply<Nat, any, M, Nat>, Apply<Nat, any, M, Suc<Nat>>>,
SCase,
Prev
>,
Apply<Nat, any, M, Prev>
>
: never;
interface DoubleNat extends TypeFunc<Nat, Nat> {
new: (arg: Nat) => NatElim0<ConstNat, Zero, DoubleSuc, typeof arg>;
}
/*
interface NatElim<
MRet,
M extends TypeFunc<Nat, MRet>,
ZCase extends Apply<infer A, infer R, M<A, R>, 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();
@ -57,6 +79,7 @@ const realFour: S<S<S<S<Z>>>> = S.s();
function isFour<F extends Apply<DoubleNat, Two>>(_: F) {}
isFour(realThree);
isFour(realFour);
*/
/////

305
typeLevelNats.ts Normal file
View file

@ -0,0 +1,305 @@
export type Zero = { tag: "Zero" };
export type Suc<Prev> = { tag: "Suc"; prev: Prev };
const zero: Zero = { tag: "Zero" };
function suc<Prev>(p: Prev): Suc<Prev> {
return { tag: "Suc", prev: p };
}
type BuildTuple<L extends keyof RealNats, T extends any[] = []> = T extends {
length: L;
}
? T
: BuildTuple<L, [...T, "x"]>;
const _12: BuildTuple<1> = ["x"];
const _13: BuildTuple<2> = ["x"];
const _14: BuildTuple<2> = ["x", "x"];
type Tail<L extends any[]> = L extends [unknown, ...infer rest] ? rest : never;
const _6: Tail<[1, 2, 3]> = [2, 3];
const _7: Tail<[1, 2, 3]> = [2, 4];
type Length<L extends any[]> = L extends { length: infer len } ? len : never;
const _8: Length<[3, 4, 5]> = 3;
const _9: Length<[3, 4, 5]> = 4;
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>>>
: 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 _3: Nat<1> = suc(zero); // should pass
const _2: Nat<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
type RealNats = [
0,
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,
44,
45,
46,
47,
48,
49,
50,
51,
52,
53,
54,
55,
56,
57,
58,
59,
60,
61,
62,
63,
64,
65,
66,
67,
68,
69,
70,
71,
72,
73,
74,
75,
76,
77,
78,
79,
80,
81,
82,
83,
84,
85,
86,
87,
88,
89,
90,
91,
92,
93,
94,
95,
96,
97,
98,
99,
100,
101,
102,
103,
104,
105,
106,
107,
108,
109,
110,
111,
112,
113,
114,
115,
116,
117,
118,
119,
120,
121,
122,
123,
124,
125,
126,
127,
128,
129,
130,
131,
132,
133,
134,
135,
136,
137,
138,
139,
140,
141,
142,
143,
144,
145,
146,
147,
148,
149,
150,
151,
152,
153,
154,
155,
156,
157,
158,
159,
160,
161,
162,
163,
164,
165,
166,
167,
168,
169,
170,
171,
172,
173,
174,
175,
176,
177,
178,
179,
180,
181,
182,
183,
184,
185,
186,
187,
188,
189,
190,
191,
192,
193,
194,
195,
196,
197,
198,
199,
200,
201,
202,
203,
204,
205,
206,
207,
208,
209,
210,
211,
212,
213,
214,
215,
216,
217,
218,
219,
220,
221,
222,
223,
224,
225,
226,
227,
228,
229,
230,
231,
232,
233,
234,
235,
236,
237,
238,
239,
240,
241,
242,
243,
244,
245,
246,
247,
248,
249,
250,
251,
252,
253,
254,
255,
256
];