Arantium Maestum

プログラミング、囲碁、読書の話題

簡単な型システムを実装していく１　序文

型理論 言語処理系 OCaml

最近は言語処理系に関してまったく手を動かしていなかった＆ブログに何も書いていなかったので練習がてら・・・

Types and Programming Languagesには非常にたくさんの型システムの実例と関連したOCamlコードが載っている。ただし多くは写経したらそのまま実行できるものではなく、また本に載っている型システムすべてについて実装が載っているわけでもない。

著者Benjamin Pierceの大学関連のホームページにTaPLのサイトがありそこにはほぼすべての型システムのテストコードなども含んだ完全形とも言えるソースがある：

www.cis.upenn.edu

これらを一つ一つDL・解凍して読んでいくのもいいのだが（というかやった）、

と誰かがGithubにあげているのを発見した。やはりパッとコードを参照したいときにGithubで読めるというのは大変ありがたい。

その旨ツイートするとさらにありがたいことに以下のレポジトリを教えていただいた：

TaPLのサンプルコードは実際いろいろと手がこんでいて、de Bruijn index化やら、エラー処理のためにパーサからのトークン位置情報が至るところに埋め込まれていたり、それなりに大規模な言語処理系としてもしっかり通用するようなフォーマットになっている。「なるほど、こうやるのがいいのか」と感心する反面、型システムそのもののコアなアイデアを学習したり、自分のプログラムに追加するために参考するのには、邪魔になってしまうようにも思う。

なので以下のような形でスッキリ整理されているのは大変ありがたい：

github.com

（上記のレポジトリではそこからさらに進んで型システムのメタ言語などがほぼそのまま論理プログラムとして直訳できる、という話にまで踏み込まれているので興味のある方は是非ご覧になってほしい）

これをベースに、さらに切り詰めて型システムのコアがわかる最低限を段階的に実装していこうと考えている。

まず手始めに、simpleboolと呼ばれるもの相当のSTLCに真偽値が加わったものを30行のgistにした：

gist.github.com

解説は次回。