2025年度振り返り
ここ数年、理論系に軸足をおいて研究を進めてきていますが、 それ以外のところでも、 ぼくの予想を裏切る形でいろいろな新しい動きが出てきていて嬉しい限りです。 理論系では control/prompt および shift0/reset0 で大きな進展がありました。 また、教育系では何と言っても OCaml Blockly の新実装でしょう。 それぞれについて、詳しく見ていきます。限定継続演算子の研究
研究室では、限定継続演算子の CPS 変換の正当性、および reflection の証明を行ってきていますが、今年度は並行して限定継続演算子の small-step の意味論と big-step の意味論をつなぐ研究を進めました。 この研究の動機は、最近、提案した control/prompt および代数的効果とハンドラの新しい CPS インタプリタがこれまでの CPS インタプリタと等価かどうかを small-step の意味論に変換することで確かめようというものでした。 その等価性は無事に示されたのですが、 同時にそれが CPS 変換の正当性や reflection の証明にも貢献しそうなことがわかってきました。control/prompt に対する新しい CPS 変換
昨年度、control/prompt の CPS 変換の正当性の証明を行ったのですが、 そこには論理関係というかなり大掛かりな道具立てが必要でした。 このままでは、正当性は示せたとしても、一歩進んだ reflection の証明を行うのは大変です。 そこで今年度は control/prompt に対する新たな CPS 変換を提案しました。 従来の CPS 変換は継続とトレイルが常に独立して現れていましたが、 この表現はトレイルが継続の列であるという直感を表現してはいません。 そのため、その直感を論理関係を使って保証してあげる必要がありました。 一方、新しい CPS 変換では、この直感を直接、 CPS 変換に埋め込む形で表現しました。 これにより、トレイルが継続の列であることが常に明らかとなり、 CPS 変換が等価性だけでなく簡約も保存することを示すことができました。 この性質は reflection を証明する際の大きな一歩となります。
CPS 変換の簡約の保存を示すにあたって重要だったポイントは、 継続の列が結合則を満たすことです。 直感的には、トレイルは継続の列なわけですが、 実際には継続もトレイルも高階関数で表現されています。 そのため、３つの継続 k1, k2, k3 があった時に (k1 @ k2) @ k3 と k1 @ (k2 @ k3) が等しいかどうかは明らかではありません。 これらが等しいことを保証することで、 CPS 変換の簡約の保存を証明することができました。
振り返ってみるに、どうやら一見すると当たり前のような継続の列の結合則が control/prompt の本質のようです。 4 年前に 4 種の限定継続演算子に対する抽象機械を設計した時も、 継続を線形化する部分が鬼門でした。 さらに、今年度 control/prompt に対する small-step の意味論と big-step の意味論をつなぐ際にも、 やはりこの継続の線形化が最も苦労させられたところでした。 でも、control/prompt のもともとの直感は、 すでにスタックに存在する継続に捕捉した継続をつなげるところです。 そうすると、 この新しい CPS 変換はその直感を最も自然に表現しているように感じられます。
shift0/reset0 の Reflection の証明
control/prompt の実装にはトレイルを使うわけですが、shift0/reset0 の実装にはメタ継続が使われます。 両者は 4 種の限定継続演算子の独立した 2 軸を形成していて、両者、 それぞれを理解することが 4 種の限定継続演算子を制覇するには必須です。 今年度は shift0/reset0 の研究も大きく進みました。
shift0/reset0 については、Biernacki らのグループが研究を進めており、 CPS 変換の正当性のみならず reflection の証明まですでになされています。 ところが、彼らの仕事は微妙に使用している限定継続演算子の定義が異なる上に、 reflection を証明する手法もかなり特殊です。 一方、我々のグループでは 4 種の限定継続演算子を統一的に扱い、 いずれは共存できることまで目指しています。 そこで、すでに存在している shift/reset に対する reflection の証明をもとに、それを素直に shift0/reset0 に拡張することで shift0/reset0 の reflection の証明を試みました。
実際に行ったのは、 まず CPS 変換の一種であるコロン変換を定義することからです。 コロン変換というのは、CPS 変換の結果が煩雑になりすぎないように適宜、 最適化を入れながら行う CPS 変換です。 これまで shift/reset に対してはそのような変換が知られていましたが、 コロン変換については Biernacki らのかなり特殊なものしか知られていませんでした。 そこで、我々は Danvy, Nielsen による系統的な手法を採用し、 まずは shift0/reset0 の定義から自然に導かれるコロン変換を定義しました。
このようにして得られたコロン変換に対して reflection の証明を行います。 直感は shift/reset に対する reflection の証明を CPS 変換して、 メタ継続が存在する状態で同じ証明を行うというものです。 考え方は簡単なのですが、実際にやってみると一筋縄ではいきません。 最も重要だった点は、各式の継続 k が 継続に存在するのかメタ継続に存在するのかを区別するところです。 普通、各式の継続 k は末尾の位置の継続に現れます。 しかし、reset で継続が区切られるとメタ継続に押しやられてしまいます。 このふたつの場合を適切に表現して対処してあげることで、 CPS 変換とその逆変換が簡約を保存することを示すことができました。 これらが示せると reflection の証明まであともう少しという感じです。
代数的効果とハンドラ
今年度は small-step の意味論と big-step の意味論を結ぶプロジェクトの 一環として、shift0/reset0 についても扱ってみました。 こちらは control/prompt のときとは違って、比較的、 スムーズに両者を結びつけることができました。 そこで欲張って、さらに代数的効果とハンドラも扱ってみました。 その結果、こちらも筋よく両者を結びつけることができました。
shift0/reset0 は（deep な）代数的効果とハンドラと近いことが知られていますが、 4 種の限定継続演算子の理論に基づいて 代数的効果とハンドラの理論を構築するのが良いことの ひとつの例を示すことができました。 代数的効果とハンドラは OCaml 5 に入るなど近年、盛んに研究されていますが、 統一的な基礎理論はまだ確立されていない印象です。 研究室では、4 種の限定継続演算子の基礎理論をベースにして 代数的効果とハンドラの理論の確立を目指しています。
ZINC 仮想機械の最適化
研究室では OchaCaml という言語を開発しています。 これは OCaml の前身である Caml Light に shift/reset を入れた言語です。 Caml Light や OCaml では、中で ZINC という仮想機械が使われ、 そこに関数呼び出しを効率的に実行する最適化が組み込まれています。 この最適化を、shift で切り取ってきた継続についても適用できないか というのが目下の研究課題です。
この手の最適化は、 低レベルな機械語（バイトコード）で語られることが多いのですが、 機械語で最適化を議論すると、その正当性を保証するのが難しくなります。 そうではなく、研究室では、インタプリタのレベルでこれらの最適化を議論し、 正当性が自明な形で最適化を入れる方法を研究しています。 昨年度までに ZINC の最適化の重要な部分はカバーしたのですが、 今年度の研究でほぼ全てをカバーできたと考えています。
そうすると、いよいよこの最適化を 限定継続演算子で切り取ってきた継続に対しても適用してみよう という段階にやってきたことになります。 現在の OchaCaml は shift/reset しかサポートしていませんが、 ZINC の抽象機械の最適化は shift/rest に特有ではなく 4 種の限定継続演算子全てについて使えると考えています。 OchaCaml に 4 種の限定継続演算子を最適化込みで実装する日は そう遠くないと期待しています。
初心者プログラミング教育
初心者プログラミングで、ブロックを使うのは有効です。 いずれテキストエディタでプログラムを書くようになる情報の学生さんにとっても、 最初の慣れないうちはブロックを使って楽にプログラムを書くことで、 プログラミングの本質に集中することができます。 後日、慣れた頃にテキストエディタに移るのは、 多少の抵抗はあっても案外とすんなり行くものです。そう信じて OCaml Blockly を作ってきましたが、 その開発とメンテナンスは恐ろしく大変なんです。 あまりに大変でもう諦めようかと思うこともありました。 でも、今年度は新たな希望が生まれました。
OCaml Blockly の新実装
どうして OCaml Blockly の開発・メンテナンスが大変かというと、 あの手の環境を構築するにはブロックの配置や接続、メニューの作成や、 設定ボタンなどありとあらゆるものを作り上げないと 皆に使ってもらえるシステムとはならないからです。 でも、よく考えてみると、 その多くの機能は OCaml Blockly に特有ではありません。 OCaml Blockly は Google が開発した Blockly をベースにしています。 Google の Blockly は手続き型言語専用で OCaml はサポートしていません。 でも、OCaml 特有の機能以外の部分については、そのまま流用できれば メンテナンスの労力は大きく減らせます。今年度はそれを行いました。
設計方針の基本は、Google の Blockly には触らずにそのまま利用し、OCaml に特有の機能だけを追加する形で実装するというものです。 OCaml に特有の機能というのは、OCaml 用の各種のブロックに加えて、 型推論の機能とスコープの機能があげられます。 各種のブロックはもちろん実装しなくてはなりませんが、これは単純作業です。 それ以外に必要な機能を洗い出してみると、 それほど大量ではないことがわかってきました。 これらを Google Blockly とは独立して提供することで、 OCaml Blockly に必要な機能の差分を明らかにすることができました。
これ、言葉で書くと簡単ですが、実装は相当、大変です。 膨大な Google の Blockly のソースコードを理解した上で、 それを壊すことなく必要な機能を追加していきます。 実装言語は TypeScript です。 でも 1 年間、頑張った結果、それらしい形になってきました。 これはとても大きな成果です。 これまで、どうにも手をつけられなくなっていた OCaml Blockly が復活したと言っても過言ではありません。 また、OCaml を入れるにあたっての概念的な差分が 思ったほどは大きくなかったことがわかったことも収穫でした。
授業で使うには、もっと完成度を上げていかなくてはなりませんが、 その道筋が見えてきました。 1 年後に新生 OCaml Blockly を授業で使えるよう頑張ります。
LA ゲームプログラミングでのチュートリアル
昨年度、OCaml Blockly 用のチュートリアル言語を作成しました。 これ、チュートリアル実装の中身を何も知らなくても チュートリアルを作れるという優れもの。 これを活用しない手はない、と、 今年度 LA ゲームプログラミングの授業で使用しました。
具体的には、各授業のレジメの中に、 そこで学ぶ内容を伝えるチュートリアルを大量に組み込みました。 これで、学生さんは操作につまづいた時、 いつでもチュートリアルを見直してやり方を思い出すことができます。 そのおかげかどうかはわかりませんが、 今年度の授業では基本的な操作でつまづく学生さんが少なく、 より内容に関する質問が増えたような印象があります。
今年度、本格的にチュートリアルを作ってみて、 チュートリアルシステム自体の信頼性も上がりました。 来年度は、関数型言語のチュートリアルを作ってみるのも面白そうです。