Hindley-Milnerは、よく知られている多くの関数型プログラミング言語の型システムの基礎となる型システムです。 Damas-Milnerは、Hindley-Milner型のシステムで型を推定（推論する）アルゴリズムです。CS101学生が理解できるようにDamas-Milner型推論を記述する
Wikipediaは、私が知る限り、「統一」という単一の単語に相当するアルゴリズムの説明を提供します。それはすべてそれにあるのですか？もしそうなら、それは興味深い部分が型推論システムではなく型システムそのものであることを意味します。
Damas-Milnerが統一以上のものであれば、私は簡単な例と、理想的にはいくつかのコードを含むDamas-Milnerについて説明したいと思います。
また、このアルゴリズムはしばしば型推論を行うと言われています。それは本当に推論システムですか？私はタイプを推論することしか考えていなかった。
関連した質問：
ダマスミルナーは、統一の単なる構造化された使用です。
ラムダ式に再帰すると、新しい変数名が作成されます。サブクラスで、指定された型を必要とするような方法でその変数が使用されると、その変数とその型の統一を記録します。個々の変数がintとa - > bの両方の関数であると言うように、理にかなっていない2つの型を統一しようとすると、何か悪いことをしたときに怒鳴ります。
また、このアルゴリズムはしばしば型推論を行うと言われています。それは本当に推論システムですか？私はタイプを推論することしか考えていなかった。
タイプを推論するのは型推論です。タイプ注釈が特定の用語に対して有効であることを確認することは、タイプチェックです。彼らは別の問題です。
もしそうなら、それは興味のある部分がタイプ推論システムではなくタイプそのものであることを意味します。
ヒンドレーミルナースタイルタイプシステムは、カスプ上でバランスがとれていると一般的に言われています。さらに多くの機能を追加すると、そのタイプを推論することが不可能になります。したがって、推論プロパティを破壊することなくHindley-Milnerスタイルの型システムの上にレイヤリングできるタイプのシステム拡張は、現代の関数型言語の面白い部分です。場合によっては、型推論と型チェックを混在させることもあります。たとえば、Haskellでは、最近の拡張機能の多くは推論できませんが、チェックすることができるため、多態的な再帰のような高度な機能のための型アノテーションが必要です。
ウィキペディアは、私が知る限り、「統一」という単一の単語に相当するアルゴリズムについて説明します。それはすべてそれにあるのですか？もしそうなら、それは興味深い部分が型推論システムではなく型システムそのものであることを意味します。
IIRC、Damas-Milner型推論アルゴリズムWの興味深い部分は、可能な最も一般的な型を推測することです。