問題タブ [value-restriction]

リストに非常に単純なMergeSort実装があります。

しかし、F# Interactive で任意の入力をテストしようとすると、次のようになります。

値制限エラーが発生しました:

エラー FS0030: 値の制限。値 'xs' はジェネリック型 val を持つと推測されています xs : '_a list when '_a : comparison 'xs' を単純なデータ項として定義するか、明示的な引数を持つ関数にするか、意図しない場合はジェネリックにするには、型注釈を追加します。

なぜそれが起こるのですか？それを修正する簡単な方法は何ですか？

整数とトリプレットを取り、指定された位置でトリプレットの要素を返す関数を作成しようとしています (ヒッキーの本の演習 5.3)。トリプレットには、さまざまなタイプの要素を含めることができる必要があります。

それぞれがトリプルの特定の要素を返す 3 つの小さな関数を記述し、それに応じて大きな関数がそれらの 1 つを返すようにすると、うまくいくと思いましたが、うまくいきません。

この「イータ拡張」の概念をいじってみましたが、わかりませんでした。

ここでは「2」と書くだけです。何かアドバイス？

行列の転置を計算しようとしている F# の割り当てがあります。簡単ですが、値制限エラーが発生し続け、その理由がわかりません。そこにあるVRエラーの質問の多くを調べましたが、私はまだ暗闇の中にいます. これが私のコードです：

エラーの一部は空のリストが原因であると思いますが、何も役に立たないようです。任意のポインタをいただければ幸いです。

編集:このコードの次のバージョンは機能します。誰でも理由を説明できますか?

ただし、let を使用してバインドしない限り、上記の転置呼び出しにはユニット型が必要であると、コンパイラはまだ不平を言っています。誰かがここで何が起こっているのかを明確にしてもらえますか?

OCamlの弱いポリモーフィズムについて少し混乱しています。

関数を定義する次のスニペットを参照してくださいremember。

コンパイラは多相型を推論でき、'a -> 'aローカルcacheで使用されます。

しかし、上記のコードを次のように変更すると

コンパイラは弱ポリモーフィック型'_a -> '_aを推論します。また、それはcacheの呼び出し間で共有されているようですremember。

なぜコンパイラはここで弱いポリモーフィック型を推論し、なぜcache共有されているのですか?

さらに、コードを再度変更すると

コンパイラはポリモーフィック型'a -> 'a -> 'aを推測し、cacheローカルで使用されるようになります。これはなぜですか？

MLton のドキュメントによると:

標準 ML では、使用する前に型を定義する必要があります。【リンク】

すべての実装がこの要件を強制するわけではありません (たとえば、SML/NJ は強制しません) が、上記のリンクのページは、健全性のために必要になる理由 (実装が値の制限をどのように処理するかによって異なります) の良い例です。定義のコメントの一部と一致します。

私たちの定義では想定されていませんが、すべてのコンテキストC = T、U、EがE ⊆ Tという名前のプロパティを持つことが意図されています。したがって、 Tは大まかに、「生成された」すべての型名を含むと考えることができます。[…] もちろん、「生成された」ものについての発言は、意味規則に関して正確ではありません。しかし、次の正確な結果は簡単に実証できます。

S を文T , U , E ⊢句⇒ Aとし、 E ⊆ Tを tynamesとし、S' を S の証明に現れる文T ', U ', E ' ⊢句⇒ A ' とする。次に、 E ' ⊆ T 'も tynames します。

[21ページ]

しかし、私はこれに二重に混乱しています。

まず、上記の定理は後ろ向きに見えます。「Sの証明で発生する」というフレーズを正しく理解すると、これは（対比によって）「E ⊆ Tという名前の意図に違反するコンテキストがあると、後続のすべてのコンテキストもその意図に違反する」ことを意味するようです。それが本当だとしても、逆を主張する方がはるかに有用で意味があるように思われます。 "。いいえ？

第二に、MLton のステートメントもDefinitionのステートメントも、実際には推論規則 (またはそれに続く「さらなる制限」) によってサポートされているようには見えません。いくつかの推論規則には、副条件として「tynames τ ⊆ T of C」または「tynames VE ⊆ T of C」がありますが、このプログラムにはこれらの規則は必要ありません (上記のリンクのドキュメントに記載されています)。

(具体的には、規則 (4) はlet、規則 (14) は=>、規則 (26) は と関係recがあります。このプログラムでは、これらのいずれも使用されていません。)

そして、別の方向から来ると、宣言をカバーするルール (17) は、生成された型名がCのTにdatatypeないことだけを要求します。したがって、既存の値環境で使用される型名の生成を妨げません (ただし、VE ⊆ TのCという名前が既に真である場合を除きます)。

ここにはかなり基本的なものが欠けているように感じますが、それが何であるかはわかりません!

は弱いポリモーフィズムですが、ref.

orを使わずに弱いポリモーフィズム関数を書く方法はありますrefかpartial application?

このコードはコンパイルされません:

• http://ideone.com/qktsOb

ユニファイヤは、関連付けられている型パラメータを修正し、最初の出現を確認したfと思います。gこのプロセスを支配するものは何ですか? これは「値の制限」に非常に似ていると思いますがf、gすでに eta 拡張されています! これは難しい問題です。

• http://en.wikipedia.org/wiki/Value_restriction

事前定義された演算子を整数型に対してアドホックなポリモーフィズムで入力することの背後には、何らかの黒魔術があることは確かに想像できますが、それは単なる私の推測です。任意の情報をいただければ幸いです。