問題タブ [hindley-milner]

Hindley-Milnerという用語に出会いましたが、その意味を理解しているかどうかはわかりません。

次の投稿を読みました。

• Steve Yegge -動的言語の逆襲
• Steve Yegge -ピノキオ問題
• Daniel Spiewak - Hindley-Milner とは? （そして、なぜそれはクールなのですか？）

しかし、通常、簡潔な説明を提供してくれるウィキペディアには、この用語の単一のエントリはありません。
^{注- 1 つ追加されました}

それは何ですか？
それを実装または使用する言語とツールは何ですか?
簡潔な答えを教えてください。

Hindley-Milnerは、多くのよく知られている関数型プログラミング言語の型システムの基礎となる型システムです。Damas-Milnerは、Hindley-Milner型システムの型を推測（推測？）するアルゴリズムです。

ウィキペディアは、私が知る限り、「統一」という一言に相当するアルゴリズムの説明を提供しています。それだけですか？もしそうなら、それは興味深い部分が型推論システムではなく型システム自体であることを意味します。

Damas-Milnerが統一以上のものである場合は、簡単な例と、理想的にはいくつかのコードを含むDamas-Milnerの説明が必要です。

また、このアルゴリズムは型推論を行うとよく言われます。それは本当に推論システムですか？タイプを推測するだけだと思いました。

関連する質問：

• Hindley Millerとは何ですか？
• 統一問題への型推論

型推論の制限は何ですか? 一般的な推論アルゴリズムを持たない型システムは?

Andrew Koenig のAn anecdote about ML type inferenceで、著者はマージ ソートの実装を ML の学習演習として使用し、「正しくない」型推論を発見して喜んでいます。

驚いたことに、コンパイラは次のタイプを報告しました。

つまり、このソート関数は、あらゆるタイプのリストを受け入れ、整数のリストを返します。

それは不可能です。出力は入力の順列でなければなりません。どのように異なるタイプを持つことができますか? 読者はきっと、私の最初の衝動に親しみを覚えるでしょう。コンパイラのバグを発見したのではないかと思ったのです!

もう少し考えてみたところ、関数が引数を無視する別の方法があることに気付きました。確かに、私が試してみたところ、まさにそれが起こったのです: sort(nil)return でしたnilが、空でないリストを並べ替えると、無限再帰ループに入ります。

Haskellに翻訳すると

GHC は同様の型を推論します:

Damas-Hindley-Milner アルゴリズムはどのようにこの型を推測しますか?

この非常に単純なSML関数の末尾再帰バージョンを作成しようとしていました。

この過程で、私はパラメータに型注釈を使用していました。次のコードはこれを示しており、タイプエラーが発生します（以下を参照）が、タイプアノテーションを削除するだけで、SMLは問題なくそれを受け入れ、関数全体に上記のより単純な関数と同じシグネチャを与えます。

エラー：

与えられた2つのエラーがあります。後者はここではそれほど重要ではないようです。suffixes_helperの2つの句の不一致です。最初は私が理解していないものです。'a:list最初のパラメータがタイプであり、2番目のパラメータがタイプであることを示すために注釈を付け'b:listます。私が理解しているように、一般的な統一の最上位に構築されているHindley-Milner型推論アルゴリズムは、？の置換を使用して、で'b:list統一できるべきではありません。'a:list list'b ---> 'a list

編集：答えは、ある意味で型注釈によって与えられたものよりも厳密な推論された型を許可しない型推論アルゴリズムと関係があるかもしれないことを示唆しています。このようなルールは、パラメーターと関数全体の注釈にのみ適用されると思います。これが正しいかどうかはわかりません。いずれにせよ、型アノテーションを関数本体に移動しようとすると、同じ種類のエラーが発生します。

エラーは次のとおりです。

関数型言語の型推論を行うためのよく知られたDamas-Hindley-Milner アルゴリズムに関する情報、特に実装に関する情報を探しています。

アルゴリズム Wの実行方法は既に知っていますが、通常の統合ではなく、制約ジェネレーター/ソルバーに基づく最近の新しいアルゴリズムについて聞いたことがあります。ただし、これらの新しいアルゴリズムの実装に関する議論を見つけることができません。

