プログラミング言語の基礎概念(CoPL)という本があります。この本は操作的意味論と型システムの入門書なんですが、オンライン演習システムがあるのが特色で、演習問題を解くと正誤を自動でジャッジしてくれます。
導出規則にしたがって式の評価や型付けを行って導出木を書くというのが演習の形式で、問題はなんと160問も用意されています。すごいですね。
ということで演習システムの問題を解くプログラムを書きました。
github.com
以下の導出システムに対応しています。
- EvalML1〜5 (簡単な式の簡約、局所定義と束縛、関数抽象・適用、リスト、パターンマッチ)
- EvalRefML3 (参照)
- EvalContML1,4 (継続、第一級継続)
Githubで「CoPL」で検索すると同じようなことをしている人がたくさん見つかります。はてなブログにも先駆者がいらっしゃるようです。通過儀礼みたいなものでしょうか。
fetburner.hatenablog.com
さて、作ったプログラムが対応していない問題も別に実装するなり人力で導出するなりしてどうにか160問全部解くことができたので、演習問題を解く過程で得られた(多くは非本質な)知見を後続の人に向けて書き留めておきたいと思います。
動機
はじめのうちは人力で解いていたんですが、EvalML3で関数が再帰をはじめたあたりで導出の量が殺人的になってきて、心が折れてやむなくプログラムに解かせることにしたという経緯があります。参考までにEvalML3のとある問題の導出を載せておきましょう:
長いので折り畳み
|- let rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2) in fib 5 evalto 5 by E-LetRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib 5 evalto 5 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- 5 evalto 5 by E-Int {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 5 by E-IfF {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- n < 3 evalto false by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- n evalto 5 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- 3 evalto 3 by E-Int {};
5 less than 3 is false by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- fib (n - 1) + fib (n - 2) evalto 5 by E-Plus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- fib (n - 1) evalto 3 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- n - 1 evalto 4 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- n evalto 5 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- 1 evalto 1 by E-Int {};
5 minus 1 is 4 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 3 by E-IfF {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- n < 3 evalto false by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- n evalto 4 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- 3 evalto 3 by E-Int {};
4 less than 3 is false by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- fib (n - 1) + fib (n - 2) evalto 3 by E-Plus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- fib (n - 1) evalto 2 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- n - 1 evalto 3 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- n evalto 4 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- 1 evalto 1 by E-Int {};
4 minus 1 is 3 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 2 by E-IfF {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n < 3 evalto false by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n evalto 3 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- 3 evalto 3 by E-Int {};
3 less than 3 is false by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib (n - 1) + fib (n - 2) evalto 2 by E-Plus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib (n - 1) evalto 1 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n - 1 evalto 2 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n evalto 3 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- 1 evalto 1 by E-Int {};
3 minus 1 is 2 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 1 by E-IfT {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- n < 3 evalto true by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- n evalto 2 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- 3 evalto 3 by E-Int {};
2 less than 3 is true by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- 1 evalto 1 by E-Int {};
};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib (n - 2) evalto 1 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n - 2 evalto 1 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n evalto 3 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- 2 evalto 2 by E-Int {};
3 minus 2 is 1 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 1 by E-IfT {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- n < 3 evalto true by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- n evalto 1 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- 3 evalto 3 by E-Int {};
1 less than 3 is true by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- 1 evalto 1 by E-Int {};
};
};
1 plus 1 is 2 by B-Plus {};
};
};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- fib (n - 2) evalto 1 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- n - 2 evalto 2 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- n evalto 4 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 4 |- 2 evalto 2 by E-Int {};
4 minus 2 is 2 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 1 by E-IfT {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- n < 3 evalto true by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- n evalto 2 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- 3 evalto 3 by E-Int {};
2 less than 3 is true by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- 1 evalto 1 by E-Int {};
};
};
2 plus 1 is 3 by B-Plus {};
};
};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- fib (n - 2) evalto 2 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- n - 2 evalto 3 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- n evalto 5 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 5 |- 2 evalto 2 by E-Int {};
5 minus 2 is 3 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 2 by E-IfF {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n < 3 evalto false by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n evalto 3 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- 3 evalto 3 by E-Int {};
3 less than 3 is false by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib (n - 1) + fib (n - 2) evalto 2 by E-Plus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib (n - 1) evalto 1 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n - 1 evalto 2 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n evalto 3 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- 1 evalto 1 by E-Int {};
3 minus 1 is 2 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 1 by E-IfT {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- n < 3 evalto true by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- n evalto 2 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- 3 evalto 3 by E-Int {};
2 less than 3 is true by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 2 |- 1 evalto 1 by E-Int {};
};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib (n - 2) evalto 1 by E-AppRec {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var2 {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] |- fib evalto ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)] by E-Var1 {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n - 2 evalto 1 by E-Minus {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- n evalto 3 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 3 |- 2 evalto 2 by E-Int {};
3 minus 2 is 1 by B-Minus {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- if n < 3 then 1 else fib (n - 1) + fib (n - 2) evalto 1 by E-IfT {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- n < 3 evalto true by E-Lt {
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- n evalto 1 by E-Var1 {};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- 3 evalto 3 by E-Int {};
1 less than 3 is true by B-Lt {};
};
fib = ()[rec fib = fun n -> if n < 3 then 1 else fib (n - 1) + fib (n - 2)], n = 1 |- 1 evalto 1 by E-Int {};
};
};
1 plus 1 is 2 by B-Plus {};
};
};
};
3 plus 2 is 5 by B-Plus {};
};
};
};
};
どうですか、心は折れましたか？なんか検索してみると「《強力なエディタ》とスニペットさえあれば人力でもいける」と主張する人がぼちぼち見つかるんですが、わたしは《強力なエディタ》を使いこなす力を持ちあわせていないのであっさり諦めました。
方針
とりあえず実装に使う言語はOCamlに決定しました。わたしが使うことのできる言語のなかで最もプログラミング言語処理系の作成に向いているのがOCamlだからです。
そうはいってもわたしのOCaml経験はLazy Kで世界に挨拶(OCamlの練習) - AdC用にとりあえず用意したブログでLazy Kのコードを吐くプログラムを書いたくらいで、yaccも使ったことがなくて言語処理系をつくるには微妙なところでしたが、天下の京都大学が公開しているプログラミング言語処理系の講義資料IoPLMaterials | Materials for the class “Implementation of Programming Languages” in Kyoto University.がとてもいい感じだったのでそれを足掛かりにしてどうにかプログラムを書くことができました。
講義資料に習ってビルドシステムにはdune、構文解析と字句解析にはmenhirとocamllexを使います。
ここで「導出システムの数だけプログラムを別々に作る」のと「複数の導出システムを同居させる」ので迷ったんですが、EvalML1〜EvalML5は互換性があるだろうと期待していたわたしは後者を選択しました。
結論をいえば前者の方が楽です。後述しますが、導出システムはEvalML1〜EvalML5でも微妙に互換性のない部分があるので後者を選択すると構文解析とかでいろいろと悩むことになってしまいます。その悩みの内容というのは操作的意味論や型システムとは関係ない非本質な部分なので悲しいですね。
知見
以下は演習システムを触ったことがある人向けの内容になります。
EvalML3
(再帰)関数抽象と適用を扱う導出システムです。人力でやると心が折れます。
互換性
EvalML3はEvalML2の完全な上位互換で、EvalML2で正しい導出はEvalML3でも正しいことになります。
当然のことのように思えますが、実はこのような互換性があるのはEvalML2とEvalML3の間だけで、EvalML3より上位の導出システムは些細な違いがあってEvalML3との互換性がありません。悲しいですね。
循環参照
EvalML2では値をValueモジュール、環境をEnvモジュールで管理していたんですが、EvalML3で第一級関数を導入すると
- 環境は値をもつ(EnvはValueに依存する)
- 関数の値は関数閉包として環境をもつ(ValueはEnvに依存する)
ということで循環参照が発生してしんでしまいました。ここでは応急処置としてEnvモジュールを削除してValueモジュールに統一して相互再帰のデータ型を定義しましたが、再帰モジュールにしてもよかったかもしれません。
EvalRefML3
参照と副作用を扱う闇の導出システムですが、参照と値の対応である「ストア」を値として持って回すことで評価関数自体は純粋につくることができます。おもしろいですね。
互換性
EvalRefML3は環境のほかにストアというものが登場して、構文も拡張されます。しかし空のストアは表記を省略できるので、EvalML3と導出に互換性があるように思えます。
しかしながら、何故かEvalRefML3に限ってe * eという式に対応する導出規則がE-TimesではなくてE-Multであるという罠があります。謎です。
どうしようもないので、式を評価するまえに構文を調べて導出システムのバージョンを検出して、それを導出関数にわたすという解決策をとりました。
ロケーションの名前と入力の終端
ストアは参照のアドレスを表す「ロケーション」というものを持っているのですが、導出システムの表記の都合上、これには名前をつけてあげる必要があります(@lとか@l1とか)。じゃあこの名前は適当に生成していいのかというとそんなことはなくて、与えられる判断に出現する名前と同じにしないといけません。
|- let x = ref 2 in let y = ref 3 in
let refx = ref x in let refy = ref y in
let z = !refx := !(!refy) in !x
evalto 3 / @l1 = 3, @l2 = 3, @l3 = @l1, @l4 = @l2
例えば上の判断の導出を作成するときは、ロケーションの名前は@l1 @l2 @l3 @l4にする必要があるわけです。
ここでひとつ(本質的ではない、どうでもいい)問題が浮上します。
今までは、判断を導出するために必要な情報はevaltoより前に全て与えられていて、evaltoの後の情報は必要ありませんでした。するとevaltoを入力の終端として扱うことができるので、
- プログラムを起動する
- 演習システムで与えられた判断をコピペする
- Enterキーを押す
だけで入力の終端を意味するevaltoが読み込まれて、プログラムは入力の読み込みを完了して結果を返してくれます。わたしはこの操作感にやたらこだわっていました。
一方で今回はevaltoより後の情報が必要になります。ここで、最も右側にくるストアの構文は@l1 = 1, @l2 = 2, ...とどこまでも続く可能性があるので、別に終端を表す記号を与えない限りプログラムは入力を永遠に待ち続けることになります。終端を表す記号といえばCtrl DでEOFを与えるか、;;と書くかといったところでしょうか。
しかし当時のわたしは何故か「コピペ→Enter→終わり」の流れを死守しようとして、以下の方法を思いついて実装しました。
- まず
evaltoを終端として入力を取り、評価、導出を行う。ロケーションの名前には適当に生成したものを用いる。
- すると生成されるロケーションの数がわかるので、個数分だけ
<Value> / <Loc>または= <Value> , <Loc>という文法で構文解析を行いロケーション名前を取り出す。終端記号は必要ない。
- 導出中のロケーションの名前を全て書き換える。
なかなか邪悪な方法ですが、とにかく「コピペ→Enter→終わり」の流れは守られました。演習問題を解くのには差し支えありません。これを実装できたときは自分の邪悪さに笑い転げていたような覚えがあります。人生楽しそうですね。
もし今作り直すなら譲歩して
- まず
evaltoを終端として入力を取り、導出システムを検査する。
- EvalRefML3だったときに限り、追加で入力と終端記号を要求する
という感じにすると思います。
EvalML4, EvalML5
リストとパターンマッチを扱う導出システムです。素数列挙とかが可能になります。
互換性
変数の値を取り出す導出規則E-Var1 E-Var2がE-VarひとつにまとめられたことでEvalML3との互換性を失っています。
それから、EvalML4とEvalML5のパターンマッチは構文も導出規則も異なることに注意が必要です。
TypingML4
多相性のない型システムを扱う導出システムです。
コードの再利用
TypingML系列は今までのEvalML系列とは大きく異なる導出システムで、共通しているのは式の構文(Exp)と導出の表記方法くらいです。
ここで共通する部分は使いまわせるように、今までEvalMLのみに対応していた導出関連のモジュールをファンクターにしたりしました。
導出システムの判別
TypingML系列は式に続いてevaltoのかわりに:が入るので、そこでEvalML系列と判別をすることが可能です。空の環境と空の型環境でreduce/reduce conflictが発生したりしますが、少し工夫するとなんとかなります。
MLは関数の引数の型を明示しないので、単純型システムといってもプログラムに導出させるには型推論が必要になります。最後の章に型推論のアルゴリズムが載っているので実装しましょう。
さて、TypingML4は多相性こそありませんが、それでも型推論のアルゴリズムにはPolyTypingML4で定義される型変数を用います。すると式と型環境の情報だけでは型が代入されない型変数が現れることがあります。
最も単純な例はfun x -> xという関数です。
次の判断に対しては、
|- fun x -> x : int -> int
次の導出が与えられます。
|- fun x -> x : int -> int by T-Fun {
x : int |- x : int by T-Var {};
};
一方、次の判断に対しては
|- fun x -> x : (int -> int) -> (int -> int)
次の導出が与えられます。
|- fun x -> x : (int -> int) -> int -> int by T-Fun {
x : int -> int |- x : int -> int by T-Var {};
};
与えた型環境と式は同じなのに導出が違いますね。導出に:以降の情報を必要とするやつです。EvalRefML3で同じようなことがありました。
さすがに今回EvalRefML3で行ったような邪悪な方法は使わないし、それはおそらく不可能です。型変数が型推論の結果に現れたときは、求める型(と終端記号)を入力してもらって、それらを対応づける型の連立方程式を組んで導出を書き換えます。
それから、型変数が内側に残ることがあります。次のような場合です。
|- (fun x -> fun y -> x) 1 (fun x -> x) : int by T-App {
|- (fun x -> fun y -> x) 1 : ('_a4 -> '_a4) -> int by T-App {
|- fun x -> fun y -> x : int -> ('_a4 -> '_a4) -> int by T-Abs {
x : int |- fun y -> x : ('_a4 -> '_a4) -> int by T-Abs {
x : int, y : '_a4 -> '_a4 |- x : int by T-Var {};
};
};
|- 1 : int by T-Int {};
};
|- fun x -> x : '_a4 -> '_a4 by T-Abs {
x : '_a4 |- x : '_a4 by T-Var {};
};
};
PolyTypingML4ならこれで正解なんですが、TypingML4に型変数はないので不正解になってしまいます。このような型変数はintかboolで塗りつぶすとよいです。
PolyTypingML4
let多相の型システムを扱う導出システムです。プログラムで解くために実装するのはHindley-Milner型推論ってやつでしょうか？
互換性
TypingML4で型付けできる式はすべてPolyTypingML4で型付けできますが、それはそれとして導出の形式をみるとTypingML4とPolyTypingML4に互換性はありません。しかも式や型環境から両者のどちらを使うべきか判別することができない場合があります。仕方がないのでコマンドライン引数--no-polyを用意して、どちらを使うか指示できるようにしました。
ところで、TypingML4のT-FunはPolyTypingMLでは何故かT-Absに名前が変更されています。謎です。
型変数の名前
PolyTypingML4には型変数があるので、名前付きの型変数が与えられることがあります。一方で、型推論の過程で新しい型変数を生成するということもあります。
両者を明確に区別するために、型変数を表す型の定義は次のようにしました。
type t = Generated of int | Named of string
そして、型の連立方程式で「型変数どうしが等しい」という関係が現れたら、名前付きの型変数が優先的に生き残るようにします。こうすることで演習システムに怒られない導出を吐けるわけです。
ちなみに型変数を生成するコードは以下のとおりです。副作用バンザイですね。
let varnum = ref 1
let generate () =
let v = !varnum in
incr varnum;
Generated v
EvalContML1
継続(continuation)という概念を扱う導出システムです。導出がほぼ一直線になります。
どうでもいいんですが、わたしはEvalContML系列は継続渡しスタイルで実装してみました。
コードの再利用
これもEvalML系列とは大きく異なる導出システムですが、式(Exp)や値(Value)は共通しているので、それらのコードを再利用することができます。
導出システムの判別
構文は継続を書けるように拡張されていますが、空の継続を省略することが認められていて、省略されるとEvalML1と見分けがつかなくなってしまいます。そのせいで入力からEvalCont系列であることを判別できないので、諦めてコマンドライン引数--contを用意しました。
EvalContML4
第一級継続を扱う導出システムです。Schemeとかにあるやつですね。
互換性
EvalContML4には環境があって、これは省略できないので、EvalContML1と互換性はありません。まあ環境をoption型で持ったりしてどうにかすればコードはほとんど再利用できます。
循環参照
継続をContモジュール、値をValueモジュールで管理していると、第一級継続を導入するときに循環参照が発生します。わたしは再帰モジュールにして解決しました。
切り捨てた導出システム
Nat系列
これらは全て人力で解き終わっていたので実装しませんでした。
導出システムの数が多いわりに問題数は少ないのでプログラムで解かせる必要はないんじゃないかと思いますが、うまくコードを再利用すると早いかもしれないですね。
EvalML1Err
推論規則の数がやたら増えるから、という理由で実装しませんでした。
EvalMLでは推論規則の名称をヴァリアント型で表していて、推論規則が大量に増えると型の定義が大きくなって大変だったのです。今思うと、推論規則の名称はそのまま文字列で表すべきでした。
NamelessML3
NamelessML3は環境と式を名前無し表現に書き換えるだけなので、それほど大変ではないだろうと考えて人力で導出しました。
EvalNamelessML3
実はEvalNamelessML3用のブランチがこっそり切ってあって、そこに実装してあります。
なぜ分けてしまったのかというと、EvalNamelessML3の構文はEvalML1の構文(環境なしに式から書き始める構文)とshift/reduce conflictを引き起こすのが理由なのですが……
- なぜコマンド引数で分岐することを検討しなかったのか
- なぜ人力導出が容易なEvalML1ではなくEvalNamelessML3を切り捨てたのか
このように2点ツッコミどころがあります。しかし解いてしまったモノを再実装するのも面倒なので放置中です。
While言語
もはやMLではないので、別にプロジェクトを用意してOCamlで同じように実装しました。
While言語は関数がなかったり、intとboolが構文レベルで区別されてたりするので実装は簡単な癒し系です。実装にかかった時間は3時間くらいでした。
雑記
menhirのコンフリクト情報を得る
パーサジェネレータのmenhirがわけのわからんコンフリクトで文句を言ってくる、というときは--explainオプションをつけることで大変わかりやすい説明を.conflictファイルに吐いてくれます。duneでビルドする場合次のような設定を書きます。
(menhir
(modules parser)
(flags --explain))
演算子優先順位と入出力
本で与えられる定義に括弧は書かれていないからつい忘れてしまうのですが、リストの値(1 :: 2) :: 3とか関数の型(int -> int) -> intとかを出力するときには括弧が必要になるし、パーサも括弧に対応させておく必要があります。
式の出力は優先順位がだいぶややこしいです。例えば、負数の優先順位が関数適用より低いということを忘れるとf (-1)がf -1になって怒られたりします。式を与えると優先順位を吐く関数を用意して括弧付けを一般化すると楽になります。
