ここでは、静的型付けと動的型付けについて興味深い議論が見られます。私は通常、コンパイル型チェック、より適切に文書化されたコードなどの理由から、静的型付けを好みます。ただし、たとえば Java のように行うと、静的型付けがコードを乱雑にすることに同意します。
それで、私は自分自身の関数型スタイル言語の構築を開始しようとしています。型推論は、私が実装したいものの 1 つです。私はそれが大きな主題であることを理解しています。私はこれまでに行われたことのないものを作成しようとしているのではなく、基本的な推論にすぎません...
これに役立つ何を読むべきかについての指針はありますか？より理論的な圏論/型理論のテキストとは対照的に、より実用的/実用的なものが望ましいです。データ構造/アルゴリズムを使用した実装に関する議論のテキストがあれば、それは素晴らしいことです。
次のリソースは、難易度の高い順に型推論を理解するのに役立ちます。
ただし、学習するのに最適な方法は実行することなので、プログラミング言語コースの宿題を使って、おもちゃの関数型言語の型推論を実装することを強くお勧めします。
MLでこれら2つのアクセス可能な宿題をお勧めします。どちらも、1日以内に完了することができます。
これらの課題は、より高度なコースからのものです。
残念なことに、このテーマに関する文献の多くは非常に密集しています。私もあなたの立場でした。プログラミング言語: アプリケーションと解釈からこのテーマを初めて紹介しました。
抽象的なアイデアを要約してから、すぐにはわからなかった詳細を説明します。まず、型推論は、制約を生成して解決することと考えることができます。制約を生成するには、構文ツリーを再帰的に実行し、各ノードで 1 つ以上の制約を生成します。たとえば、ノードが+演算子の場合、オペランドと結果はすべて数値でなければなりません。関数を適用するノードは、関数の結果と同じ型を持ちます。
のない言語letの場合、代入によって上記の制約をやみくもに解決できます。例えば：
(if (= 1 2)
1
2)
ここで、if ステートメントの条件はブール値でなければならず、if ステートメントの型はthenandelse句の型と同じであると言えます。私たちは数であることを知っ1ており2、代入によって、ifステートメントが数であることを知っています。
厄介なところ、そしてしばらく理解できなかったのは、let の処理です。
(let ((id (lambda (x) x)))
(id id))
ここでは、id渡されたものは何でも返す関数 (ID 関数とも呼ばれます) にバインドしています。問題は、関数のパラメータの型が のx使用ごとに異なることですid。2 番目idは type の関数でa -> a、どこaでもかまいません。1 つ目はタイプ(a -> a) -> (a -> a)です。これは let ポリモーフィズムとして知られています。重要なのは、特定の順序で制約を解決することです。最初に の定義の制約を解決しますid。これは になりますa -> a。次に、 のタイプの新しい個別のコピーを、id各場所の制約に代入できます。idたとえばa2 -> a2、 とが使用されa3 -> a3ます。
これは、オンライン リソースでは容易に説明されませんでした。アルゴリズム W または M については言及しますが、制約の解決に関してそれらがどのように機能するか、または let ポリモーフィズムを妨げない理由については言及しません。これらのアルゴリズムはそれぞれ、制約の解決に順序付けを強制します。
このリソースは、アルゴリズム W、M、および制約の生成と解決の一般的な概念をすべて結び付けるのに非常に役立つことがわかりました。少し密度が高いですが、多くのものよりも優れています。
http://www.cs.uu.nl/research/techreps/repo/CS-2002/2002-031.pdf
そこにある他の論文の多くも素晴らしいです：
http://people.cs.uu.nl/bastiaan/papers.html
やや暗い世界を明確にするのに役立つことを願っています。
型とプログラミング言語 Benjamin C. Pierce 著
アルティメットのラムダ、ここから。