Scala で TAPLを勉強しつつ LLVM コンパイラを作る日記

■ 関数ポインタを弄る

コンパイラを作り、SML#を勉強し、コンパイラをLLVM化し、TAPLを読みつつ、Coqを勉強し、集合論を勉強し、、、疲れました。

そこで、気分転換にスタックマシン的なLLVM用のコンパイラの関数ポインタをこうすればうまく行くんじゃないかなと思ってたので修正をしてみたところ、特に悩む事もなく対応出来てしまいました。

関数の型 TFun(Tv,List())みたいな物が()=>voidになるってだけで、LLVMのコード上ではvoid()*とポインタになるというのでうまく行くんじゃないかと思っていたのですが本当にそうでした。構造体内の関数ポインタも使えるようになりました。

immutableはないですけど、普通にゲームは作り進められそうです。

■ 「集合とはなにか」を読んでます。

面白いです。良くわからないので何回も見直してます。

ついでにと思って、「層と圏とトポス」も買ってみました。

集合がある性質を表す物の集まりなんだけど、それを色々拡張して行くと、この方が便利だ、あの方が便利だって話になって行って、圏論が産まれてHaskellはその圏論を元にした言語だってことなんだろうなぁと。圏論はそういう事で素晴らしい者なんだろうなぁとは思うのですが、コンパイラを作る上で無くてはならないものではないので、とりあえずおいておこうと思います。ここで圏論に行くと、HaskellかScalazかっていう話に進むんでしょうけど。

例によって分かる範囲で、まじめに読んで、途中から眠くなって来たので斜め読みで最後まで見ただけなので、詳しい理解は出来てないのですが、記号は覚えても忘れそうだけど、スラスラ読めてよかったです。

古典集合論→ZF集合論→位相空間→層→圏→トポス

群が抜けてますけど、どうなってるか良くわからないのでいいやと。

量子集合論みたいなのも展開出来るはず見たいな話が書いてあって、今どうなってるとか全然知りませんが、線形代数を基礎にしている量子力学とはまた違った、非連続的な量子力学の理解とかに繋がるのかなぁとか名前だけ見て思ったのでした。

ということで、ググってみると、おお、量子集合論の論文とかがあって、面白いですね。量子力学の実験結果を元に、事実である命題として集合論を作る際に使っているのかな？

量子化とかは、こうして見ているパソコンのグラフィックスも、デジタルな音声も全て量子化された情報なのですぐにどうこうってわけではないかもしれませんけど、いろいろと役に立ちそうです。

多分、夢の除染装置であるコスモクリーナーを実際に作る場合もも量子化された原子のサイズが重要な鍵となってるんじゃないのかなっと。

あと、物語としても面白くてよかったです。

で、こちらの方面も色々見て見ててまとめられると面白いだろうなぁと思ったんですけど、やっぱり、コンパイラ造りに直接必要ないので、そこそこにしておきます。やる気がなくなったらみてみよう。

一階記述論理をゲーデルって人が考えて、その友達がこの本の作者ってことなのかな？

凄い人だし、何を考えて集合論が出来て来たのかがずいぶんわかりました。

でも、Coqをやってから見てるので、集合と命題については分かるけど、動的言語で書かれているので分かり辛いんだなと思いました。SetとPropがあるけどTypeがないから分かり辛いんで。

集合と命題に型を加えた理論が欲しいってなると型理論になるわけです。型理論はどうも、ラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築したそうです。でも、不確定性定理は存在しうるのでどうこうって話になってるらしいと。

そして、型システムは型理論を形式的な言語の基盤にしてるらしいと。

Coqを理解していけば型理論について理解が進む事になるし、型理論があると集合論も分かりやすくなる部分もあるけど、全てを表す事が出来る訳ではないのかな。

動的なCoqみたいなので、集合を記述出来たら良いんでないかなぁと思います。そういうのが出来るかどうかもわからないですけど。型はあるけど、明示されないって感じになるのかな？

要するに、型のない世界で普通に集合論があって、そこで型を追加して言語を作るのが型理論の話で、型理論を使って証明出来る事を使って作った言語がCoqなので、型理論の後の話がCoqなんだけど、型がある方が分かりやすいって事もあるよと。

