将棋の編入試験の「いいとこ取り」は最長 26 局で十分

問題

将棋の編入試験の受験資格に、「いいところ取りで 10 勝以上、勝率 65% 以上」という基準があります。 プロ棋士でない人が(任意の)プロ棋士と対戦した履歴の中で、勝利が 10 個以上、かつ、勝率が 65% 以上であるような「連続範囲」を切り出すことができれば(=いいとこ取り)、編入試験を受ける資格が得られるというものです 1

この「いいとこ取り」、どうやっていいところを取ればいいでしょうか。 非常に長い連続範囲を切り出すことで条件を満たせる可能性を考えると、どこまで計算すればいいのか自明でないと思います。

つまり、「苦節 20 年、ついに 65 勝 35 敗で編入試験の受験資格を獲得」みたいなニュースはありうるのだろうか、というのが気になっていました。

結論

結論としては、そういうニュースは起きそうにありません。 というのも、編入試験の受験資格を獲得した対戦履歴は必ず次のいずれかの連続を含むからです。

  • 連続 10 局の中で 10 勝 0 敗(= 10 連勝)
  • 連続 11 局の中で 10 勝 1 敗
  • 連続 12 局の中で 10 勝 2 敗
  • 連続 13 局の中で 10 勝 3 敗
  • 連続 14 局の中で 10 勝 4 敗
  • 連続 15 局の中で 10 勝 5 敗
  • 連続 18 局の中で 12 勝 6 敗
  • 連続 20 局の中で 13 勝 7 敗
  • 連続 23 局の中で 15 勝 8 敗
  • 連続 26 局の中で 17 勝 9 敗

つまり、「いいとこ取り」は連続 26 局だけ確認すればよい(それより長い範囲を確認しても無駄)、ということです。

なお、それより長い連続範囲で条件を満たすことはあります。 しかしこのとき、同時に上記のいずれかのパターンも満たしているはずです。

その証明を以下においておきます。

証明

言葉の定義

次のように言葉を定義します。

  • 勝敗結果の連続範囲を切り出したものを「戦歴」と呼ぶことにします。
  • 受験資格を満たす戦歴を「突破戦歴」と呼ぶことにします。A 勝 B 敗の戦歴について、勝数  A \geq 10 かつ勝率  \frac{A}{A+B} \geq 0.65 であるものが突破戦歴です。
  • 中により短い突破戦歴を含まない突破戦歴を「原始突破戦歴」と呼ぶことにします。

主張は、「原始突破戦歴は最長で 26 局」です。

定理:19 勝以上を含む原始突破戦歴は存在しない

A 勝 B 敗の突破戦歴( A \geq 10 かつ  \frac{A}{A+B} \geq 0.65)について、 A \geq 19 の場合、それは原始突破戦歴ではない(その戦歴の中により短い突破戦歴がある)ことを示します。

19 勝以上の突破戦歴を、先頭から 10 勝目までの前半と、10 勝目から終端までの後半に分けます(10 勝目は両方に含める)。

前半の敗北数を b とすると、前半は「10 勝 b 敗」、後半は「(A-9) 勝 (B-b) 敗」となります。

(1)  \frac{10}{10 + b} \geq 0.65 の場合

前半の勝率が 0.65 以上なので、明らかに前半だけでより短い突破戦歴になっています。

(2)  \frac{10}{10 + b} \lt 0.65 の場合

後半だけでより短い突破戦歴になることを示します。  A \geq 19 なので、後半の勝数 A-9 は 10 以上で、勝数の条件は満たしています。 勝率の条件は、 \frac{A-9}{A-9+B-b} \geq 0.65 、すなわち  0.35 (A-9) − 0.65 (B-b) \geq 0 を示せばよいことになります。 この左辺を分解すると

 0.35 (A-9) − 0.65 (B-b) = (0.35 A − 0.65 B) + (0.65 b − 0.35 \times 9)

このとき、

  • 第 1 項は、全体が突破戦歴( A / (A+B) \geq 0.65 、すなわち  0.35 A − 0.65 B \geq 0)なので 0 以上。
  • 第 2 項は、 10 / (10 + b) \lt 0.65 より  0.65 b > 3.5 > 3.15 = 0.35 \times 9 なので正。

よって  0.35 (A-9) − 0.65 (B-b) \gt 0 となり、後半だけで勝率の条件も満たしています。 つまり後半だけでより短い突破戦歴になります。

したがって、19 勝以上の突破戦歴は、その中により短い突破戦歴があると言えます。証明終。

なお一般化して、「いいとこ取りで W 勝以上、勝率 p 以上(W ≧ 2 、0 < p < 1)」という条件の場合、まったく同じ議論で「2W - 1 勝以上の突破戦歴の中には、より短い突破戦歴がある」が言えます。

原始突破戦歴を全列挙する

A 勝 B 敗の突破戦歴について、B を決めたとき、勝率 0.65 以上となる最小の勝数 A は次のとおり(勝数条件 A ≧ 10 も課す)。

  • 0 ≦ B ≦ 5 の場合、A ≧ 10
  • B = 6 の場合、A ≧ 12
  • B = 7 の場合、A ≧ 13
  • B = 8 の場合、A ≧ 15
  • B = 9 の場合、A ≧ 17
  • B ≧ 10 の場合、A ≧ 19

前の定理により 19 勝以上の突破戦歴は原始突破戦歴ではないので、B ≧ 10(A ≧ 19)は除かれ、0 ≦ B ≦ 9 の場合のみ考えれば十分です。

また、最小より勝数が多い戦歴は、より短い突破戦歴を含んでしまいます。 たとえば B = 6 のとき、13 勝 6 敗の戦歴は

  • 最後が勝利の場合、それを取り除いた 12 勝 6 敗が突破戦歴
  • 最後が敗北の場合、それを取り除いた 13 勝 5 敗が突破戦歴

よって、より短い突破戦歴を含みます。 つまり、B = 6 の原始突破戦歴は 12 勝 6 敗だけ。

以上より、原始突破戦歴は次のパターンに限られます(必要性)。

  • 10 勝 0~5 敗
  • 12 勝 6 敗
  • 13 勝 7 敗
  • 15 勝 8 敗
  • 17 勝 9 敗

