Dialyzer の型推論アルゴリズムについて - Qiitaこの記事は 第2のドワンゴ Advent Calendar 22日目の記事として書かれました。 ドワンゴ新卒の @amutake です。仕事では Erlang を書いています。 今回は Erlang の静的型検査ツールである Dialyzer が採用している 成功型付け (success typings) という型付けの手法について調べたので簡単に紹介します。 (本当は Coq で回転寿司屋の店内を形式化して設計した回転寿司システムがお客さんを満足させることを証明した話が書きたかったのですが、証明が終わりませんでした) Dialyzer の不満点 Erlang を書いている人はほぼ全員使っているであろう静的型検査ツールの Dialyzer ですが、いくつか不満点があります。 メモリを食いまくる 時間がかかる ときどきよくわからない推論をする メモリを食いまくることと時間がかかることについて