RubyとJavaでJavaのほうが分かりやすい事もあると。

そんな話でした。

あと、不確定性定理をゲーデルさんが考えたそうなんですが、不確定性原理と観測問題（かんそくもんだい）とかと似通ってるのかなぁ。名前も似てるし。原理と定理は別に２つあるんですね。とか、観測する事で位置が決まる。観測しない間は、確率でしかない。とかいうのは、遅延評価だよなぁとか。

数学者が結構精神的に弱る人が多いみたいなんだけど、それもまた、脳内のシナプスの使い方が、論理的な事を考えるように最適化されて行った結果なんじゃないかなぁとか、思ったりしました。

高速に演算する為に、３つも４つもの同じような回路を使っていた物を、１つで、すぐに結果が出るようにして行くと、日常生活が困難になる方向に進んで行ってしまうとかあるんじゃないのかなと。

論理的に正確さを求めて行くと、不正確であるものの存在を認めざるを得なくなるのだと気がついて、そういう目で周りをみると、１００％なんてあり得ないのに、100%の自信を持って話す人がいて、それが信用ならないってことになり、人間不信になって行く。

そういう話なのかなと思ったりしました。

あと、強いエネルギーを持っている物の存在確率の半径みたいなのは広いとかなんとからしいんですけど、そいつを観測するとなると、行動範囲を狭められるので、嬉しくない。

確率的に、その狭い範囲にいる確率は減るので、スケジュールにあわせるのが辛くなるとかで、遅刻とかしやすくなってしまう。でも、それが駄目だっていう世間の目と、そんな事いわれても時間にあわせるのが大変なんだっていうのとのギャップもまた、苦しむ原因の１つなんじゃないかと。

体調が良くないと動けない人に、スケジュールぴったりに動けというのは酷だって思うのでした。それが出来る人はいいけど、出来ない人に取ってそいつは辛い話なのですよ。

大物ぶってるわけでもなく、動けない人は色々理由があってうごけないんだよなぁ。スケジュールがぴったり守れることは良いことですけど、それだけを物差しとして、友達を選ぶような人達とは残念ながら友達になれそうにないって思ったりするのかなと。

権威に興味があるのであって、俺個人に興味がある訳ではないだろうとか。ってほとんど愚痴になってしまってますけど。

■ Coq の コアライブラリ(Prelude)を見て数学が分かった気になる

集合はどうも、数学の基礎にあたるようです。でも、集合を把握すする前に「定義、公理、命題、定理とは何か？」を把握すると良いです。この辺の話はCoqの構文を覚えることでプログラミング言語を覚えるように覚えることができます。

http://homepage3.nifty.com/rikei-index01/biseki/bisekiteiri8.html

集合論は型理論の基礎的な知識だそうですが、集合の前にある前提として論理とか、自然数の足し算やかけ算等があるようです。Coqで一からどう形作られているかを見れば、その関係が分かるはずです。

http://coq.inria.fr/stdlib/index.html

Init: The core library (automatically loaded when starting Coq)

Notations Datatypes Logic Logic_Type Peano Specif Tactics Wf (Prelude)

Coqで集合のライブラリを遡るとCoqのコアライブラリに行き着きます。

Coqが開始すると自動的にロードされるライブラリがコアライブラリであり、Preludeにまとめて書いてあります。

http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Prelude.html

Library Coq.Init.Prelude

Require Export Notations.
Require Export Logic.
Require Export Datatypes.
Require Export Specif.
Require Export Peano.
Require Export Coq.Init.Wf.
Require Export Coq.Init.Tactics.
Add Search Blacklist "_admitted" "_subproof" "Private_".

Notations で記法(演算子の定義)がされていて、

Logicで論理的な定義、

Datatypesでデータの型、

Specifが基本仕様、

Peanoで、ペアノ数、

Wfで整礎関係 Well-founded relation や整礎帰納法 Well-founded inductionについて

Tacticsでタクティクが定義されていて、

検索から_admitted, _subproof Private_は検索されないように定義されています。

Ligic_typeはPreludeに書かれてませんが、最初に読み込まれるそうで、論理の型ってことでしょう。

Notationsを見て見ます。

http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Notations.html

