外部swfのリンクに成功した(id:mzp:20091108)ので、swf生成に関する課題がおおむね片付きました。残る課題は、最適化やライブラリの充実などの作り込みに関する部分なので、そろそろHappyABC 1.0の完成が見えてきました。
というわけで、ぼちぼちとHappyABC 2.0の準備を始めています。
HappyABC 1.0の目的はswf生成に関する、いわゆるバックエンド部分の構築でした。対して、HappyABC 2.0の目的はずばり型システムの導入です。
そもそもHappyABCを作り始めた動機の1つがActionScriptの貧弱な型に嫌になった、というのがあるので、型システムの導入は絶対に必要です。
ただ、HappyABCの設計方針は無茶をしないなので、HappyABCオリジナルの型システムを構築するつもりはなくて、一般的に使われているlet多相を借りて来るつもりです。
とはいうものの、Flashにしかない概念もあるので、let多相をある程度の拡張するのは避けられません。ただ、そうなると拡張したlet多相が正しいことの証明がどうしても必要になってしまいます。
ただ、紙と鉛筆だけでちゃんした証明ができる自信もありません。たぶん、どこかで間違えると思います。
というわけで、定理証明機であるCoqを使って、ラムダ計算に関する諸定理を証明する練習をしています。その成果はmzp/lambda ? GitHubで見れます。