型推論の限界は何ですか？

タイプ推論の限界は何ですか？どのタイプのシステムには一般推論アルゴリズムがありませんか？型推論の限界は何ですか？

2009-08-09 Anonymous

Joe Wellsは、型推論は独立ジラールとレイノルズによって発見され、最も基本的な多型ラムダ計算されているシステム F、のために決定不能であることを示しました。これは、型推論の限界を示す最も重要な結果です。

ここではまだ開いている重要な問題です：ヒンドリー - ミルナーの型推論に一般化代数データ型を統合するための最良の方法は何ですか？毎年Simon Peyton Jonesは新しい答えを思いつきました。これはおそらく前年の答えよりも優れています。私は2009年3月版を読んでいないので、確定していると思うかどうかは言えません。

出典

2009-08-09 16:01:46

アルゴリズムWは、決定可能なシステムFの可能な部分集合をカバーしていますか？ –

@ott：私は尖頭型の理論家ではありませんが、System Fには複数の比較可能な決定可能な部分集合があります。拡張の可能性は言うまでもない（GADT、等価制約、修飾型）。それは尖った群衆のための完全な雇用です:-) –

@Norman Ramsey：面白い。タイプ理論家が尖っているかどうかはわかりませんが、私が見た論文は現実とはかなり離れているようですが、タイプ理論が主流になり広く受け入れられるかどうかはわかりません。あなたはまだ基礎を理解するためにMLを学ばなければなりません。 –

値依存型システム（またはショート、依存型システム内）のようなものを言うタイプ記述することができます：「評価時（ランタイム）、この変数の値は、常にその値に等しくなります変数は、異なる評価プロセスで計算されます。コードからこのタイプを自動的に推論するには、定理の自動証明が必要です。あなたが表現できる定理の集合が自動的に証明可能な定理に限定されていれば、それは問題ではないでしょうが、依存型言語の場合、これは一般的ではありません。

だから、依存型指定されたシステムは、一般的に持っている（完全な）推論を入力することはできません。

私は誰かが道徳的正式かつ完全な答えを提供することができます確信している...

出典

2009-08-09 13:01:34 Peaker

型推論の限界は何ですか？

答えて

関連する問題