これらの突破戦歴はすべて「9 連勝、B 連敗、(A-9) 連勝」で具体例を構成できます。 これらの具体例は明らかにより短い突破戦歴を含まないので、すべて原始突破戦歴です(十分性)。

結論としては、最も長いのは 17 勝 9 敗の 26 局となります。

Lean による証明

念のため、Claude Code に Lean で証明しておいてもらいました。

live.lean-lang.org

Lean 何もわからないけれど、Theorem を眺めた限りでは正しそう。

注意:より長い範囲で初めて条件を満たすことはある

誤解しないでほしいのですが、26 局より長い連続範囲で初めて条件を満たすこと自体はあります。

たとえば、○が勝ち、 ●が負けとして

○○○○○○○○○●●●●●●○○●○●○○●○○●○○○

という 29 局は、19 勝 10 敗は勝率 65.5% で、初めて条件を満たしています。

しかしこのとき、最後の 14 局だけに注目すると

○○●○●○●○○●○○○

これは「10 勝 4 敗」のパターンになっています。

このように、27 局以上の範囲で初めて条件を満たした場合、同時に上記のいずれかのパターンも満たしている、というのが上の主張です。

まとめ

将棋のプロ編入試験の受験資格の「いいところ取りで 10 勝以上、勝率 65% 以上」を判定するには、最長で 26 局の連続範囲で条件を満たすものがないかを確認すれば十分であることがわかりました。

より具体的には、プロと対戦するたびに、直近 26 局の結果の中で上記 10 通りのいずれかが発生していないか確認するのがよさそうです。

「苦節 20 年~」みたいなニュースが(意図的に数値を大きく見せようとしない限り)起きなそうなのはちょっと残念。

インターネットで調べてもこういう議論が見つからなかったのだけど、可能性がありそうなアマチュアの間では常識なのかなあ?

余談:フリークラス脱出条件は最長 58 局の戦歴で判定できる

将棋のフリークラス脱出条件のひとつに「30 局連続のいいところ取りで勝率 65% 以上」があります。

勝数ではなく対局数(連続 30 局以上)が指定されているのが、編入試験とちょっと違うところです。 式でいうと、「A 勝 B 敗」の戦歴が A+B ≧ 30 かつ A / (A+B) ≧ 0.65 のとき、フリークラス脱出条件を満たします。

「60 局以上の原始脱出戦歴は存在しない」が証明できます(証明略)。 具体的に原始脱出戦歴を列挙すると、次のようになるようです。

  • 30 勝 0 敗
  • 29 勝 1 敗
  • ...
  • 21 勝 9 敗
  • 20 勝 10 敗
  • 21 勝 11 敗
  • 23 勝 12 敗
  • 25 勝 13 敗
  • 26 勝 14 敗
  • 28 勝 15 敗
  • 30 勝 16 敗
  • 32 勝 17 敗
  • 34 勝 18 敗
  • 36 勝 19 敗
  • 38 勝 20 敗

  1. 編入試験の条件はこれだけではないようですが、今回はこの条件だけに注目します。詳しくは Wikipedia の「棋士 (将棋)」を参照。

グリニッジ天文台はどこにあるとよかった?

経度 0° の本初子午線はイギリスのグリニッジ天文台を基準に決められたもので、世界標準時 (UTC+0) の起点となっています。

ここから東西 15° ごとの合計 24 本が「標準時子午線」と呼ばれます。ほとんどの国・地域はいずれかの標準時子午線を自国の標準時の基準にしています。

日本の標準時 (UTC+9) は東経 135° の標準時子午線に基づいていて、これが兵庫県明石市を通ることはよく知られています。「なんで明石?」と思ったこともありますが、たまたまグリニッジ天文台から 135° 東の位置にあったからです。

ところで、自国の領土に標準時子午線がまったく通っていない国もしばしばあります。有名どころだとオランダ・スイス・イスラエル・ニュージーランド、日本の近くだと韓国などです。まあ、標準時子午線が通っていないことの実用上の困りごとは特にないようですが。

本題

ふと気になりました。もしグリニッジ天文台がもう少し東、または西にあれば、より多くの国・地域が標準時子午線を持てていたんじゃないでしょうか。

確かめたくなったので、ちょっとおもちゃを作ってみました。

Where should Greenwich have been?

mame.github.io

地図を左右にドラッグすると、画面の中央に固定された赤い線 (本初子午線) を任意の経度に合わせられます。これに連動して、何カ国・地域にいずれかの標準時子午線が通っているかが即座に表示されます。地図の下には地域別の国名一覧もあって、カバーされている国は緑、そうでない国は薄い赤で色分けされます。

結論

地球全体に 258 の国・地域 (Natural Earth の 1:10m Admin 0 - Countries 基準) があって、現行のグリニッジ基準だとそのうち 104 か国・地域に標準時子午線が通っています。

もしグリニッジ天文台がいまの位置から西に約 87 km、英国南部のハンプシャーかバークシャーあたりと同じ経度にあったら、109 か国・地域まで増やせていたようです (現行の西経 1.250° を 0° にしたケースに相当)。

逆に、もしグリニッジ天文台がいまの位置から東に約 280 km、北フランス〜ベルギー国境付近と同じ経度にあったとしたら、85 か国・地域にしか通らなくなっていたはずです (現行の東経 3.976° を 0° にしたケース)。グリニッジ天文台が北海上になくてよかった(?)。

つまり、グリニッジ天文台の位置は最適 (109) からマイナス 5 でしかなく、結果的にはかなり最適に近い場所にあったということがわかりました。

AI コーディングエージェントのおかげでどうでもいい疑問を調べるのが大変容易になった。すばらしい時代だなあ。

おまけ 1

グリニッジ天文台をイギリス内で 0.001° 刻みでずらす全探索をしてみたところ、109 が達成される位置はおおよそ 5 つありました。

