型推論の制限は何ですか? 一般的な推論アルゴリズムを持たない型システムは?
1469 次
2 に答える
12
Joe Wellsは、Girard と Reynolds によって独立して発見された、最も基本的な多形ラムダ計算である System F の型推論が決定不能であることを示しました。これは、型推論の限界を示す最も重要な結果です。
まだ未解決の重要な問題があります: 一般化された代数データ型を Hindley-Milner 型推論に統合する最良の方法は何ですか? サイモン・ペイトン・ジョーンズは毎年新しい答えを出していますが、これはおそらく前年の答えよりも優れています. 私は 2009 年 3 月版を読んでいないので、それが決定的なものになるかどうかはわかりません。
于 2009-08-09T16:01:46.963 に答える
6
値依存型システム (つまり、依存型システム) は、「評価時 (実行時) に、この変数の値は常にその変数の値と等しくなります。つまり、別の評価プロセスで計算されます。」コードからこの型を自動的に推定すると、定理の自動証明が必要になります。表現できる定理が自動的に証明できるものに限られていれば問題ありませんが、依存型言語の場合は一般的にそうではありません。
したがって、依存型付けシステムは、一般的な (そして完全な) 型推論を行うことができません。
誰かが道徳的で正式で完全な答えを提供できると確信しています...
于 2009-08-09T13:01:34.683 に答える