[解決済み] ヒンドレーミルナーとは？

質問

この用語に出会ったのは Hindley-Milner という言葉に出会いましたが、どういう意味なのかよくわかりません。

以下の投稿を読ませていただきました。

• Steve Yegge - 動的言語の逆襲
• スティーブ・イェーゲ ピノキオの問題
• ダニエル・スピワック Hindley-Milnerとは何なのか？(そしてなぜそれがクールなのか?)

しかし、通常、私に簡潔な説明を提供してくれるwikipediaには、この用語の単一の項目はありません。


ノート - があります。 が追加されました。

何ですか？

どのような言語やツールが実装・使用しているのですか？

簡潔な回答をお願いします。

どのように解決するのですか？

ヒンドレーミルナーは 型システム であり、ロジャー・ハインドリー（論理学の研究者）とロビン・ミルナー（プログラミング言語の研究者）によって独自に発見された。 Hindley-Milnerの利点は以下の通りです。

• それは ポリモーフィック 例えば、要素の型に依存せずにリストの長さを与えることができる関数や、木に格納されたキーの型に依存せずに二分木のルックアップを行う関数などです。

• 時には関数や値が 複数の型 それは "整数のリストから整数へ", "文字列のリストから整数へ", "ペアのリストから整数へ" というようになります。 この場合、Hindley-Milner方式の信号の利点は、以下の通りです。 それぞれのよく型付けされた用語が一意の"best"型を持っていることです。 と呼ばれるものである。 主な型 . リストレングス関数の主型は "任意の a のリストから、関数 a を整数に変換する関数です。 ここでは a はいわゆる "型パラメータで、これは ラムダ計算では明示的に ですが ほとんどのプログラミング言語では暗黙的 . 型パラメタの使用は、Hindley-Milnerがなぜ パラメトリック ポリモーフィズム . (MLでlength関数の定義を書くと，このように型パラメータを見ることができます．

   fun 'a length []      = 0
     | 'a length (x::xs) = 1 + length xs
  
  

• もし がHindley-Milner型であれば 型宣言をしなくても主な型を推測することができます。 またはプログラマによる他の注釈を必要とせずに、主要な型を推測することができます。 (これは、注釈のないMLコードの大きな塊を扱ったことのある人なら誰でも証明できるように、複雑な祝福です)。

Hindley-Milnerはほとんど全ての静的型付けされた関数型言語の型システムの基礎となっています。 一般的に使用されているそのような言語には

• MLファミリー ( 標準的なML と オブジェクティブカムル )
• ハスケル
• クリーン

これらの言語はすべてHindley-Milnerを拡張しています。Haskell、Clean、Objective Camlは野心的で珍しい方法でそうしています。 (基本的なHindley-Milnerは、例えば、不特定多数の型の値のリストを保持するmutable cellを使用して覆すことができるので、拡張はmutable変数を扱うために必要である。 このような問題には 値の制限 .)

その他、型付き関数型言語をベースにしたマイナーな言語やツールの多くがHindley-Milnerを使用しています。

Hindley-Milnerは、以下のような制約があります。 システムF の制限であり、より多くの型を許容するが はプログラマによるアノテーションを必要とします。 .