型システムとは、プログラムの各部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法である。
「型システム入門」より
概要
Erlangの型検査ツールであるDialyzerの振る舞いを理解したいという目的でソースコードを読みます。対象とするOTPバージョンは21.1.4です。
対象とする読者
- Dialyzerの挙動を学びたいErlangプログラマー
- 型システムに興味のある人
Dialyzerの中身
おおざっぱなコールグラフを示します。私が重要だと感じた関数のみを記載しほとんどのプライベート関数や型検査に直接関係なさそうな多くの関数を省いています。
dialyzer_worker モジュールの launch 関数は4つのモードごとに違った仕事を非同期的に行います。dialyzerはPLTを作成する plt_build とそれを使って型検査する succ_typing という2つの処理がありますが、前者では typesig モードの仕事を、後者では typesig, dataflow, warning の3つの仕事を行うようです。なお compile モードはソースから型検査する場合にbeamファイルを作成するということをやっているようですが今回の興味からは外れるため省略しています。
success typing
DialyzerはSuccess typing1と呼ばれるアルゴリズムを基礎にしています。そのアルゴリズム が実際に行われる部分は dialyzer_typesig:analyze_scc と思われます。型付け規則による型導出が traverse 関数、制約解消を行うのが solve 関数で、論文の内容とおおよそ合致します。
論文に記載されなかった詳細や論文との相違
型付け規則の[ABS]規則
論文では[ABS]規則において
\tau = ((\tau_1,...,\tau_n) \to \tau_e \texttt{ when } C)
のような制約をつけており、$$\tau \texttt{ when } C$$ のような制約をもった型が必要のように読めますが、実際には必要なく次のような規則で実装されています。
\frac
{A\cup \{x_1\mapsto \alpha_1,...,x_n\mapsto \alpha_n\} \vdash e : \tau_e, C}
{A\vdash \texttt{fun}(x_1,...,x_n) \to e : (\alpha_1,...,\alpha_n) \to \tau_e, C}
[\text{ABS}]
型付け規則の[CASE]規則
TODO
solveにおける型変数への型割り当ての初期値
solveでは型変数へ割当たる型を狭めていくという方針で制約解消を目指しているようです。初期値は any() 型とするようです。
よくある質問
TODO
宣伝
dialyzerより軽くて早いErlangの型検査ツールをOCamlで開発しています。