型を明示的に記述しなくても、言語処理系が文脈から主要型を推論する機構

推論に失敗するとその時点でエラーを報告できるので、誤った型を用いることに依るバグは回避できる

定式化

型環境\Gammaと、式eから、

S\Gamma\vdash e:\tauを満たすような型代入Sと型\tauを求める

のが、型推論

型推論器の持つべき性質

型推論できたプログラムは必ず型検査を通過する

型が推論できるなら、そのプログラムは正しい

比較的容易

型宣言をした場合に型検査に通過するようなプログラムは、すべての型宣言を省略した場合でも主要型の型推論に成功する

MLの型推論機は健全かつ完全である

型推論の手順 ref

コード中の未知の型変数を文脈に追加

推論規則を用いて型の等値成約を生成

得られた成約列を単一化して、文脈に追加した型変数を消す

最も汎用的な型を求めて元々辞書に書いてあった型を更新するってこと？

ちがうか、型変数を消して型を特定するってことか

型の連立方程式を求める

文脈を更新して、次に進む

以下の記事を見たらだいたい分かる

用語

文脈

変数、関数名と、その型の辞書

推論規則

成約を生成するルール

型の等値成約

型変数同士の等式

一度は異なる型変数をおいたが、推論の過程で同じものだとわかったときに、一致させて片方の型変数を消す

型推論の歴史 ref

Lispは動的型付きの言語だが、大きなプログラムを維持するとなると静的検査が必要になった

型を付与する上で問題になったのが以下の2つ

ポリモーフィズムをどう扱うか

特にLispはリストを扱うことがとても多いので。

型推論をどうするか

ポリモーフィズムありで型推論がないと、型を明示する際にめっちゃ煩雑になるので辛い

1970年前後にHindley-Milner 型システムが登場

弱点

TypeScriptの型推論

参考

CoPL 10章

手続き的に型推論器を実装する

Neural Networkを使った漸進的型付けに対する型推論