2017 Fiscal Year Research-status Report
プログラム意味論に基づく先進的なプログラミング環境の構築
| Project/Area Number |
15K00090
|
|---|
| Research Institution | Ochanomizu University |
|---|
Principal Investigator |
浅井 健一 お茶の水女子大学, 基幹研究院, 准教授 (10262156)
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | 開発環境 / 関数型言語 / 型システム / 型デバッガ / ステッパ |
|---|
| Outline of Annual Research Achievements |
本年度は (1) 静的な意味論に基づくプログラミング環境として、型エラースライサの高速化の実装と評価を行なった。また (2) 動的な意味論に基づくプログラミング環境として、前年度までに実装したステッパを拡張して例外処理と出力命令をサポートするとともに、関数呼び出しをスキップする機能を実装した。それぞれ、詳しく述べる。
(1) 静的な意味論に基づくプログラミング環境については、作成した型エラースライサの高速化を行なった。型エラースライサは型デバッグ時の質問の回数を減らすのに有効だが、型エラースライスを求めるのに内部で何度も型推論を行なっている。プログラムが大きくなっているとそのオーバヘッドが無視できなくなってくる。そこで、これまでの１ノードずつ処理する方法を改め、子ノードのうち一番大きなものから処理をする方法と複数ノードを同時に選ぶことで２分探索と同じ形で処理する方法を実装した。いろいろなプログラムで実験してみた結果、２分探索を行う形にすると特に大きなプログラムの場合、速度向上が見られることがわかった。
(2) 動的な意味論に基づくプログラミング環境については、ステッパを拡張して例外処理をサポートした。例外処理の定式化には例外を表す値を伝播させていく方法があるが、そのように表現したのでは実際の処理系の動きとは異なってしまう。そこで（メタ言語の）例外処理そのものを使って例外処理のステップ実行を実装した。このようにすることでユーザは例外が発生した途端、制御がハンドラに移る様子を観察できるようになる。
これ以外に print 文のような出力命令をサポートした。これは「これまでに出力された文字列」を保持することで実装した。また、これまでのステッパは全ステップをひとつひとつ進む必要があったが、それを関数呼び出し単位でスキップする機能も実装した。これにより使いやすさがかなり向上した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(1) については、型エラースライサの実装と高速化ができている。これでひと段落したと考えており、おおむね順調に進展していると考えられる。一方、ユーザインタフェース部分の構築は１年目以降は思ったほどは進んでいない。これは（定理証明系 Agda などとは異なり）OCaml では型情報がそれほど多くないため有効なインタフェースを提供しにくいこと、初心者でも使える環境を構築するには膨大な労力が必要な割にその有効性の見通しが乏しいことによる。これを発展的に解消する方向性として現在、型情報をコネクタ部分に保持するブロックを使ったインタフェースの構築を開始している。
(2) については、これまでに作成してきたステッパの信頼性がかなり向上してきているのに加えて、例外処理のサポートや関数のスキップなども実装できており、計画はおおむね順調に進展していると考えられる。次年度の授業では、このステッパを主力として使用しており、これまでのところ順調に進んでいる。
|
| Strategy for Future Research Activity |
(1) については、型エラースライサの実装をまとめて公開できるように検討する。また、ユーザインタフェース部分については、ブロックプログラミングの方向を引き続き真剣に検討する。
(2) については、引き続き授業でステッパを使用しながら完成度をあげるとともに、まだサポートできていない命令、具体的にはモジュールについて検討する。
|
| Causes of Carryover |
ステッパについて、この半年でいくつかの進展（具体的には、関数の実行を飛ばす機能の実装、例外処理のサポート、出力命令のサポート、各種の安定性の向上）があった。申請者の４月からのプログラミングの授業で実際に改良されたステッパを使用し、その改良がどのくらい有効であるかを確認したいため。
作成したステッパ（と型エラースライサ）を実際の授業で使った際に得られるフィードバックへの対応のために人手が必要なため、主に謝金で支出予定。
|