本初子午線の候補 その場合の日本の標準時子午線
1.332°W 付近 (ニューベリー駅付近) 133.668°E (岡山県倉敷市玉島)
1.316°W 付近 (ニューベリー駅の東 1 km) 133.685°E (岡山県倉敷市船穂)
1.250°W 付近 (サッチャム駅の東 1 km) 133.750°E (岡山県倉敷市中心部)
0.651°W 付近 (アスコット駅の東 1 km) 134.349°E (兵庫県佐用町役場の西 500 m)
0.524°W 付近 (ステインズ駅の西 1 km) 134.477°E (兵庫県相生市役所の東 400 m)

「Most covered」ボタンはどれを選んでもカバー数 109 は同じなのですが、なんとなく 3 番目の西経 1.250° を採用しました。

おまけ 2

グリニッジ天文台を本初子午線に定めたのは 1884 年の国際子午線会議で、他にもいくつかの候補が議論されたそうです。それぞれを 0° に採用していた場合のカバー数は次のとおりでした。

候補 経度 カバー数
ナポリ (伊) 14.26°E 107
ギザの大ピラミッド (埃) 31.13°E 105
グリニッジ (英) 0.00° 104
ベルリン (独) 13.40°E 103
ウィーン (墺) 16.34°E 102
リスボン (葡) 9.18°W 101
フェロ (歴史的・カナリア諸島) 17.66°W 100
ワシントン (米) 77.07°W 100
プルコヴォ (露) 30.33°E 99
ローマ (伊) 12.45°E 98
パリ (仏) 2.34°E 96
カディス (西) 6.21°W 96
コペンハーゲン (丁) 12.58°E 96
エルサレム 35.24°E 96
ストックホルム (瑞) 18.06°E 95
アゾレス諸島 (葡) 25.67°W 92
クリスチャニア / オスロ (諾) 10.72°E 91
ベーリング海峡 (中立案) 169.00°W 89

ナポリだったらもう少しよかったようです。会議の議事録を読むと、フランスは「特定の国を意味しない中立案」としてベーリング海峡やアゾレスを推していたそうですが、地理的中立性は確かに高いものの、カバー数で見ると下位グループに入ります。

なお、言うまでもないですが、1884 年当時は国の数も形もいろいろ異なるので、完全に荒唐無稽な話をしています。

「型システムのしくみ」発売のお知らせ

「型システムの仕組み - TypeScriptで実装しながら学ぶ型とプログラミング言語」という本を書きました。

「型システムの仕組み - TypeScriptで実装しながら学ぶ型とプログラミング言語」
「型システムの仕組み - TypeScriptで実装しながら学ぶ型とプログラミング言語」

どんな本?

簡単な型チェッカを自作してみることで、型システムの仕組みを概観する本です。 型チェックする対象の言語はTypeScript(のサブセット言語)、型チェッカを実装するための言語もTypeScriptです。

たとえば、次のようなプログラムが型チェックできるようになります。

const add = (x: number, y: number) => {
  return x + y;
}

const a = add(1, 2);
const b = a + true;

型チェッカは、それぞれの変数がどういう型を持つか管理しつつ、プログラムの各パートがどういう型になるかを判定していきます。 直感的には理解できても、これを実際に動くプログラムとして書いたことがある人は多くないのではないでしょうか。 本書は、そのような基本的な型チェッカをわずか100行程度の実装からはじめます。

後半では、型チェッカを拡張してオブジェクト型をサポートさせたり、部分型付けを加えたりしていきます。 最後の章では、基本的なジェネリクスを導入します。

ちなみに、上のコードの最後の行では number 型と boolean 型を足しているので、型チェッカは型エラーを報告します。 ただ、このようなケースがなぜエラーとされるのか(型チェッカ開発者の視点でいうと、なぜエラーに"すべき"なのか)という問いは、実は奥の深いテーマです。 本書では、こうした設計上の判断についても丁寧に解説しています。

なぜ書いた?

型システムを本格的に学ぶなら、Benjamin C. Pierce の "Types and Programming Languages"(通称TAPL)が定番です。 TAPLは計算機科学を専門とする大学院生向けの教科書なので、その内容がすばらしいのは言うまでもない(私はTAPLの邦訳版「型システム入門」の翻訳者のひとりです)のですが、対象言語がMLであることや、定理の証明が多く含まれることから、一般のエンジニアや大学生にとってはハードルが高いのも事実です。

そこで本書は、「TypeScriptという親しみやすい言語を使って型チェッカを実装することで、TAPLのエッセンスをわかりやすく学べる」ことを目標に執筆しました。

定理の証明などは省きつつも、型システムの雰囲気はしっかり理解できるように書いたつもりです。 また、本書の内容がTAPLのどの章に対応するかを細かく書いているので、本書を読んだあとにTAPLに挑戦することもできます。

本書の対象読者

  • 型システムに興味があるエンジニア
  • プログラミング言語に興味を持ち始めた学生
  • TAPLを読もうとしたが挫折した人
  • TAPLの輪講・勉強会をしたいが、教師役が見つからない人たち
  • 実際に手を動かしながら型システムを学びたい人

「抽象構文木とは?」というレベルから説明しているので、言語処理系というものをはじめて学ぶ人にも読めると思います。

一方で、部分型付け・再帰型・ジェネリクスなどにも踏み込んでいます。 これらの言語機能をユーザ視点で知っていても、その型チェックを実装するとなると、より深い理解が必要になります。 そのため本書は、これらの言語機能について一般的なTypeScriptの入門書では踏み込まないであろう領域まで非常に詳しく説明しています。 そのため、ある程度経験のある方にも楽しんでいただけると思います。

本書の構成

本書は、型システムの基礎から発展までを順を追って学べるようになっています。

  • ベースとなる基本的な型チェッカ(1~4章)(TAPLでいうと、単純型付きラムダ計算相当)
  • オブジェクト型・再帰関数の拡張(5~6章)
  • 部分型付け(7章)
  • 再帰型(8章)
  • ジェネリクス(9章)

各章では、TypeScriptのサブセットを対象に型検査器を実装しながら進めるので、手を動かしながら学ぶことができます。

型検査の対象はTypeScript(のサブセット)、型検査器の実装に使う言語もTypeScriptです。なるべく平易なTypeScriptで書いていますし、少し高度な機能を使う場面では都度解説を入れているので、そこまでTypeScriptに詳しくなくても読めると思います。

