108 lines
2.2 KiB
TypeScript
108 lines
2.2 KiB
TypeScript
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();
|
|
}
|