概要

2018年3月11日から4月14日まで楽天技術研究所でEgisonの型システムの設計 & 型検査器を書くインターンをしていた。もうインターンから半年も経ってしまったが、何も書かないよりはましというわけでブログ記事を書くことにした。

実装した型検査器はここにある。まだまだ不完全ではあるが、一応動くのでよかったら試してみてほしい。

Egisonとは

Egisonとは江木さんという方が開発しているLisp likeなプログラミング言語で、非常に強力なパターンマッチ機構を持つ言語である。江木さんは2007年からほぼ一人でEgisonを開発し続けており、その歴史はここで見ることができる。最近ではパターンマッチ機構を活かして、数式処理システムの制作に使われている(江木さんがつかっている)。

インターンが始まるまで

楽天技術研究所では，現代数学を簡潔に記述するためのプログラミング言語EgisonをHaskellで開発する方(アルバイトやインターンなど)を募集しています．
Haskellで言語実装することに興味ある方は，ぜひDMください！
— Egison (@Egison_Lang) 2017年11月13日

Twitterをぼんやり眺めていたら「Haskellで言語実装するバイトがある!」ということで即応募した。 DMを送ったらSkypeで面接することになって、そのまま採用してもらった。普段は京都に住んでいるので、東京に行かずに済んだのはすごく助かった。

採用が決まった後は、Egisonが微分幾何の記述に使われるということなので局面と曲線の微分幾何を読んでいた。研究室でPPL2018に行ったら隣の席に江木さんがいて、そのとき初めて江木さんに会った。

インターン初週

インターン初日、東京で疲れてしまったのか、高熱と吐き気がして会社を休んだ。社会人失格かと思ったが、次の日出社したら「大丈夫ですか」と気遣ってくれて嬉しかった。後でTwitterを見た感じ、東京で風邪が流行っていたらしい。

インターン初週はEgisonの実装を読むことが主な業務だった。 Egisonは巨大な構文木インタープリタとして実装されており、相次ぐ機能の拡張によってエライことになっていることが分かった。

インターン2週目

江木さんがEgisonに型検査を入れたいというので、Egisonのサブセットを抽出、定式化をして、そのサブセットに対して型システムを設計しようという話になった。 Egisonにはmatcherやprimitive patternなどの通常の言語には無い構文要素があり、ちょっと大変だった。

この週の金曜日、江木さんが東大の出身研究室(萩谷研)を訪問するというのでくっついて行った。萩谷研では、Egisonの意味論をどう定義するかという話をしていた(僕は議論する様子を眺める係をしていた)。この議論は後々論文になり、APLAS 2018に採択されている。

インターン3週目

2週目に設計した型システムを型検査器として実装した。基本的にはHM型の制約解消アルゴリズムで実装したが、型付けできない式を受理するためにワイルドカード型を入れたりした(Egisonはもともと型なしの言語なので、型付けできないが動く式が基本ライブラリ中に存在する)。当時は知らなかったのだが、あとで確認してみると漸進的型付けの型検査と同じような実装になっていた。