Reserved Notation "x <-> y" (at level 95, no associativity).
Reserved Notation "x /\ y" (at level 80, right associativity).
Reserved Notation "x \/ y" (at level 85, right associativity).
Reserved Notation "~ x" (at level 75, right associativity).
:

ずらずらと、演算子と、優先順位、結合法則が書かれてます。

基本的な演算子はここで全て定義されている訳です。

Logicを次に開いてみましょう。

http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html

(* Propositional connectives *)
(* 命題の結合 *)

(* True is the always true proposition *)
(* Trueは常に真の命題 *)
Inductive True : Prop :=
  I : True.

(* False is the always false proposition *)
(* Falseは常に偽の命題 *)
Inductive False : Prop :=.

(* not A, written ~A, is the negation of A *)
(* Aでなければ、Aならfalse *)
Definition not (A:Prop) := A -> False.

Notation "~ x" := (not x) : type_scope.
(* ~ x は not *)

Hint Unfold not: core.
(* ヒント 逆展開 not: core *)

(* conjection 論理積 and型 *)

(* 定義 and A B : A ⇒ B ⇒ A ⋀ B *)
Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B
:

Coq立ち上げ時にはこのような沢山の定義や定理等が読み込まれます。

このような数学的な土台の上に、集合(Coq.Sets.*)が定義されているわけです。

全てを覚えるのは難しいですが、こういう構造だと理解したのであれば、それで十分ではないかと思います。後は、必要になったら見ればいいのです。

Javaだって、全てのAPIを覚えないですよね。

基本的な構文を覚えて、よく使うライブラリを覚えれば、あとは必要なときにライブラリを探せばいいのと一緒です。

そして、TAPLの2章についても、必要になったら見れば良いライブラリという認識をしておけば十分ではないかと思います。

という悟ったような状態になったのが今日の収穫です。

全てを理解した訳ではないし、全部を覚える事は出来ないけど、論理を決めて、論理で使う型を決めて、基本仕様を決めて、自然数を決めて、関係とかを決めて、タクティクを決めて、論理の型を決めてから、集合や関係、関数、順序集合、列、帰納法等の上に、型理論を構築するんだ、という事が分かったので、ずっと、気が楽になりました。

■ TAPL２章が分からない8つくらいの理由

全体像は分かって来たので理論的な所も読みたくなってきました。

2章にはTAPLで使う定義がまとめてあり、必要なときに見ればいいと書いてあります。しかし、出来れば理解したい所です。でも覚えられない。

何が分からないのかが分からない状況です。辛い理由を考えて、それに対応することで分かるようになりましょう。

■ 分からない理由1 形式的な言語が分からない

まず、このような問題については檜山正幸さんの ーーー 「形式的」とは何だろう ーーー があります。

http://www.chimaira.org/docs/FormalReasoning.htm

形式的なモデルを使うのに慣れてないのが１つの答えです。このページを読むと形式的な文章が読みやすくなります。いくつか別のモデルを示されていて、それぞれ別の意味を持つことが書いてあるので分かります。

1+1は2とは限らないし、定義が無ければ意味がまったくないかもしれないってことが分かれば良いのだと思います。

それは分かってるんですよー。

■ 分からない理由2 全体像が把握出来てない

全体像が把握出来てないとどのくらい進んでいるのかも分からず焦ってしまいます。そんな時は、まず全体像を把握しましょう。

• 2.1 集合と関係と関数
• 2.2 順序集合
• 2.3 列
• 2.4 帰納法

集合はJavaのコレクションでいうとSetです。関係とはMapみたいなもん。関数は関数ですね。順序集合ってのは、集合の関係について順番を入れ替えたりした時の挙動とかを決めてます。

列はLispとか関数型言語で使うリストのことですね。

帰納法は、再帰的にグリグリと回って、最後にゼロとか、nilとか空のリストになる再帰的に証明するやり方ですね。この本でどんな証明をするかが書いてあると。

大体こんな感じという所までは分かるようになりました。

■分からない理由3 標準的な集合の記法が書いていない

2.1.1で集合は標準的な記法を用いると書いているので、これが分からないんですね。標準的な方法を知らないので、分かる訳けないですね。

標準的な集合の記法を覚えよう！！

