| Edit this page | Report an issue |
この先読むと良さそうな本についてまとめた．プログラミング言語処理系の実装に関する本があまりないので，追加しないといかんなあ．
和書では
がおすすめである．サポートページもあり，かつ自分で導出木を書くオンライン演習システムもあります．
また，証明支援系 Coq を使って学ぶオンライン教科書としては（英語であるが）
がおすすめである．この教科書の Volume 2 まで問題を解いていくと，型の話を含むプログラミング言語理論の基礎の部分が自然に身につくだろう．
現在の型のスタンダードな教科書は
である．λ計算という関数型言語のコアを取り出した小さい言語で意味論を形式的に定義したり，型理論を展開したり，その性質を証明する方法が解説してある．この本をしっかり読むと，型を扱っている論文がまあまあ読めるようになるはず．この本は京大生であればKULINEから無料で電子版が読める．
東北大の住井英二郎さんらが和訳したバージョンもあるのだ．
これも KULINE から読めるはずである．
また，型理論の応用にカリーハワード同型 (Curry-Howard isomorphism) と呼ばれる性質がある．これは型理論と論理の間の対応を与えるもので，証明支援系の理論の基礎になったりしている．すごく雑に言えば，なにか型システムが与えられたときに，その型を命題だと思って，プログラムを証明だと思うと，証明システムが得られるし，その逆も行けるという話である．この話題に関する教科書としては
がある．プログラミング言語の世界の型理論の話と，論理の世界の意味論や証明論やの話を丁寧に説明した良い本だが，一人で読むのはなかなか大変かもしれない．これも KULINE から読めます．
また，型の最近の応用に篩型 (refinement type) がある．OCaml の型は int とか bool のようにざっくりと「整数値」「ブール値」のような分け方しかしないが，これに {x : int | x > 0} という「正の整数を表す型」のような，述語を用いて詳しい型を扱えるようにした型システムである．x > 0 の部分に任意の述語が書けてしまうと型検査や型推論は決定不能になるが，これにうまく制限をかけて結構いろいろ検証できるようにした Haskell の拡張 Liquid Haskell という処理系がある．チュートリアルがここにある．
また，篩型のような表現力の高い型システムにおける型検査には，能力の高い制約解消ソルバが必要である．このようなソルバは，例えば x >= 0 && y < x + 1 && z < x みたいな制約は充足可能かどうかを検査したり，充足可能だとしたときに x,y,z への可能な代入を返すとかができる必要がある．このようなことができるソルバとして SMT ソルバと呼ばれる SAT ソルバを線形不等式や文字列等に関する述語を扱えるように拡張したソルバ用いられている．一番広く用いられている SMT ソルバが Z3 である．これが自分でも使えると，いろいろな検証器が作れたりする．OCaml からも使えるが，Python からも使うことができて，Python を使ったチュートリアルがここにある．使ってみると面白いかもしれない．（MiniML を篩型を使って拡張するみたいなパートを誰か書いてくれ．）
もう少しマニアックな言語がお好みであれば， F* という言語をやってみると面白いかもしれない．副作用を持ちうるプログラムの性質を保証するための証明支援系で，OCaml に似た文法を持っているが，篩型や副作用を表す型などを用いていろいろなプログラムのいろいろな性質が検証できる．この言語を用いて開発されたプログラムとして有名なのがHACL*という暗号ライブラリで，Firefox 等でも用いられている．これもチュートリアルがここにある．（あまりドキュメント化されていない言語なので，やるならば茨の道を進むつもりで．）