TypeScriptの型レベルプログラミングで数独を解く
これは、FORCIA Advent Calendar 2021の21日目の記事です。
こんにちは。第二旅行プラットフォーム部エンジニアの浦上です。アドベントカレンダーの枠を取ってみたはいいものの特にネタが思いつかずフォルシアの過去のアドベントカレンダーを遡っていたところこのような記事を見つけました。
プログラミング言語ではなく、フォルシアの高速検索の鍵を握るSQLで数独を解く
なるほど、アドベントカレンダーというのはCやPythonのような『普通の』プログラミング言語以外で数独を解けばよいのですね。 ということでこの記事ではTypeScriptの『型』だけを用いて数独を解いていこうと思います。
盤面の表し方
まずは、数独の問題を表現する型を作りましょう。 扱いやすいように、以下のルールで扱うことにしました。
- 埋まっているマスは
1から9の数値リテラル型で表す。 - 空きマスは数値リテラル型
0で表す。 - 盤面全体は、左上から順に長さ81のタプル型で表す。
以上をコードで表すと下記のようになります。Problem1も変数ではなく「初項から順に数値リテラル0,2,4, ......である長さ81のタプル型」であることにご注意ください。
// 使用可能な数字は1から9まで type Digit = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9; // 空きマスは0で表す type Empty = 0; // 長さ9のタプル型 type Tuple9<T> = [T, T, T, T, T, T, T, T, T]; // 長さ81のタプル型 type Tuple81<T> = [ ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T>, ...Tuple9<T> ]; // 数独の問題を表す型 type Problem = Tuple81<Digit | Empty>; // 問題例 type Problem1 = [ 0, 2, 4, 0, 8, 7, 5, 0, 9, 8, 9, 1, 4, 5, 6, 3, 7, 2, 5, 6, 7, 0, 9, 3, 0, 0, 1, 7, 8, 6, 5, 2, 9, 0, 3, 4, 2, 0, 0, 3, 1, 0, 0, 0, 0, 1, 4, 0, 6, 7, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 3, 0, 0, 0, 0, 0, 1, 0, 9, 0, 0, 0, 0, 5, 0, 0, 0, ];
準備
数独を解くために必要となる型をいくつか準備しておきましょう。
// タプルのindexを行番号に変換するための型 type ToRow = [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, 5, 5, 5, 5, 5, 5, 5, 5, 6, 6, 6, 6, 6, 6, 6, 6, 6, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8, 8, 8 ]; type PopValue<T extends Digit[], K extends number, V extends Digit | Empty> = { [key in keyof T]: key extends `${K}` ? Exclude<T[key], V> : T[key]; }; type RowLimit< Board extends Problem, Ret extends Tuple9<Digit> = Tuple9<Digit>, I extends unknown[] = [] > = I["length"] extends 81 ? Ret : RowLimit< Board, PopValue<Ret, ToRow[I["length"]], Board[I["length"]]>, [...I, unknown] >; // 以下は使用例 type Ex1 = PopValue<[1 | 2 | 3, 3], 0, 2> // -> [1 | 3, 3]; type Ex2 = PopValue<[1 | 2 | 3, 3], 1, 3> // -> [1 | 2 | 3, never]; type RowLimitProblem1 = RowLimit<Problem1>; /* -> [ 1 | 3 | 6, never, 2 | 4 | 8, 1, 9 | 4 | 5 | 6 | 7 | 8, 9 | 2 | 3 | 5, 9 | 1 | 2 | 3 | 4 | 5 | 7 | 8, 9 | 2 | 4 | 5 | 6 | 7 | 8, 1 | 2 | 3 | 4 | 6 | 7 | 8 ] */
PopValueはタプル型の第K項から型Vを削除するための型です。使用例はEx1、Ex2をご覧ください。
RowLimitは「0〜8行目(TypeScriptの配列は0から数えるのでそれに合わせて1〜9行目でなく0〜8行目と表しています)のそれぞれについて、まだ使われていない数字はどれか」というのを表現する型です。上記の例だと、1番上の行には1,3,6がまだ使われていないこと、その下の行はもう完成していて何も使えないこと、などを表しています。
これがどのように実現されているかというと
Retの初期値をTuple9<Digit>、つまりすべての行に1から9すべてが使える状態にしておく- 左上のマスから順に、
Retの「そのマスの行番号」から「そのマスに書かれている数字」を削除する - 右下のマスまで見終わったら終了
ということをしています。タプル型Iの長さを1ずつ増やしながら再帰することで型でもfor文のようなことを実現できます。
「行」だけでなく「列」「グループ(3×3の正方形)」の条件もつくるために、ToColumn・ToSquare、ColumnLimit・SquareLimitも同様に定義しておきます。
// タプルのindexを列番号に変換するための型 type ToColumn = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8 ]; // タプルのindexを3×3のグループの番号に変換するための型 type ToSquare = [ 0, 0, 0, 1, 1, 1, 2, 2, 2, 0, 0, 0, 1, 1, 1, 2, 2, 2, 0, 0, 0, 1, 1, 1, 2, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 5, 3, 3, 3, 4, 4, 4, 5, 5, 5, 3, 3, 3, 4, 4, 4, 5, 5, 5, 6, 6, 6, 7, 7, 7, 8, 8, 8, 6, 6, 6, 7, 7, 7, 8, 8, 8, 6, 6, 6, 7, 7, 7, 8, 8, 8 ]; type ColumnLimit< Board extends Problem, Ret extends Tuple9<Digit> = Tuple9<Digit>, I extends unknown[] = [] > = I["length"] extends 81 ? Ret : ColumnLimit< Board, PopValue<Ret, ToColumn[I["length"]], Board[I["length"]]>, [...I, unknown] >; type SquareLimit< Board extends Problem, Ret extends Tuple9<Digit> = Tuple9<Digit>, I extends unknown[] = [] > = I["length"] extends 81 ? Ret : SquareLimit< Board, PopValue<Ret, ToSquare[I["length"]], Board[I["length"]]>, [...I, unknown] >;
なお、このコードはTypeScript4.4以前だと再帰回数の上限を超えてしまいエラーとなってしまいます。TypeScript4.5で型レベルでの末尾再帰最適化が行われるようになったので動くようになりました。この機能が追加されていなければ今回の記事は実現しなかったでしょう。
数独を解く
それではいよいよ数独を解いていきましょう。結論から書いてしまうと、以下の型で数独を解くことができます。
type Solve< Board extends Problem, Row extends Tuple9<Digit> = RowLimit<Board>, Column extends Tuple9<Digit> = ColumnLimit<Board>, Square extends Tuple9<Digit> = SquareLimit<Board>, Answer extends Digit[] = [], L extends number = Answer["length"], T = Board[L] extends Empty ? Row[ToRow[L]] & Column[ToColumn[L]] & Square[ToSquare[L]] : Board[L] > = L extends 81 ? Answer : T extends Digit ? Solve< Board, PopValue<Row, ToRow[L], T>, PopValue<Column, ToColumn[L], T>, PopValue<Square, ToSquare[L], T>, [...Answer, T] > : never;
上のコードは「左上のマスから順番に『そのマスに使える数字を1つ選んで埋めて、次のマスに進む』を繰り返す。最後(右下)のマスまで詰まずに埋めることができたらそれが答え」という方針を実現するコードです。
まずは各型変数の説明です。
Board：問題の盤面を表すRow：(現時点で)各行でまだ使われていない数字はどれかを表す長さ9のタプル型。Column、Square：Rowの「行」を「列」、「グループ」に置き換えたもの。Answer：左上から順に埋めた数字を記録していくタプル型。これの長さが81まで達するとそのときのAnswerが解。L：Answerの長さは色々なところで使うので見やすさのために新たに文字で置いたもの。「ここまでいくつ埋めたか」を表すと同時に、「今から埋めようとしているマスのindex」も表している。T：今から埋めようとしているマス(=L番目のマス)で使うことのできる数字を表す型。BoardのLマス目に応じて以下のように決まる。- 問題で埋まっているマスならその数字しか使えないので
Board[L] - 空きマスなら行、列、グループの条件をすべて守る必要があるので
Row[ToRow[L]]、Column[ToColumn[L]]、Square[ToSquare[L]]の交差型。ここで、例えばRow[ToRow[L]]は「L番目のマス目の属している行で使える数字」を表すことに注意。
- 問題で埋まっているマスならその数字しか使えないので
T extends Digit ? ...によってTにunion distributionが適用される(union distributionについてはこちらの記事の解説がとても分かりやすいです)ので、例えばTが1|3であった場合、
Solve< Board, PopValue<Row, ToRow[L], 1>, PopValue<Column, ToColumn[L], 1>, PopValue<Square, ToSquare[L], 1>, [...Answer, 1] > | Solve< Board, PopValue<Row, ToRow[L], 3>, PopValue<Column, ToColumn[L], 3>, PopValue<Square, ToSquare[L], 3>, [...Answer, 3] >
と展開されます。要は
Answerに埋めようとしている数字を追加L番目のマスが所属する行、列、グループのそれぞれからL番目のマスに使った数字を削除
した状態で次の再帰に進みます。 途中でTがnever型になってしまった、つまり使える数字が1つもなくなってしまった場合にはその分岐はneverを返却して終了するので、無事81マスすべて埋めることができたものだけが最終的な答えとなるわけです。
実際に問題を解いてみる
早速何問か解いてみましょう。
type Answer1 = Solve<Problem1>; /* -> [ 3, 2, 4, 1, 8, 7, 5, 6, 9, 8, 9, 1, 4, 5, 6, 3, 7, 2, 5, 6, 7, 2, 9, 3, 8, 4, 1, 7, 8, 6, 5, 2, 9, 1, 3, 4, 2, 5, 9, 3, 1, 4, 7, 8, 6, 1, 4, 3, 6, 7, 8, 2, 9, 5, 4, 7, 2, 9, 3, 1, 6, 5, 8, 6, 3, 5, 8, 4, 2, 9, 1, 7, 9, 1, 8, 7, 6, 5, 4, 2, 3 ] */ type Problem2 = [ 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 6, 0, 9, 1, 5, 2, 0, 0, 0, 0, 0, 0, 2, 3, 0, 4, 8, 0, 0, 0, 0, 4, 1, 8, 0, 0, 6, 5, 0, 0, 7, 0, 9, 3, 2, 5, 0, 0, 0, 8, 0, 6, 0, 9, 3, 4, 1, 0, 9, 2, 1, 5, 0, 0, 3, 0, 0, 5, 0, 0, 0, 1, 8, 2, 9, 6 ]; type Answer2 = Solve<Problem2>; /* -> [ 6, 9, 4, 8, 5, 7, 1, 2, 3, 3, 8, 7, 1, 4, 2, 6, 5, 9, 1, 5, 2, 6, 3, 9, 7, 8, 4, 2, 3, 5, 4, 8, 1, 9, 6, 7, 4, 1, 8, 9, 7, 6, 5, 3, 2, 7, 6, 9, 3, 2, 5, 8, 4, 1, 8, 7, 6, 2, 9, 3, 4, 1, 5, 9, 2, 1, 5, 6, 4, 3, 7, 8, 5, 4, 3, 7, 1, 8, 2, 9, 6 ] | [ 6, 9, 7, 8, 4, 2, 1, 5, 3, 3, 8, 4, 1, 5, 7, 6, 2, 9, 1, 5, 2, 6, 3, 9, 7, 8, 4, 2, 3, 5, 4, 8, 1, 9, 6, 7, 4, 1, 8, 9, 7, 6, 5, 3, 2, 7, 6, 9, 3, 2, 5, 8, 4, 1, 8, 7, 6, 2, 9, 3, 4, 1, 5, 9, 2, 1, 5, 6, 4, 3, 7, 8, 5, 4, 3, 7, 1, 8, 2, 9, 6 ] */ type Problem3 = [ 0, 0, 0, 3, 0, 0, 0, 1, 9, 6, 7, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 2, 0, 3, 4, 0, 0, 7, 0, 2, 0, 0, 0, 0, 6, 0, 3, 1, 5, 0, 0, 0, 0, 0, 0, 6, 0, 0, 9, 0, 1, 3, 0, 6, 0, 0, 0, 0, 2, 0, 0, 4, 7, 0, 0, 6, 0, 0, 2, 0, 9, 0, 4, 0, 0, 0, 0 ]; type Answer3 = Solve<Problem3>; /* -> [ 4, 5, 8, 3, 2, 6, 7, 1, 9, 6, 7, 2, 9, 1, 4, 3, 8, 5, 9, 1, 3, 8, 5, 7, 4, 2, 6, 3, 4, 1, 5, 7, 9, 2, 6, 8, 8, 9, 6, 2, 3, 1, 5, 7, 4, 7, 2, 5, 4, 6, 8, 1, 9, 3, 1, 3, 7, 6, 8, 5, 9, 4, 2, 5, 8, 4, 7, 9, 2, 6, 3, 1, 2, 6, 9, 1, 4, 3, 8, 5, 7 ] */
無事数独を解くことができましたね！
Problem2のように答えが複数ある場合は解すべてのunion型が得られます。
また、Problem3のようなヒントの少ない難しい問題でも解くことができました。
最後に
今回使用したコードはこちらで試すことができます。
浦上 真之
2020年度新卒入社エンジニア。
本記事のProblem3を自力で解こうとしたところ15分かけたうえで間違えてしまいました。
フォルシアではフォルシアに興味をお持ちいただけた方に、社員との面談のご案内をしています。
採用応募の方、まずはカジュアルにお話をしてみたいという方は、お気軽に下記よりご連絡ください。
※ 弊社社員に対する営業行為などはお断りしております。ご希望に沿えない場合がございますので予めご了承ください。
