2024年度振り返り
今年度は理論系に軸足をおいて研究を進めてきました。目指すのは４種類の 限定継続演算子の研究を全てやり尽くして、全体像を確立させることです。 が、思いがけず教育系の方もいろいろ進みました。今年度は、理論系から 書こうと思います。限定継続演算子の研究
control/prompt の正当性の証明
４種類ある限定継続演算子のうちのひとつである control/prompt について、 その CPS 変換が正しいことを証明しました。この研究は、何年も前から 取り組んでいたのですが、これまではうまく行っていませんでした。それを 「継続とトレイルはいつも一緒に使われている」ということに注目し、それを 反映したような論理関係を定義することで証明に至りました。
結果を一言で述べると上のようになりますが、ここまで来るには 多くの涙ぐましい（笑）努力がありました。これまで、いろいろな失敗を した経験から、研究室全体で議論できる土壌を作るのが大事と考え、今年は、 まずは五十嵐先生の「プログラミング言語の基礎概念」をゼミでしっかり 読み込みました。大学院の授業ではパラメトリシティと論理関係の話 （につながる話題）を扱いました。表向きは型の話から カリーハワード同型までを扱う普通の授業ですが、こちらのねらいはもちろん 研究室の４年生にパラメトリシティと論理関係の基礎を理解してもらうこと です。さらに、研究室合宿でもその話題を取り上げました。 これらの基礎の上に立って、研究室の先輩の control/prompt に関する論文を 皆で読んで理解しました。これらの努力のおかげで control/prompt の動きを 肌で感じられる人材が育ち（笑）、当たり前のように control/prompt の話が できるようになりました。素晴らしいことです。
CPS 変換の正当性の証明ができたら、次は reflection の証明を行いたいとこ ろです。ですが、これはまた大きな山かも知れません。reflection の証明では、 単なる等価性ではなく簡約が対応することを示さなければなりません。しかし、 等価性の証明の段階で論理関係のような道具立てが必要となると、 簡約の対応関係をすんなり示せるとは思えません。もう少し深い考察が必要に なりそうです。これは、来年度に向けての課題になります。
限定継続演算子の効率的な実装に向けて
限定継続演算子は、これまでによく使われてきた shift/reset 以外に、 control/prompt を含めてあと３種類、存在します。でも、これまで研究室で 作ってきた OchaCaml は、shift/reset しかサポートしていません。OchaCaml での経験から、実装が存在するのは限定継続演算子の研究ではとても大切です。 是非とも、４種類の限定継続演算子すべてを使える処理系が欲しいところです。 そのような処理系の作成に向けて、今年度は「限定継続演算子の定義を与える インタプリタ」を少しずつ変形して OchaCaml（や OCaml）の抽象機械を導き 出すという研究を行いました。
この抽象機械は ZINC 抽象機械と呼ばれていて、複数引数の関数呼び出しを効 率的に実行できることが知られています。しかし、これまでその実装方法は 抽象機械レベルでのみ定義されていて、そこにどのようにして限定継続命令を 入れたら良いのかは明らかではありませんでした。今回「限定継続演算子の 定義を与えるインタプリタ」から ZINC 抽象機械を得る方法を理解したことで、 限定継続演算子の ZINC 抽象機械上での実装方法が明らかになってきたと 考えています。
すでに４種類の限定継続演算子に対する型システムは 2022 年の研究で 明らかにしているので、いよいよ４種類の限定継続演算子をすべてサポートする OchaCaml を実装できるかと期待しています。
４種類の限定継続演算子に対する多相の型システムに向けて
OchaCaml のような実際に汎用で使うことのできるプログラミング言語を作る ためには、多相の型システムは重要です。これまで shift/reset に対する 多相の型システムは提案されていますが、それ以外の限定継続演算子に対する 多相の型システムは提案されていません。今年度は、そこを突破できないかと 研究を行いました。
この研究、現時点での結論は「shift/reset 以外の限定継続演算子に対して 多相の型システムを作るのは簡単ではない」なのですが、そこに至る過程で いろいろなことを学びました。ひとつは control/prompt の答えの型について 多相を導入するのは難しそうだということ。これは、捕捉する継続の答えの型が 他の部分にも現れてしまっているためです。一方、control/prompt の トレイルの型については多相を導入できるかも知れないことがわかってきました。 ここはまだ精査が必要ですが、これまでに考えていたのとは違った方向の多相の 可能性が出てきました。
これらの考察は、なかなか複雑で理解するのが大変なのですが、 control/prompt を肌で感じられる人材が育ったおかげで、かなり見通しよく いろいろな議論ができるようになりました。
shift/reset を使ったプログラムに対する reasoning
shift/reset を使ったプログラムについての性質の検証は、ここ２年ほど 取り組んでいる研究テーマです。今年度は篩型（ふるいがた）を 導入することで、性質を検証できないかを検討しました。その結果、 簡単ではないものの上手に基本型に性質を記述する（篩型を使う）と いくつかのプログラムの性質を検証できることがわかってきました。
一方で、性質の記述がなかなか難しいこと、また、それを上手に伝播させて 証明を進めるのも簡単ではないことなどが課題です。現在の実装では、 shift/reset を使ったプログラムはモナドを使って表現しています。この 表現では答えの型も明示的に扱っているので、CPS 変換をしたプログラムと 同等のものになっています。そうすると、CPS で書かれた普通のプログラムの 検証と同じ程度の難しさでできるはずと考えられるのですが、どうも現状では それよりも難しくなっているように感じられ、そこの差がなんなのかは 解明できていません。これは、今後の課題です。
初心者プログラミング教育
ここ数年、研究室では初心者プログラミング教育に向けて いろいろな取り組みをしてきました。今年度は、その資産を生かして、それを 活用していく段階を踏んだように思います。Mikiβの本格使用
まず、最初に行ったのが Mikiβの本格使用です。Mikiβは、推論規則の 定義を与えるとその GUI が得られるシステムですが、昨年度までに 推論規則の定義を web 上で与えられるようになっていました。つまり、 なんらプログラムを作ることなく web 操作だけで推論規則の GUI が 得られるのです。
これは活用しない手がないというわけで、五十嵐先生の「プログラミング言語 の基礎概念」を読む際、そこに出てくる各種の推論規則を Mikiβにのせて みました。これ、面倒なだけで詰まらないかと最初は思ったのですが、実際に 作ってみると、自由に証明木をブラウザで作ることができるようになるので 推論規則の理解に大きく役に立ったように思います。
ここでの経験があったから、その後 control/prompt の型システムなど複雑な ものが出てきたときも、上手に Mikiβを使っていろいろな証明木を作ることが でき、それが深い理解につながったと思います。いろいろな実例に基づいて ものを考えられるようになり、大いに役に立ちました。
チュートリアル作成向け専用言語
次に活用したのは OCaml Blockly のチュートリアルです。研究室では、 OCaml のゲームプログラミングを自分で学習できるチュートリアルサイトを 作っています。今年度当初は、そのような学習教材をもっといろいろ 作ってみようと思い、どのようなものをどんな感じで作ったら良いかを 検討しました。
ちなみに、その検討の一環として、任天堂 Switch とゲームをひとつ購入し、 ゼミでそのゲームを行って検討するという面白いゼミをやりました。この ゲームは「ゲームを作るゲーム」で、ユーザは遊びながらプログラミングを 学び、好きなゲームを作ることができるようになっています。実際、皆で そのゲームをすることで、どのようにして何も知らない人にプログラミングを 教えているのかを勉強しました。なかなか参考になるものが多かったように 思います。
その上で、では実際に新しいチュートリアルを作ろうと思ったところで 問題が起きました。これまでに作ってきたチュートリアルサイトは javascript で書かれていますが、そこに手を加えるのが難しかったのです。 中では各種のデータ構造を使ってチュートリアルを表現し、それを読み込み ながらチュートリアルを進めているのですが、構造が複雑で、開発者以外が 手を加えるのは難しい状況でした。
そこで、この実装を整理して、チュートリアル作成を専用に行う専用言語を 設計し、実装しました。これを使うと、内部の実装を全く知ることなく、 単に行いたい操作を順に書いていけばチュートリアルが完成します。これに よって、とても簡単にまた気軽にチュートリアルを作ることができるように なりました。
新しく専用の言語を作ったことで新たな展望も開けてきました。途中で 間違った操作をしてしまった場合の処理や、不可能な操作（メニューを 開いていないのに、その中のブロックを取り出そうとするなど）の排除などを 考えることができるようになってきたのです。これらを実装できると、 さらに便利な言語に育っていきそうです。
また、気軽に使うことのできる専用言語ができあがったので、これを使って 来年度は実際にいろいろなチュートリアルを作ってみたいものと思っています。 手始めに、後期のゲームプログラミングの各回の授業用のチュートリアルを 順に作るというのは面白そうです。
OCaml Blockly
「関数型言語」の授業では、もう何年も OCaml Blockly を使っています。 OCaml Blockly は研究室の先輩が作り上げたものですが、これがこれまで 日本語の論文でしか発表されてこなかったのは残念だと思っていました。 それを打破すべく、２年ほど前から OCaml Blockly についての論文を 書いていたのですが、それがこの度、ついに採録されました。
OCaml Blockly では、ブロックでプログラミングをするので構文エラーは （穴が全部、埋まっていれば）起こりません。加えて、OCaml Blockly では 裏で型チェックも行っているので型エラーも起こりません。さらに、変数は スコープの中でしか使えないのでスコープエラーも起こらないように なっています。これらの特徴に加えて、論文では OCaml Blockly が教育に どのくらい有効そうかについての考察も行いました。
OCaml Blockly は、なかなか面白いシステムになっていると思っていたので、 それがついに英語になって世に出ることになったのは とても嬉しく思っています。 一方で、論文の査読では「VS Code を使えば似たようなことができるのでは ないか」といった批判も受けました。ぼくは、たとえ情報を専門とする人が 対象であっても、プログラミングの最初のハードルを下げる役割は十分にある と考えていますが、確かに VS Code は便利な環境を提供しています。それが どのくらい便利かを調べるため、来年度からは関数型言語の授業で VS Code を使ってみる予定です。そこでどのようなことが起きるのか今から楽しみです。
関数型言語の授業では OCaml Blockly を使わなくなりますが、全学向けの ゲームプログラミングの授業では OCaml Blockly をまだまだ使い続けます。 OCaml Blockly は、初心者にはやはりおそろしく便利だと思います。
VS Code の extension
来年度から、関数型言語の授業で VS Code を使うにあたり、これまで 提供してきたいろいろなツールが使えなくなるのは容認できません。特に OCaml のステッパは必須と考えています。そこで、VS Code の中から ステッパを使えるようにする VS Code の extension を実装しました。 これ、研究成果として発表できるような話ではありませんが、授業を スムーズに行うためにはとても重要です。研究室の皆がいろいろな面で 貢献してくれたので、それなりのものができたと思っています。これで 来年度の授業を乗り切りたいと考えています。
VS Code に移るにあたり、残念ながら型デバッガは使えなくなってしまいます。 VS Code をうまく使うためには OCaml の language server というツールを 入れる必要があるのですが、それと型デバッガがうまく共存できないのです。 これは残念なので、将来的には共存できるように手を加えたいと考えていますが、 これにはかなりの時間がかかりそうです。それまでの間は、VS Code が提供する 型エラーの波線表示で乗り切る予定です。