「プログラミング言語の基礎概念」や「プログラミング言語の基礎理論」、「論理と計算の仕組み」、「プログラムの意味論」が良いそうです。

集合の基礎的な所を勉強しましょう。

wikipedia:

http://ja.wikipedia.org/wiki/%E9%9B%86%E5%90%88

http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/class/sf05w/resume1.pdf

ノートに図を書いたり、色々調べて大分覚えました。

■分からない理由4 すぐ実装してみることが出来ない

Coqのような定理証明系の言語を覚えれば、理論や証明をコンピュータ上で実装してみることが出来ます。

覚えるのには時間がかかります。地道に勉強しましょう。

昨日は、Coqチュートリアルをやってみました。

以下のようなファイルを用意して、CoqIDEで上行ったり、下行ったりして眺めています。

続きを読む

■分からない理由5 記号を覚えられない

システムを作る際には仕様書を作って実装をするわけですが、仕様書にはそれほど記号は出てきません。理由は演算子を使えないとか、使えても限りがあるからです。そのシステムを作る為の演算子を使うってことはあまり多くないのです。

記号は使わずに、英単語で覚えることに慣れているので記号と意味と英単語の表を書くと理解に繋がるようです。

また数学的記号の多くは漢字と同じような表意文字です。ただ、元となる文字がアルファベットであったり、英単語だったりするので英単語と対で覚えると楽です。

■ 定義2.1

S T U	Set	集合
R	Relation	関係
f(x)	Function	関数
x s t u	Element	要素

集合と関係と関数、要素は英語でなんと言うのかまとめてみました。

関数がFunctionと、要素はElementは有名だと思います。

関係はRelationで集合がSetが繋がってない人は多いかもしれません。

■ 定義2.1.1

{...}	Enumeration	列挙
{x ∈ S｜...}	Comprehensions	内包表記
x ∈ S	x is element of S	xはSの要素
∅	Empty set	空集合
S ∖ T	Set Minus	差集合
S ∪ T	Union	和集合 UnionのU Andの反対でOrな感じ
S ∩ T	Intersection	積集合 共通部分,Unionをひっくり返したものAndのAっぽい

集合については標準的な記法を使うってことで、標準的な集合についても調べてみました。

Union,Intersectionは知ってるのですが、∪と∩がunionとintersectionなんだぁと、改めて実感しました。∈はelementのeなんですね。

■ 定義2.1.2.

N	Nat (Natural number)	自然数 0,1,2... ホントは2重線のNです
-	countable set	可算集合 自然数と一対一に対応付けられる集合

■ 定義2.1.3.

R ⊆ S1×S2×...×Sn	n-ary relation	n項関係
⊆	subset of or eauql to	サブセット
s1∈S1...sn∈Snに対して(s1,s2...sn)がRの要素	n-ary relation	要素(s1,s2...sn)はRによって関係ずけられる
単項関係 項が１つだけの関係
S上の単項関係	S上の述語

今までは∈??なんだっけ、このヨのひっくり返したような奴？ってなってたのですが、∈はelementの略で要素だと覚えればもう忘れません。elementはHTMLのDom操作でもう慣れてますからね。

内包表記はhaskellで使えるそうなので覚えてます。コンプリヘンションズって読むのかな？集合はSetだってなれば、只のJavaのSetねで覚えられるんですね。Mapは写像の集合で、Listはリストなのかな。間違えてたらすいません。

こんな感じで進めるといいんでしょうね。

全部出来てない当たりが、甘いんだろうなぁ。

■ 分からない理由6 定義や定理、補題、命題、証明がごちゃまぜになっている。

恥ずかしい話ですが、定義と定理の違いが良くわかってませんでした。

出来るだけ避けるべき存在になってました。

でも、Coqをやってみて考え方が変わりました。

定義とか定理とかは、typedefとかdefとかのようなキーワードであり、構造化された文章を書く為の構文の１つと捉えるといいようです。TAPLはドメイン特化言語を使って書かれていると考えると楽しいです。文法を定義してもいいんですけど、文法を見ても分かりずらくて、例が有るのが分かりやすいんですよね。

良書

　謝辞

　目次

　第1部 ほげほげ

　3章 ほげほげ