また、TAPLに登場する面白い概念について、TypeScriptを使って解説するコラムをたくさん用意しているので、そのあたりも楽しんでいただけるのではと思います。

執筆の裏側

本書は、n月刊ラムダノート Vol.4 No.3 (2024)に寄稿した「TypeScriptではじめる型システム」という記事を発展させたものです。そのときに書いた記事もご参照ください。

mametter.hatenablog.com

n月刊の記事では単純型付きラムダ計算相当の言語しか扱いませんでしたが、本書ではよく使われる言語拡張(オブジェクト型や部分型付けなど)をもろもろ扱っています。

また、TAPLの翻訳者からTypeScriptの専門家まで、多様で心強いレビュアー陣にたくさん指摘をいただいた(ありがとうございます!)ので、既刊部分も含めてかなり読みやすくなっていると思います。

注意

本書は、TypeScriptの型システムを詳しく説明する本ではありません。 あくまでTypeScriptを題材として、TAPL流の古典的な型システムを解説する本です。

TypeScriptの型システムは、古典的な型システムにたくさんの拡張を加えた、発展的なものになっています。 それを一冊の本として説明するのは(少なくとも私には)不可能です。 本書やTAPLを読んだうえで、論文やTypeScriptの実装を読んでいくしかないのではないかと思います。

TypeScriptの主な拡張の論文を集めた記事にリンクをはっておきます。

blog.miz-ar.info

まとめ

「型システムのしくみ」は、TypeScriptを使って型システムを実装しながら学ぶ本です。 TAPLのエッセンスを噛み砕いて紹介しており、初心者でも読みやすく書いているつもりですが、上級者にもきっと発見があります。

型システムに興味を持ち始めた方に、ぜひ手に取っていただきたい一冊です!

TypeScriptは型安全じゃないからすばらしい

「TypeScriptではじめる型システム」という記事をn月刊ラムダノートに寄稿しました。

どんな内容?

TypeScriptの極小サブセットに対する型検査器を書き、それを通して型システムを体感してみよう、という内容です。

詳しく言うと、boolean型とnumber型と関数型しかないTypeScriptサブセット言語がターゲットです。 型検査器の実装言語にもTypeScript(処理系はDeno)を使います。 TypeScriptづくしの一品です。

わかる人向けに言うと、「型システム入門」という本(通称TAPL)の単純型付きラムダ計算に相当する内容をTypeScriptで説明してみた、ただし定理や証明はすべて省いた、という感じです。

なぜ書いた?

きっかけがいくつかありました。

TypeScript界隈でTAPLが読まれているらしいと聞いた

もともと、型システムを実務プログラマ向けに説明する記事を書いてみたいという気持ちはずっとありました。 TAPLは情報科学専攻の大学院生向けの教科書なのですが、型システムというキャッチーな内容から、実務プログラマにも注目されています。 しかしTAPLは、あまり実務で見かけないMLという言語で説明されている上、定理と証明が紙面の半分くらいを占めているので、「途中で脱落した」「型システム入門入門が欲しい」という話をよく聞いていました。

TAPLを翻訳したのは12年も前のことですが、今年になって急に、日本のTypeScript界隈でTAPLを読んでいる人たちが結構いるらしいと小耳にはさみました。 それも複数の経路で同時多発的に。 そのうちのひとつでは、TAPLの訳者として声をかけていただき、トークさせてもらいました。

これで、「いまこそ記事を書くべきなのでは?」という気分が高まりました。

TypeScriptの裏側を調べてみたかった

もうひとつの動機としては、TypeScriptの設計方針や型検査器の実装を少し真面目に理解してみたいと思ったことです。 私はTypeProfというRubyの型解析器を開発してます。

github.com

TypeProfを作るうえで、TypeScriptはいろいろ参考にしてます。 ただ、TypeScriptのユーザとしての体験は多少知っているつもりですが、裏側を真面目に見たことはなかったので、ここらで少しだけきちんと調べておきたいと思っていたのでした。 この執筆は、そのきっかけにもなりました。

TypeScriptは型安全じゃない?

そうして調べているうちにわかったのですが、TypeScriptはとてもいい意味で「雑」に作られているということがわかりました。 これは、漸進的型付けがどうこうという話ではなく、もっと全体的な設計・実装方針の話です。

TypeScriptが見逃すエラー

典型的な例としては、次のような未初期化変数の参照をするプログラムが型エラーになりません。

型検査器がこのような見逃しをする場合、型安全性があるとは言わないのがふつうだと思います。 これはTDZ(Temporal Dead Zone)と呼ばれるJavaScriptの仕様なので、ちょっと考えてみると、JavaScriptの構文を保ったまま解決するのはむずかしそうです。 実際、TypeScriptにissueがあがっていますが、「めったに出てこないケースなので気にすんな」ということでWontfixとなってました。

他にも、「全然関係ない変数宣言を削除すると、出るべきエラーが消えてしまう」という、かなり理解不能な挙動をする例も作れてしまいました。

この挙動の私の理解ですが、TypeScriptの型検査器はヒューリスティック再帰を打ち切るところがたくさんあって、そのせいだと思います。つまりこの例は、ジェネリック型の展開打ち切りの閾値ぎりぎりのところに型エラーがあって、8行目の型判定を先にやっておくと判定結果がメモ化されることで探索範囲がぎりぎり型エラーに届くけど、8行目がないと型エラーまでの探索が深くなりすぎて打ち切られる、みたいな感じなのかなと思ってます。

ちなみに、TypeScriptが本当に型安全でないかは、型安全の定義によります。JavaScriptにトランスパイルされるので、未定義動作に陥ることは原理的にないから、「TypeScriptは何もしなくても型安全だ」という主張もふつうにありえます。このへんは記事のコラムにいろいろ書いたので参照ください。

それでもTypeScriptはよいもの

「雑」「型安全じゃない」というと、TypeScriptを悪く言っていると思われるかも知れませんが、まったく逆です。

現実問題として、TypeScriptが便利であることに異論を挟む人は少ないと思います。 JavaScriptは控えめに言っても(動的型付け云々以前に)いろいろと厳しい言語だと思うのですが、TypeScriptはJavaScriptのハンデを負ってなお便利なので、文句なくすごいです。

