2020年度振り返り

研究室ではこのところ、

• 限定継続演算子
• 初心者プログラミング教育

の２本立てで研究を進めています。

限定継続演算子の研究

限定継続演算子というのは例外処理を一般化したような命令で、
プログラムの制御がある場所からはるか離れた場所に飛んでいくようなことを
自在に表現することができます。中でも最近、
代数的効果 (algebraic effects andhandlers) というのが有名になってきており、
Multicore OCaml で実装されて実用的になりつつあります。

ところがこの代数的効果、その基礎理論はどうもわかりにくいものです。

確かに CPS 変換による意味論や型システムなどは提供されているのですが、
それらは以前から知られている限定継続演算子と比べると複雑で、
本質を突いているとは思えません。やはり限定継続演算子の理解には、
すっきりした CPS インタプリタ（CPS 変換）と型システム、その正当性、
また、機械語による実装への指針などが欲しいところです。


そこで今年度は、基本となる４種類の限定継続演算子について、
その理論の確立を行いました。４種類の限定継続演算子というのは、
研究室でも長らく扱っている shift/reset^(参考1), control/prompt, shift0/reset0,
control0/prompt0 と呼ばれるもので、これらは微妙にその動作が異なります。

まず、前期の大学院の授業を使って、４種類の限定継続演算子について、
その挙動と CPS による意味論（インタプリタ）を把握しました。
CPS インタプリタについては、すでに過去の仕事で示されていましたが、
授業で改めて見直し、４種類の限定継続演算子に対する
CPS インタプリタを直行する形できれいに表現できるようになりました。

参考1: shift/reset プログラミング入門


その上で、これらに対する型システムを構築しました。
型システムは、shift/reset については「これぞ」と思われるものが
すでに知られていましたが、それ以外についての状況は芳しくはありません。
一部、型システムが存在するものもありましたが、
なぜそのようになるのか、それが自然なのかは研究室では理解できていませんでした。

そこで、大学院の授業後半では４種類の限定継続演算子の中から
control/prompt を選んで、その型システムの構築を試みました。
なかなか紆余曲折があったのですが、結果として CPS インタプリタに対応する
「最も一般的」と考えられる型システムを構築することができました。
この成果については、国際会議^(参考2)で発表しています。

それ以外の型システムについては現在、検討中ですが、shift0/reset0
についてはこれまでに知られていたものが良さそうであることがわかってきました。

また control0/prompt0 については、これまで型システムは知られていませんでしたが、
良さそうなものができつつあります。これらは来年度に取り組むべき課題となります。

参考2: A Functional Abstraction of Typed Trails


これらの正当性についても研究を進めています。
正当性を定理証明系で示すのにはとても多くの労力がかかりますが、
一度、示されるとバグがなく 100% 正しいことが示されるので、その威力は絶大です。
今年度は control/prompt についての正当性の証明を進めるとともに、
shift/reset については、単なる正当性ではなく
CPS 変換が reflection になっている証明についても研究を進めています。


一方、４種類の限定継続演算子に対する機械語実装については、後期に取り組みました。
これまでに知られていた低レベルな実装は、別の演算子を用いていたのですが、
ここでは４種類の限定継続演算子を正面から扱っています。
まず最初に control/prompt に対する機械語実装（仮想機械）を、
各種プログラム変換を使う手法によって得ました。
これがなかなかうまくいったので、調子に乗って４種類の継続演算子全てについて、
仮想機械を得ました。前者については国内のワークショップで発表し、
後者については国際会議に論文を投稿中です。


４種類の限定継続演算子に対する型システムと低レベル実装の基礎理論が揃うと、
いよいよこれらを OchaCaml に実装できるかもしれません。
そのためにはさらに多相性との関連や再帰をどうするかなどを
検討しなければなりません。また、これらの知見を通して、
代数的効果の基礎理論についても取り組んでいきたいところです。

初心者プログラミング

このように、今年度は限定継続演算子の基礎理論を中心に研究が大きく進みましたが、
初心者プログラミング教育の研究を忘れているわけではありません。
昨年度から本格運用している OCaml Blockly は健在です。
コロナでオンライン授業になる中、関数型言語の授業では学生さんに
自宅のブラウザで OCaml Blockly を使って最短路問題を作成してもらいました。
今年から OCaml Blockly に実行環境も加わっていよいよ好調です。

また、後期の全学向けゲームプログラミング入門でも、今年は Racket を離れて
OCaml Blockly と研究室で開発している universe ライブラリを使って行いました。
この授業も関数型言語の授業も、対面で質問を受けられないところが
苦しいところでしたが、でも、OCaml Blockly がなかったら
オンラインでは授業はできなかったのではないかと思います。


universe ライブラリは、簡単にゲームを作れるフレームワークですが、
こちらの改良も進めています。
これまでは単独ゲームしかサポートしていませんでしたが、
対戦ゲームをできるように拡張中です。
いくつかの条件はあるものの、それらが整えば動きつつあります。
これを上手に使って、初心者が勝手に楽しみながら
（対戦）ゲームを作れるサイトを作れないかと夢見ています。


さらに、今年はこれまでに集めてきた関数型言語の授業の膨大なログを解析して、
初心者のプログラミング行動の分析を行いました。
学生さんがどのようにプログラミングに取り組んでいるのか、
どこで学生が苦しんでいるのかを把握できると、少しずつ授業の改善にもつながります。
あなたが起こした数々のエラー、確実に後の人たちの役に立っています（！？）。

また、ログを分析した結果、
OCaml Blockly を使ったプログラミングと普通のテキストプログラミングは、
その後のプログラミング力に大きな差は出ていないらしいという印象です。
まだ、データは少ないのですが、OCaml Blockly は「お遊びプログラミング」ではなく、
本格的なプログラミングなのです。


関数型言語の授業、OCaml Blockly 以外にも、
これまで型デバッガやステッパなど多くのツールを作ってきました。
来年度に向けて、これらのツールの拡張も行なっています。
特に、ステッパについては、ついにモジュールをサポートする予定です。
モジュールのサポートは、そもそもどのようにステップ実行したら良いのかの
検討から始める必要がありました。あれこれ試行錯誤をしましたが、
良いところに落ち着いてきたと思っています。
これが、学生さんの理解を深めるのにどのように役に立ってくれるか、興味津々です。

来年度(2021)に向けて

来年度はこれらに加えて、OCaml Blockly を使った数学教材の作成や、
型システム GUI 作成器 Mikiβ の拡充をしていきたいと思っています。

先ほど、初心者プログラミング教材に少し触れましたが、
同様にして数学と OCaml を両方学べる初心者向けサイトを作れないかと思っています。
OCaml は関数型言語、必要な知識は中学の数学で習う関数のみです。
これは OCaml Blockly の Scratch など他のビジュアルプログラミングエディタとは違う
大きな利点だと思っています。OCaml Blockly なら、中学、高校のカリキュラムを
押しのけることなく入っていけるのではないかと思っています。

あとは、Mikiβの拡張を行いたいですね。
Mikiβは「型システムの定義を与えると、対応する GUI を作ってくれる」という
夢のようなプログラムです。
でも、残念ながら現在、相互再帰するような型はサポートできていません。
これは、generic programming の考え方を上手に使うとどうにかなりそうという
見通しが立っています。
これを、具体化して、実際に相互再帰をサポートしていきたいです。

限定継続の型システム用の GUI が欲しいのですが、これには相互再帰が必要なんです。
うまくサポートできれば、限定継続の型システムの研究も進みそうです。