　　3.1 ほげ

　　ほげほげ

　　　定義3.1.1　ほげほげとする

　　　補題3.1.2 [ほげのほげげ]

　　　[証明]ほげほげはほげゆえにほげである。よってほげ。

　　　定理3.1.3 [ほげのほげほげ性]

　　　[証明]ほげほげはほげゆえにほげである。補題3.1.2によりほげなのでほげ。

　　　演習3.1.4 [推奨, ★★]ほげ

　　　演習3.1.5 [★]ほげ

　　　演習3.1.6 [★]ほげ

TAPLの場合、定義3.1.1とか補題3.1.2のような項目はまるでCoqで書いたプログラムのように見えます。

で、定義とか命題とか、仮定とかその辺が訳が分からないので分かったつもりになるとずいぶん、眠くならなくなりました。

定義	Definition	CoqではDefinitionは関数の定義、Inductiveは型の定義,Variableは変数の定義, Fixpointは再帰関数の定義
命題	Proposition	証明するための論理的問題
仮定	Hypothesis	真偽はともかくとして、何らかの現象や法則性を説明するのに役立つ命題
公理	Axiom	その他の命題を導きだすための前提として導入される最も基本的な前提のない仮定
定理	Theorem	公理を前提として演繹手続きによって導きだされる命題
補題	Lemma	定理を証明する為の証明されている命題
系	Corollary	(ある定理から直ちに導かれる定理)
事実	Fact	カエサルは殺された
注意	Remark
演習	Drill	学習するために行う計算。
ヒント	Hint	自動証明(auto)で使われる定理をヒントDBに登録する
慣習	Convention	同意、規定あるいは一般に受け入れられたしきたり、規範
例	example	実際に使った場合にどのようになるかを示したもの
解答	Result	演習の答え

定義は前提無しに決めたことです。定義は、命題だけではなくて、関数や型や値も決めることが出来ます。命題を定義した場合は、証明を行うことが出来ます。

命題は証明をすることを試みることが出来ますが、必ず証明できるわけではありません。型がProp(命題)な定義は命題です。命題を評価することは、証明することになります。（カリーハワード対応）

証明出来る命題を定理とか補題とか系等と言います。

公理は証明は出来ていないけど、自明な命題のことです。

公理は証明出来ると定理と呼べるが、２つの公理が同じ意味を表す場合は、どちらか一方の公理を使えば、もう一方の公理を証明出来る。また、公理を使って定義された定理を使って公理を証明することも出来るのです。

この辺を理解してしまえば、多分、TAPLは大分読み進めるはずです。

■分からない理由7 反射的に眠くなるように訓練されている

この説明をだだだっと、姉にしてみた所、倒れて「眠い。授業したらすぐに寝れる教授になれるよ。」と言われたのでした。

どうも、ああ駄目だ、理解出来ないでも、話は進んで行くとなんともたまらなく眠くなるように訓練されてしまっているんじゃないかと思います。もう、こういうムツカシー本は分からん。寝る。と反射的になってしまう。

これを克服するには、他の分からない理由で述べた方法で、眠くならないようにしましょう。

■分からない理由8 演習をやってない

演習は、本を書いた人が学習する為に繰り返し覚えるといいよって思う所を問題として出している訳です。問題なのですぐ答えが出せる訳では有りません。答えを見ようと思えば答え乗っていれば見れば言い訳ですが、問題意識を持ってみることが大切です。演習は答えが乗っていれば例にあたるので、考えるのが嫌なら、演習が出て来たら答えを見ましょう。

って感じの文章をもっとちゃんと奇麗にまとめると良いと思うんですけど、ま、日記だし、いいやということで。先に進みたいと思います。

■ TAPLの実装を写経する

今日も 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 = <physical:PhysicalAddr, virtual:VirtualAddr>;

getName = lambda a:Addr. case a of

<physical=x> ==> x.firstlast | <virtual=y> ==> y.name;

"123";

pa = {firstlast= "lambdamix", addr="Russia"} as PhysicalAddr;

va = {name = "ilya", email = "ilya@ru"} as VirtualAddr;

addr1 = <physical=pa> as Addr;

addr2 = <virtual=va> 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で入力してみると楽しいかもしれません。