『プログラミング言語の基礎概念』で型推論を実装する
出版社のページ プログラマーとして働いておきながらいまさら「基礎」かと思われそうなタイトルの本書ですが, 「プログラミングの基礎」ではなく「プログラミング言語の基礎」であることがポイントです. プログラミング言語を数学的に厳密に扱う意味論や, エラーを事前に検知するための型システムについての本で, プログラミングの入門本ではありません. 本書では序盤中盤に書けて, プログラミング言語分析のための枠組みについての説明がされていますが, メインは型システム, 型推論だと思います. プログラムの実行や型推論の仕組みについて厳密に扱う方法を知りたい方におすすめです. 対象としている言語は OCaml なので, ある程度 OCaml についての知識があったほうが理解がスムーズだと思います. 分析については基礎から解説してあるので, 前提知識は不要です. 導出システムについて 本書ではプログラムを厳密に扱うための枠組みとして導出システムを使います. 導出システムとは, 定義されたいくつかの規則に従って定理を導出する記述体系です. 本書の流れに沿って, 実際のプログラミング言語を扱う前に, 自然数の加算乗算を対象とした導出システムの例を見ていきます. 自然数を対象とした導出システム (natural numbers から Nat と名付けられている) では簡単のために S(...S(Z)...) のような記法で自然数を表します. 例えば以下のような感じです. 1 2 3 0 -> Z 1 -> S(Z) 2 -> S(S(Z)) 導出システムによって導出される結論を「判断」と言います. Nat での判断は以下の 2 つの形です. n1, n2, n3 は自然数で, 2 つの判断はそれぞれ加算と乗算に対応しています. 1 2 n1 plus n2 is n3 n1 times n2 is n3 式を変形するための規則「推論規則」は以下の 4 つです....