型システムに詳しい人は型安全性を気にしがちなのですが、TypeScriptは「別に全部の型エラーを検出できなくてもよい(型安全じゃなくてよい)」という思い切った割り切りをしています。 それでいて、「現実的によくあるバグは大体検出できて便利」という絶妙なバランスを達成しています。

ちなみに、ちょうどkmizuさんがほぼ同じようなことを言ってました。

TypeScriptの設計者の言葉

Anders Hejlsberg自身が、次のように言っています。

If you can't achieve perfection then you don't even try to go there and that means you cut out a whole bunch of possible things that you could do that you might not be able to prove soundness for, but we don't have that restriction and that actually makes our work very interesting because we can go in places where people typically don't go.

雑な意訳:型の研究者は型安全性が証明できそうにないことと試そうともしないので、実はいろいろできることを切り捨ててしまっている。TypeScriptにはそういう制約がない。そのおかげでわれわれは、他の型研究者がふつうは行かない領域に踏み込めるので、とても面白い仕事ができている。

www.youtube.com

これ、型の研究者には結構辛辣ですね。

個人的には、「ぜんぜん型安全じゃなくても便利な型解析器」は実際に存在できるんだというのが確信できてよかったです。 TypeProfもそういうところを目指していて、実現できるのか自分でも半信半疑でやっているのですが、達成した実例があるというのは心強く感じました。 TypeProfがそのクオリティとバランスを目指したいものです。

記事について雑多なこと

パーサはどうした

TypeScriptサブセットの型検査器を作るためにはパーサが必要だったのですが、その書き方を解説していると日が暮れるので、あらかじめ用意しておきました。

https://github.com/LambdaNote/support-ts-tapl/blob/main/utils.ts

eslintで使われているtypescript-estreeをラップする感じで作ってます。

TypeScriptプロジェクトのよい書き方がわからなかったので、とりあえずDeno専用になってます。 TypeScriptに詳しい人がみたら変な感じになってそうなので、適当にPRくれるとうれしいです。

Rubyじゃないのはなぜ

Rubyの型の開発に参加している立場でありながら、Ruby + RBSを記事の題材にしなかったのは、上に書いた動機のとおりなのですが、さらに技術的な理由として、Rubyでは無名関数が第一級の言語機能じゃないからです。 TAPLベースの型システムを説明したいという記事の方向性には、無名関数が必要でした。 もちろんProcはありますが、defを使わずにProcだけでプログラムを書くのはふつうのRubyじゃなさすぎるので。

続きが読みたい

単純型付きラムダ計算で終わっているので、人によっては「これで終わり?」って思うかもしれません。 basic.tsは部分型付け、型エイリアスジェネリクスなどを付け足していくための土台になっています。 今回の反響がよければ、それらで言語拡張するという続きを出せたらと思っています。

追記: この記事をもとに本を書きました! 実際に、部分型付け、再帰型、ジェネリクスを追加した内容になっています。詳しくは↓

mametter.hatenablog.com

RubyでSlackのボットを書く方法(なるべく自力で)

RubyでSlackのボットを書くには、slack-ruby-client gemruboty gemなどを使うのが一般的だと思います。 しかし個人的には、Slackボット程度でgemを使うのは好みでないので、なるべく素のRubyだけで書くようにしています。 その方法をまとめておきます。

Slack appを登録する

まず、https://api.slack.com/appsで"Create New App"して、適当に設定をします。

次のYAMLを"App Manifest"に貼ってSave Changesすると一気に設定できます。

display_information:
  name: Sample Slack App
features:
  bot_user:
    display_name: Sample Slack App
    always_online: true
oauth_config:
  scopes:
    bot:
      - app_mentions:read
      - chat:write
settings:
  event_subscriptions:
    request_url: https://example.com/
    bot_events:
      - app_mention
  org_deploy_enabled: false
  socket_mode_enabled: false
  token_rotation_enabled: false

かんたんに説明すると、メンションされたときに通知を受け取る(app_mentions:read Scopeとapp_mention Event Subscription)、チャンネルで発言する(chat:write Scope)、という設定です。

なお、メンションではない発言も全部受け取りたかったらchannels:history Scopeとmessage.channels Event Subscriptionを足すとよいです。

ボットからSlackにメッセージを送る

chat.postMessage APIを叩くだけです。 標準ライブラリだけで簡単にできます。

require "net/http"
require "json"

TOKEN = "xoxb-..."    # Bot User OAuth Token を埋める
CHANNEL = "CXXXXXXXX" # Channel ID を埋める

resp = Net::HTTP.post_form(
  URI.parse("https://slack.com/api/chat.postMessage"),
  {
    token: TOKEN,
    channel: CHANNEL,
    text: "Hello",
  }
)

json = JSON.parse(resp.body, symbolize_names: true)
pp json[:ok]  #=> true on success, false on failure

必要な設定は2つです。

  • Slack appの設定画面の"OAuth & Permissions"からBot User OAuth Tokenをコピーして、TOKENに入れる
  • 発言したいSlackチャンネルの"View channel details"の最下部にあるChannel IDをコピーして、CHANNELにいれる

そうしてコードを実行すれば、発言できるはずです。

ボットから発言した様子

ここでは単純に"Hello"というテキストを送っていますが、text: "Hello"の代わりに次のようなものを書けば、Slackのmarkdown風のマークアップができます。

{
  blocks: [
    {
      type: "section",
      text: {
        type: "mrkdwn",
        text: "*Hello* `world`"
      }
    }
  ]
}

このあたりについて詳しくはReference: blocksをご参照ください。 Block Kit Builderインタラクティブに構築することもできるようです。

Slackからイベント通知を受け取る

Slackから「メンションされた」や「誰かが発言した」などのイベントの通知を受け取るには、Events APIを使います。

