TypeScriptの型で虫食い算を解く
TypeScriptの型で虫食い算を解く
1~3の相異なる値で、T1 + T2 = T3を満たすものを見つける、という簡単な問題
数は二進法表記して加算を1ビットの論理演算で構築
チャーチ数使おうとしてTypeScriptは型を再帰的に定義できない？の罠にハマった
条件式の表現はanyかneverを返す形にした
条件のand演算が型のインターセクションに対応づく
テストコードは結果の型に"OK"を代入する、結果がneverなら型エラーになる
割り算は式変形で消せるので、大きめの数値型と掛け算を実装すればできるはず…
ts type BIN = 0 | 1;
type XOR<A extends BIN, B extends BIN> = (
A extends 0 ? B : (B extends 0 ? A : 0)
)
type AND<A extends BIN, B extends BIN> = (
A extends 0 ? 0 : B
)
type B2 = [BIN, BIN];
type N1 = [0, 1];
type N2 = [1, 0];
type N3 = [1, 1];
type ADD2DIGIT<A extends B2, B extends B2> = (
[
XOR<XOR<AND<A[1], B[1]>, A[0]>, B[0]>,
XOR<A[1], B[1]>
]
)
type EQUAL<A extends B2, B extends B2> = (
A extends B ? any : never
);
let a1: EQUAL<ADD2DIGIT<N1, N2>, N3> = "OK";
// let a2: EQUAL<ADD2DIGIT<N1, N1>, N3> = "OK"; // NG
// CONSTRAINT: T1 + T2 = T3
type CONSTRAINT<
T1 extends B2,
T2 extends B2,
T3 extends B2
> = (
EQUAL<ADD2DIGIT<T1, T2>, T3>
);
let b1: CONSTRAINT<N1, N1, N2> = "OK";
// let b2: CONSTRAINT<N1, N1, N3> = "OK"; // NG
let b3: CONSTRAINT<N2, N1, N3> = "OK";
type IS_PERMUTATION<
T1 extends B2,
T2 extends B2,
T3 extends B2
> =
T2 extends T1 ? never : (T3 extends (T1 | T2) ? never : any);
let c1: IS_PERMUTATION<N1, N2, N3> = "OK";
// let c2: IS_PERMUTATION<N2, N3, N2> = "OK"; // NG
let c3: IS_PERMUTATION<N2, N1, N3> = "OK";
type IS_SOLUTION<T1 extends B2, T2 extends B2, T3 extends B2> = (
IS_PERMUTATION<T1, T2, T3> & CONSTRAINT<T1, T2, T3>
);
let d1: IS_SOLUTION<N1, N2, N3> = "OK";
let d2: IS_SOLUTION<N2, N1, N3> = "OK";
// let d3: IS_SOLUTION<N1, N1, N2> = "OK"; // NG
// let d4: IS_SOLUTION<N2, N1, N2> = "OK"; // NG全加算器とリンクリストを作った
が、型エイリアスが再帰呼び出しできないためN個の型引数をとってN-1個の型引数で呼ぶとかができない
のでADDER3がADDER2を呼ぶみたいな書き方が必要になってあまり嬉しくない
tstype FULL_ADDER<A extends BIN, B extends BIN, CARRY extends BIN> = (
[
XOR<AND<A, B>, AND<XOR<A, B>, CARRY>>,
XOR<XOR<A, B>, CARRY>
]
);
type BODY<BIN2 extends [BIN, BIN]> = BIN2[1];
type CARRY<BIN2 extends [BIN, BIN]> = BIN2[0];
type LIST = BIN | [BIN, LIST]
type CAR<X extends LIST> = (
X extends [BIN, LIST] ? X[0] : X
)
type CDR<X extends LIST> = (
X extends [BIN, LIST] ? X[1] : never
)
type CHAIN1<
P extends LIST, A1 extends BIN, B1 extends BIN,
FA1 = FULL_ADDER<A1, B1, CAR<P>>
> = (
FA1 extends [BIN, BIN] ?
[
CARRY<FA1>,
[
BODY<FA1>,
CDR<P>
]
] : never
)
type ADDER2<
A1 extends BIN, A2 extends BIN,
B1 extends BIN, B2 extends BIN,
P = FULL_ADDER<A2, B2, 0>
> = (
P extends LIST ?
CHAIN1<P, A1, B1>
: never
)
type ADDER3<
A1 extends BIN, A2 extends BIN, A3 extends BIN,
B1 extends BIN, B2 extends BIN, B3 extends BIN,
P = ADDER2<A2, A3, B2, B3>
> = (
P extends LIST ?
CHAIN1<P, A1, B1>
: never
)
{
const a1: ADDER3<1, 1, 1, 1, 1, 1> = [1, [1, [1, 0]]]
const a2: ADDER3<1, 1, 0, 1, 1, 1> = [1, [1, [0, 1]]]
const a3: ADDER3<1, 1, 0, 0, 1, 1> = [1, [0, [0, 1]]]
}"Engineer's way of creating knowledge" the English version of my book is now available on [Engineer's way of creating knowledge]
(C)NISHIO Hirokazu / Converted from [Scrapbox] at [Edit]