型推論
型を明示的に記述しなくても、言語処理系が文脈から主要型を推論する機構 推論に失敗するとその時点でエラーを報告できるので、誤った型を用いることに依るバグは回避できる
定式化
型環境$ \Gammaと、式$ eから、
$ S\Gamma\vdash e:\tauを満たすような型代入$ Sと型$ \tauを求める
のが、型推論
型推論器の持つべき性質
型推論できたプログラムは必ず型検査を通過する
型が推論できるなら、そのプログラムは正しい
比較的容易
型宣言をした場合に型検査に通過するようなプログラムは、すべての型宣言を省略した場合でも主要型の型推論に成功する MLの型推論機は健全かつ完全である
コード中の未知の型変数を文脈に追加
推論規則を用いて型の等値成約を生成
得られた成約列を単一化して、文脈に追加した型変数を消す
最も汎用的な型を求めて元々辞書に書いてあった型を更新するってこと？
ちがうか、型変数を消して型を特定するってことか
型の連立方程式を求める
文脈を更新して、次に進む
以下の記事を見たらだいたい分かる
用語
文脈
変数、関数名と、その型の辞書
推論規則
成約を生成するルール
型の等値成約
型変数同士の等式
一度は異なる型変数をおいたが、推論の過程で同じものだとわかったときに、一致させて片方の型変数を消す
Lispは動的型付きの言語だが、大きなプログラムを維持するとなると静的検査が必要になった
型を付与する上で問題になったのが以下の2つ
ポリモーフィズムをどう扱うか
特にLispはリストを扱うことがとても多いので。
型推論をどうするか
ポリモーフィズムありで型推論がないと、型を明示する際にめっちゃ煩雑になるので辛い
弱点
TypeScriptの型推論
参考
手続き的に型推論器を実装する