ML 推論に関する部分的な情報を見つけることができるアイデアはありますか?

Scala 型システムと Haskell の欠点を読んでいますか? 、私は尋ねなければなりません: 具体的には、Haskell の型システムが他の言語 (C、C++、Java) の型システムよりも強力な理由は何ですか。どうやら、Scala でさえ、Haskell の型システムと同じ機能のいくつかを実行することはできません。具体的には、Haskell の型システム (Hindley–Milner 型推論) がこれほど強力な理由は何ですか? 例を挙げていただけますか？

私がやっていること:ファイルを解析し、それを一連の操作に変換し、数千のデータセットをそのシーケンスにフィードして、それぞれから最終的な値を抽出できる小さなインタープリターシステムを作成しています。コンパイル済みインタープリターは、データセットと実行コンテキストの 2 つの引数を取る純粋な関数のリストで構成されます。各関数は、変更された実行コンテキストを返します。

type ('data, 'context) interpreter = ('data -> 'context -> 'context) list

コンパイラは基本的に、次のように定義されたマップ記述を使用する最終的なトークンから命令へのマッピング ステップを備えたトークナイザーです。

type ('data, 'context) map = (string * ('data -> 'context -> 'context)) list

一般的なインタープリターの使用法は次のようになります。

問題:、、メソッド、および対応する型 (あるコンテキスト クラスでは整数、別のコンテキスト クラスでは浮動小数点数など)pocket_calcをサポートする任意のクラスでインタープリターを動作させたいと考えています。addsubmuldata

ただし、pocket_calcは関数ではなく値として定義されているため、型システムはその型をジェネリックにしません。最初に使用すると、'dataと'context型は最初に提供したデータとコンテキストの型にバインドされ、インタープリターは次のようになります。他のデータおよびコンテキスト タイプとは永遠に互換性がありません。

実行可能な解決策は、インタープリターの定義を eta-expand して、その型パラメーターをジェネリックにできるようにすることです。

ただし、この解決策はいくつかの理由で受け入れられません。

• 呼び出されるたびにインタープリターを再コンパイルするため、パフォーマンスが大幅に低下します。マッピング ステップ (マップ リストを使用してトークン リストをインタープリターに変換する) でさえ、顕著な速度低下を引き起こします。

• 私の設計は、初期化時に読み込まれるすべてのインタープリターに依存しています。これは、読み込まれたファイルのトークンがマップ リストの行と一致しない場合にコンパイラが警告を発行するためです。インタプリタは最終的に実行されます)。

• 特定のマップ リストを複数のインタープリターで再利用したい場合があります。単独で使用する場合もあれば、追加の命令 (たとえば"div") を先頭に追加する場合もあります。

質問: eta-expansion 以外に型をパラメトリックにする方法はありますか? モジュールの署名や継承に関係する巧妙なトリックでしょうか? それが不可能な場合、eta-expansion を受け入れられる解決策にするために、上記の 3 つの問題を軽減する方法はありますか? ありがとうございました！

私はJavaで書かれた単純なデータフローベースのシステム（LabViewエディタ/ランタイムのように想像してください）に取り組んでいます。ユーザーはエディターでブロックを相互に接続でき、データフローグラフが正しいことを確認するために型推論が必要ですが、ほとんどの型推論の例は数学表記、ML、Scala、Perlなどで書かれています。 "。

Hindley-Milnerアルゴリズムについて読んだところ、実装できる良い例が記載されたこのドキュメントが見つかりました。これは、制約のようにT1=T2のセットで機能します。ただし、私のデータフローグラフは、制約のようにT1> = T2に変換されます（または、T2はT1、共分散、またはT1 <：T2を拡張します（さまざまな記事で見たように））。型変数（のようなジェネリック関数で使用されるT merge(T in1, T in2)）と具象型だけのラムダはありません。

HMアルゴリズムを要約するには：

単純な等式関係ではなく、これらの種類の関係で機能するように元のHMアルゴリズムを変更するにはどうすればよいですか？Java風の例や説明をいただければ幸いです。

誰かが次の F# プログラムで段階的な型推論を説明できますか?

Hindley Milner の統一プロセスがどのように機能するかを段階的に見たいと思っています。