TAPLの実装を写経する - Scala で TAPLを勉強しつつ LLVM コンパイラを作る日記

今日も https://github.com/ilya-klyuchnikov/tapl-scala/ を写経しました。

なんで、TAPLを読んでいるのかというと、俺俺コンパイラを作る為に型理論の勉強が必要だからです。でもTAPLをすぐに読める状況ではないので何が書いてあるのかを把握する為に、実装を見て見てます。
TAPLの集合論とかを理解するには、プログラマ的にはCoqを使うと良さそうなのでCoqも勉強しています。実装が分かって、理論的な事を読む基礎知識が身に付いて、ようやくTAPLを読む事が出来る訳で、今はTAPLを読む為の修行中って感じです。でもまぁ、修行もまたTAPLを読む一環ではあると思います。

simpleboolを写してみたので次はfullsimpleです。
fulluntypedを元にfullsimpleを参考に_06fullsimpleに書き換えました。
本ではsimpleboolの拡張って書いてありますけどsimpleboolを拡張するより、たぶんfulluntypedを拡張した方が楽なんじゃと思って実際そんなかんじでした。

理論/実装/処理系上で動くソースっていうメタな階層構造になっているわけですが、メタなレベルの低いソースの例を見て見ましょう。

fulluntypedでは、以下のようなソースが動いてたわけですが、

https://github.com/ilya-klyuchnikov/tapl-scala/blob/master/examples/fulluntyped.tapl

/* Examples for testing */
zz = (lambda x. x);
true;
if false then true else false;
x/;
x;
x = true;
x;
if x then false else x;
lambda x. x;
(lambda x. x) (lambda x. x x);
{x=lambda x.x, y=(lambda x.x)(lambda x.x)};
{x=lambda x.x, y=(lambda x.x)(lambda x.x)}.x;
"hello";
0;
succ (pred 0);
iszero (pred (succ (succ 0)));
let x=true in x;

fullsimpleでは、let recが入ったり、variantが入ったりしてます。
case ofでパターンマッチングもやってますね。本にはtupleも書いてあるんだけど、どうなんだろう？

https://github.com/ilya-klyuchnikov/tapl-scala/blob/master/examples/fullsimple.tapl

/*** FIXES, LETRECS ***/
let x = succ 0
in let y = succ x
in y;
evenodd = fix (lambda eo: {even: Nat -> Bool, odd: Nat -> Bool}.
{even = lambda x: Nat. if iszero x then true else eo.odd (pred x),
odd = lambda x: Nat. if iszero x then false else eo.even (pred x)});
evenodd.even (succ 0);
evenodd.even (succ (succ 0));
// letrec is just let with fix!
letrec even:Nat -> Bool =
lambda x: Nat.
if iszero x then true
else if iszero (pred x) then false
else even (pred (pred x))
in
even (succ (succ (succ 0)));

/*** RECORDS AND VARIANTS ***/
// Records
PhysicalAddr = {firstlast:String, addr:String};
// type is not saved during compution of ascribe term!
{firstlast= "lambdamix", addr="Russia"} as PhysicalAddr;
VirtualAddr = {name:String, email:String};
// Variants
Addr = ;
getName = lambda a:Addr. case a of
==> x.firstlast | ==> y.name;
"123";
pa = {firstlast= "lambdamix", addr="Russia"} as PhysicalAddr;
va = {name = "ilya", email = "ilya@ru"} as VirtualAddr;
addr1 = as Addr;
addr2 = as Addr;
getName addr1;
getName addr2;
lambda _: Unit. 5;
\_: Unit. 5;
let x = 5 in 7;
let _ = 5 in 7;

tupleは実装されていないのか疑問だったのでそれっぽい実装あるか見て見てたのですが、おそらく、実装されてません。
TAPLとtupleって似てますよね。
TAPLって略のAってaなんだろうか、Aなんだろうかって悩む所です。Aでいいみたいなんですけど。
でtupleは間違えてtapleって書いてしまったりと、uかaかで悩むんですけど、uが正解ってことで、えー似てるなぁと。小文字のaじゃないんだなと。だから？って言われると困るんですけど。

いや、TAPLの何がいいって、言語を関数型言語でどう考えて実装して行くといいのかが、勉強出来るってことですね。サンプルも豊富だし、理論的にも裏打ちされてるから凄い。もうMinCamlを見てるので最適化付きのコンパイラに比べたらインタプリタだから簡単だし。

とにかく、

cp -rf _05fulluntyped _06fullsimple

でコピッて全ソースのパッケージ名を変えて
で、fullsimple.taplをdemo.taplに書き換える。
で、syntax.scalaを書き換える。
次は、parser.scala
次は、core.scala
最後に、demo.scala
で実行してみて、バグ取りをして例がちゃんと動きました。

syntax.scalaの修正の詳細を書いてみると

sealed trait Ty
case class TyVar(i: Int, cl: Int) extends Ty
case class TyId(id: String) extends Ty
case class TyArr(t1: Ty, t2: Ty) extends Ty
case object TyUnit extends Ty
case class TyRecord(els: List[(String, Ty)]) extends Ty
case class TyVariant(els: List[(String, Ty)]) extends Ty
case object TyBool extends Ty
case object TyString extends Ty
case object TyNat extends Ty

増えたタイプはこんだけあります。tupleはないですよね。

case class TmCase(sel: Term, branches: List[(String, String, Term)]) extends Term
case class TmTag(tag: String, t: Term, ty: Ty) extends Term
case class TmFix(t: Term) extends Term
case object TmUnit extends Term
case class TmAscribe(t: Term, ty: Ty) extends Term
case class TmInert(ty: Ty) extends Term

termはこのくらい増えて、simpleboolと同様にTmAbsにタイプが追加と。

case class TmAbs(v: String, ty: Ty, t: Term) extends Term

BindingにはTyVarBindとTyAbbBindを追加 TmAbbBindにtyを追加

case object TyVarBind extends Binding
case class TyAbbBind(ty: Ty) extends Binding

case class TmAbbBind(t: Term, ty: Option[Ty]) extends Binding

という感じで全体的にtyの追加用のコードと諸々増えた型の対応をしました。
Typerはsimpleboolからコピーして拡張がいいんでしょうけど、
全体をコピペしてしまいました。

いきなり実装を見るのもずるい気もしてましたが、ここまで来ると実装見るだけでも大変です。自分で実装出来る気がしないくらい、凄い事になってます。でも、動いているんだからすげぇなぁっと思う訳です。

まだまだ分からない所がありますが、大分理解は進んだように思います。

https://twitter.com/search?q=%23tapl

ツイッターの書き込みでCoqでTAPLの授業を発見しました。

Takashi Miyamoto ‏@tmiya_ 10年10月11日
TAPLをCoqで扱っている授業のページ。ここの課題をCoqで実装するのがTAPLをCoqで復讐するのに楽かなー。 http://www.cs.helsinki.fi/u/lealanko/ftt09/ #TAPL #Coq

Coqのソースは見れないみたいですが、htmlは見れるようです。

http://www.cs.helsinki.fi/u/lealanko/ftt09/html/tapl_ch3.html
http://www.cs.helsinki.fi/u/lealanko/ftt09/html/tapl_ch8.html
http://www.cs.helsinki.fi/u/lealanko/ftt09/html/tapl_ch9.html
http://www.cs.helsinki.fi/u/lealanko/ftt09/html/tapl_ch12.html

とりあえず、Coqで入力してみると楽しいかもしれません。