2024年現在、Events APIには2種類の通信方法があります。

  • publicなHTTPサーバを立てて、HTTPリクエストとして通知を受け取る
  • WebSocketでSlackに接続し、プッシュ通知を受け取る(Socket Mode

両方かんたんに説明します。

HTTPサーバを立てる方法

sinatra gemでHTTPサーバを書きます。gemですが、sinatraは自分の心の許容リストに入っているのでOKとしています。

require "sinatra"
require "json"
require "openssl"

SIGNING_SECRET = "..." # Signing Secret で埋める

def verify_signature(timestamp, body, sig_actual)
  msg = ["v0", timestamp, body].join(":")
  sig_expected = "v0=" + OpenSSL::HMAC::hexdigest(OpenSSL::Digest::SHA256.new, SIGNING_SECRET, msg)
  OpenSSL.secure_compare(sig_actual, sig_expected)
end

post "/" do
  body = request.body.read

  # Slack からの POST であることを検証する
  halt 401, "{}" unless verify_signature(
    request.env["HTTP_X_SLACK_REQUEST_TIMESTAMP"],
    body,
    request.env["HTTP_X_SLACK_SIGNATURE"]
  )

  json = JSON.parse(body, symbolize_names: true)

  case json[:type]
  when "url_verification"
    # Slack に URL を登録するときのイベント、challenge をそのまま返せば良い
    json[:challenge]

  when "event_callback"
    event = json[:event]

    case event[:type]
    when "app_mention"
      # メンションされた
      p event[:text]
    end
    ""

  else
    ""
  end
end

必要な設定は1つだけです。

  • Slack appの設定画面の"Basic Information"の"App Credentials"からSigning Secret(hexで32桁)をコピーして、SIGNING_SECRETにいれる

このサーバをインターネットからアクセスできるところで実行します。 実験ではngrokなど使うとよいかもしれません。

$ ruby ~/bot-server.rb
...
== Sinatra (v4.0.0) has taken the stage on 4567 for development with backup from WEBrick
[20XX-XX-XX XX:XX:XX] INFO  WEBrick::HTTPServer#start: pid=XXXXXX port=4567

そして、"Event Subscriptions"のRequest URLで、立てたサーバのURLを入力します。 うまく行けば"Verified"となります。

URLの設定に成功した様子(Verified)

Slackでボットに対して@Sample Slack Bot Helloなどとメンションしてみましょう。 うまく行っていれば、HTTPサーバの方に発言内容が出ているはずです。

"<@XXXXXXXXXXX> Hello"
XXX.XXX.XXX.XXX - - [XX/XXX/20XX:XX:XX:XX +0900] "POST / HTTP/1.1" 200 - 0.0064

Socket Modeを使う方法

Socket Modeは、RubyからWebSocketでSlackに接続してプッシュ通知を受け取る方法です。 publicなHTTPサーバを用意しなくてよいので、運用は手軽かもしれません。

残念ながら、RubyでgemなしでWebSocketクライアントを使うのは大変です。いろいろ調べましたが、満足できる方法はみつけられませんでした。

調べたこと(クリックしたら詳細表示)

WebSocketプロトコルを扱うwebsocket gemはよくできていて、依存もゼロなので好みです。

ただ、実際に通信するgemとなると、eventmachineだったりfaradayだったり、巨大なgemに依存しがちです。

その点websocket-client-simple gemは、その手のものに依存しないクライアントというコンセプトは好きなのですが、細かいところで気になることが多かったです *1 。これを好みに合わせて直すくらいなら、Slackボットに特化したかんたんなものを自作するかって気分になりました。

net/httpがWebSocketをサポートしてくれたらいいのになあ。

ということで、あきらめてwebsocket gemのみに依存するslack_socket_mode_botというgemを作りました。それを使う例だけ示しておきます。

require "slack_socket_mode_bot"

SLACK_BOT_TOKEN = "xoxb-..."
SLACK_APP_TOKEN = "xapp-..."

bot = SlackSocketModeBot.new(token: SLACK_BOT_TOKEN, app_token: SLACK_APP_TOKEN) do |data|
  if data[:type] == "events_api" && data[:payload][:event][:type] == "app_mention"
    event = data[:payload][:event]

    p event[:text]
  end
end

bot.run

必要な設定は3つです。

  • Slack appの設定画面の"Socket Mode"でEnable Socket Modeを有効にする
  • Slack appの設定画面の"OAuth & Permissions"からBot User OAuth Tokenをコピーして、SLACK_BOT_TOKENに入れる(`xoxb-で始まるもの)
  • Slack appの設定画面の"Basic Information"の"App-Level Tokens"を作って、SLACK_APP_TOKENにいれる(xapp-で始まるもの)

あとは、このコードを実行するとSlackと通信し始めます。

$ ruby bot.rb

Slackでボットに対して@Sample Slack Bot Helloなどとメンションしてみましょう。 うまく行っていれば、発言内容が通知され、pで出力されるはずです。

"<@XXXXXXXXXXX> Hello"

ちなみに、Socket ModeのWebSocketはあくまでイベント通知を受け取るためだけのものであり、これを経由してchat.postMessageなどのAPIを呼ぶことはできません。 slack_socket_mode_botでは、SlackSocketModeBot#call(method, data)というAPIを呼ぶ方法もおまけで付けておきました。

まとめ

なるべくgemに頼らずにRubyでSlackのボットを書く方法を説明しました。 ここで述べた方法は、Ruby開発者のSlack workspaceで動くボットたちで長期間運用しています。

techlife.cookpad.com

もちろんslack-ruby-client gemなどを使うのがかんたんだと思うし、抵抗がないならそれが賢いと思います。 ただ、slack-ruby-client gemはSlack社謹製ではないので、たとえばまだSocket Modeに対応していないようです。

なぜgemに頼らないかというと、依存を減らしたいという個人的な好み(いわゆるNot Invented Here症候群かも)が最大の理由ですが、Slackはわりと頻繁にAPIを仕様変更するので、多少面倒でもSlack公式のAPIを直接叩いておくほうが長期的にはメンテナンス性が高いのでは? と思ったり思わなかったり。

変更履歴

  • 06/24 22:00 OpenSSL.secure_comparehalt 401, "{}" を使うようにした(thanks @sora_h)

*1:websocket gem以外にも依存があるところ、内部的にThreadを作っているところ、ソケットを1文字ずつ読み込んでいるところ、pingフレームを処理してくれないところ、などなど。

継承はなんでダメ?

オブジェクト指向の継承を使うな」という主張が広まっているようです。なんでダメになったんでしょうか。

インターネットで見かけた「継承はダメ」という主張をいくつか眺めて、友人と議論しつつ、考えてみました。

「コードが読みにくくなる」

継承があると、メソッド呼び出しが実際にどのメソッド定義を呼び出すのか字面でわからない。 デバッガを使って、親クラスのメソッドに飛んだり、子クラスに飛んだりするのを追いかけないと行けない。 つらい。という主張。

めっちゃわかる。わかるんですが、これは「高度に共通化されたコードは読みにくい」という一般的な側面がかなり大きいような。 たとえば継承の代わりに高階関数を使うと、関数呼び出しがどのクロージャに飛ぶか字面でわからなくなる。 ひどいとコールバック地獄になって何が何やらになります。

継承がことさらにまずい理由を想像すると、すべてのメソッド呼び出しがポリモーフィックになりうるのは、読みにくさを増してるかも。 高階関数なら、高階関数の呼び出しだけ注意すればよいから。C++ の virtual キーワードは正しかったのだ(?)。

そういえば「インターフェイスの継承は良いが、実装の継承はダメ」という派閥も見かけますが、この問題はあまり変わらなそうです。 なんなら、飛び先の候補が「親子クラスだけ」から「インターフェイスを実装した全クラス」になるので、悪化する可能性も。

「すぐ神クラスになる」

基底クラスについつい便利メソッドを生やしてしまい、気づけば便利メソッドを寄せ集めた「神クラス」になっている。 その便利メソッドたちは、誰が使ってるかわからないので、変更できなくなってしまう。 つらい。という主張。

前半(寄せ集め)はややわかる。 コンポジション等で切り出そうと思っても、既存のインスタンス変数にアクセスする必要があったりすると、ついついインスタンスメソッドにしてしまったり。 インスタンスメソッドが暗黙的に this/self を受け取り、容易にインスタンス変数にアクセスできてしまうのは、継承が強力すぎるせいといえる気はします。

ただ、「神クラス」を作ってしまう者は、継承を禁止すると、すべてを詰め込んだ単一「神モジュール」を育成させたりしないのかな。

後半(変更できなくなる)は、コード共通化そのものの問題で、継承以外でも起きる気がします。 いろんなところから使われているコードを変更するのはどうしたってしんどい。 関数で切り出しても、mix-in にしても、コンポジション・委譲で切り出しても、それは本質的にはかわらない。

継承だと特別しんどくなる理由があるだろうか。あまり思いつかなかった。 それこそインスタンス変数のアクセス性確保のために、切り出しがむずかしい面はあるかなあ?

「変な継承をする人がいる」

コードを再利用するためだけに、親子関係とは言えない継承をしてしまうプログラマがいる。 愚かものが悪用してしまう継承は禁止すべきだ。という主張。

幸い、意図的にそんなことをするプログラマは身近にいないので、最初はピンときませんでした。 でも、そういう継承関係が生まれるシナリオは思いつきました。

  • もともと Clock というクラスでアナログ時計を実装していた。
  • デジタル時計も実装したくなった。
  • Clock を基底クラスにし、AnalogClock クラスと DigitalClock クラスを派生させるとよさそう。
  • と思ったが、すでにいろんな人が new Clock() している。全部 new AnalogClock() に書き換えてもらう? うーん……
  • 互換性を重視して、やむなく DigitalClock extends Clock で妥協する。
  • 「デジタル時計がアナログ時計を継承する」という結果だけ見た人は、書いた人をバカだと思ってしまう。

ということで、互換性の配慮などの事情で、奇妙な継承関係は確かに生じうる。というか、身に覚えもある。

ただ、これは継承以外でも普通に起きる。 アナログ時計を作る create_clock() という関数を公開しちゃうと、後から create_analog_clock() にするのは大変。 未来のユーザは「なんで create_clock() がアナログ時計なの、バカなの」って思うのかもしれません。

(時計の例がしっくりこない人は、モノクロテレビ・カラーテレビとか。レトロニム一覧から好きな例を選んで読み替えてください)

継承がことさらに問題だとしたら、後知恵だと良い設計が見えやすく、そうなっていないことが気になりすぎるのかも。 関数なら「はいはい」って流せるけど、オブジェクト指向はドグマになっていて、奇妙な設計を見ることに耐えられない。 でもそれで継承自体を禁止しようというのは、もはやオブジェクト指向への偏執的な愛情って感じがしますね……。

まとめ

「継承はダメ」という理由で、ある程度共感したのはいまのところ2つ。

  • すべてのメソッド呼び出しがポリモーフィックになりうるので、どこに飛ぶか常に注意が必要で、コード読解が大変(いまどきならエディタ支援でなんとかならんかな)
  • 暗黙的に this を受け取るインスタンスメソッドは便利すぎて悪用しやすく、寄せ集めの「神クラス」につながりがち(ただ、継承禁止で本当に解決するかはわからない)

「継承の問題はそんな些末なことじゃない! もっと大きい問題だ!」という人がいたら、ぜひやさしく教えて下さい。

ブラウザでRubyを動かす夢

何に使うわけでもないけど、とにかくブラウザで Ruby を動かしたかったんです。

その夢が、ついにかなった気がします。

振り返ってみると、ここに来るまで 6 年もかかったようです。ちょっと嬉しくなったので経緯を書き残します。

EmscriptenRuby をビルドする

2018 年、ふと思い立って、EmscriptenRuby をビルドできるようにしました。

Emscripten は、要するに C/C++ プログラムを JavaScript や Wasm に変換してくれるコンパイラです。C で書かれた RubyEmscripten でビルドすれば、ブラウザで動く Ruby が作れるはず。

意外と微修正だけで miniruby *1 がビルドできて、簡単なコードなら動かせるようになりました。

mametter.hatenablog.com

安定した Emscripten'ed Ruby をメンテナンスする

ただ、ちょっと凝ったコードを走らせると落ちたり刺さったりして、まともに使えるクオリティにはできませんでした。また、RubyEmscripten も変わっていくので、しばらくしたらビルドできなくなってしまいました。

しょうがないので放置していたら、kateinoigakukun さんっていうスーパーハッカーがさっそうと現れて、Ruby の Wasm/WASI 対応をはじめてくれました。RubyKaigi 2022のキーノートは記憶に新しいですね。

rubykaigi.org

kateinoigakukun さんは自分と違って Wasm にちゃんと超詳しいので、不安定な挙動に対して場当たり的に対応するのではなく、まじめに根本原因を調べて改善することをやってくれました。また、ビルドシステムのメンテナンス力も高く、Wasm/WASI Ruby の nightly ビルドを配布してくれるようになりました。

github.com

katei さんの興味は WASI *2 のはずですが、なぜか Emscripten ビルドも提供してくれました。このおまけにより、そこそこ安定的な RubyEmscripten ビルドを無料で得られるようになったのでした。最高。

Emscripten プログラムを xterm.js につなぐ

ブラウザで Ruby が動くようになったので、いくつかアプリを書けました。楽しい。

ruby-puzzles-2022.cookpad.tech mame.github.io

ただ、別に Ruby でブラウザアプリが書きたかったわけではないんですよ。やっぱり REPL を動かしたい。何に使うわけでもないけど。

そのためには、ブラウザで動く端末につないで irb を動かさなきゃいけない。ブラウザで動く端末エミュレータには xterm.js があり、これは vscode でも使われている超安定ライブラリなので、あとは Emscripten'ed Ruby とつなぐだけでした。

これがまた大変でした。

Emscripten プログラムに限らないのですが、端末エミュレータとプログラムは通常、直結していません。Linux でも、C プログラムが printf("Hello\n"); とやると、端末エミュレータには Hello\r\n という文字列が渡されます。\r が挿入されていることに注意。これを挿入するのは、プログラムでも端末エミュレータでもなく、実は Linux カーネルです。Line discipline という機能がそれです。*3

xterm.js で Linux プログラムを動かす場合、node-pty という定番ライブラリがあり、vscode などもこれを使っているようです。が、これは Linux の pty のラッパなので、ブラウザでは動きません。Emscripten のために、ブラウザの上で動く pty がほしいという声はちらほらあるようでしたが、作った人はいないようでした。

ないなら作るかってことで、xterm-pty という Emscripten プログラムとつなぐための xterm.js アドオンを作りました。

github.com

これは要するに Line discipline を気合で実装したものです。ブラウザで Ruby を動かしたいと思ったら、いつのまにか Line discipline を JavaScript で実装していた。

まあ、xterm-pty で Vim が動いたときはなかなかの達成感でした。Vim のデモは↓を参照。

xterm-pty.netlify.app

なお、Vim を Emscripten すること自体は既出でした。あちらは Vim に特化したレンダラを自作したのに対し、こちらは xterm.js とつないで動かしたところが新規性。汎用的なので Vim 以外の CUI プログラムも動きます。詳しくはデモを参照。

xterm-pty をまともにする

で、irb を動かすために作った xterm-pty でしたが、実際に irb と満足につなぐには課題がありました。

Line discipline は、IO のやり取りだけでなく、シグナルを投げる役割もあります。Ctrl+C が押されたときに SIGINT を投げるのは、実は Line discipline です。しかし Emscripten プログラムにはシグナルという概念そのものがなかったので、投げようがありませんでした。

また、xterm-pty と Emscripten プログラムとつなぐ部分が極めて不安定でした。Emscripten ランタイムをモンキーパッチして read/write/select などのシステムコールインターセプトしていたので、Emscripten がちょっと変数名を変えると動かなくなる。

そんなわけで、しょうがなく放置していたのですが、なんか Ingvar Stepanyan っていう Emscripten に超詳しいスーパーハッカーがさっそうと現れて、「Emscripten にシグナルを実装した」「モンキーパッチでなく Emscriptenプラグイン的に xterm-pty を使えるようにした」と言う、ほとんど作り直しに近い PR をくれたので、突如解決しました。最高。

github.com

ついに Ruby の REPL がブラウザで動く

刷新された xterm-pty をリリースしたので、組み合わせて irb を動かしてみたら、なんと一切のパッチを必要とせずに動きました。すごい、すごすぎる。6 年前と比べると別世界。

補完も出るし、イースターエッグのアニメーションも動きます。

twitter.com

いやー、これが見たかったんですよ。夢がかなった瞬間。何に使うわけでもないけど。

まとめ

ブラウザで Ruby を動かす夢がかないました。かなったんじゃないかな。

まあ、Thread.new が動かないとか、拡張ライブラリをロードできないとか、まだまだ課題はあるわけですが。

適当なものを作って放置してたらスーパーハッカーたちが直してくれる人生だったので、さらなるスーパーハッカーの登場を待ちたい。

おまけ

実は、kateinoigakukun さん自身が irb.wasm をやっています。

irb-wasm.vercel.app

これは Emscripten ではなく WASI で実現されています。

irb.wasm は jquery-terminal を使っているそうで、補完などは出ません。が、RubyWorld Conference 2022 で picoruby/picoirb を発表してた hasumikin さんに相談したら irb.wasm で xterm.js を使うモードを実装してくれたので、そっちなら補完が出ます。ただ、pty をまじめに模倣しているわけではなく、irb や reline にモンキーパッチをあててどうにかしているようなので、再現性はやや微妙かも。たとえば例のイースターエッグは(まだ)動かなかった。irb.wasm で xterm-pty を使うようにするとよさそうだけど、できるのかな?

*1:Ruby のビルド時に中間的に作られる簡易な Ruby インタプリタ。拡張ライブラリがロードできないなど、制限がある。

*2:WASI は、Wasm のポータブルなシステムインターフェイスEmscripten がブラウザ特化の Wasm を出力するのに対し、WASI に基づいた Wasm はブラウザだけでなく配布用実行ファイルやエッジコンピューティング環境などで共通して使える。

*3:pty とか termios とかのキーワードのほうがわかりやすいかも。pty は Line discipline で繋がれたマスター・スレーブのペアで、termios はスレーブ側から Line discipline を制御するための API 、だと思ってますが、正確な定義は自信ない。