9

緩和された値の制限がいつ開始されるかについて、誰かが簡潔に説明できますか? ルールの簡潔で明確な説明を見つけるのに苦労しました。ガリーグの論文があります：

http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

しかし、それは少し濃いです。だれかもっと詳しい情報源を知っていますか?

補遺

以下にいくつかの適切な説明が追加されましたが、次の動作の説明を見つけることができませんでした。

# let _x = 3 in (fun () -> ref None);;
- : unit -> 'a option ref = <fun>
# let _x = ref 3 in (fun () -> ref None);;
- : unit -> '_a option ref = <fun>

誰もが上記を明確にすることができますか? 囲んでいる let の RHS 内の ref の浮遊定義がヒューリスティックに影響するのはなぜですか。

4

4 に答える 4

9

私は型理論家ではありませんが、Garrigue の説明に対する私の解釈は次のとおりです。値 V があります。通常の値制限の下で (OCaml で) V に割り当てられる型から始めます。型にはいくつかの数 (おそらく 0) の単相型変数があります。型の共変位置 (関数矢印の右側) にのみ現れるそのような変数ごとに、完全にポリモーフィックな型変数に置き換えることができます。

議論は次のようになります。単相変数は変数であるため、任意の単一の型に置き換えることを想像できます。したがって、無人型 U を選択します。これは共変の位置にのみあるため、U は任意のスーパータイプに置き換えることができます。ただし、すべての型は非居住型のスーパータイプであるため、完全にポリモーフィックな変数に置き換えても安全です。

そのため、共変の位置にのみ現れる単相変数 (となるもの) がある場合は、緩和された値の制限が適用されます。

（私はこれが正しいことを願っています.octrefが示唆するように、@gascheは確かにうまくいくでしょう。）

于 2013-03-22T03:17:27.403 に答える
5

Jeffrey は、緩和が正しい理由について直感的な説明を提供しました。それがいつ役立つかについては、最初に回答octrefを再現できると思います。

いつか、自分の抽象型が思ったほどポリモーフィックではないという問題に遭遇するまでは、これらの微妙な点を安全に無視してもかまいません。その場合は、署名の共分散注釈が役立つ可能性があることを覚えておく必要があります。

これについては、数か月前に reddit/ocaml で議論しました。

次のコード例を検討してください。

module type S = sig
  type 'a collection
  val empty : unit -> 'a collection
end

module C : S = struct
  type 'a collection =
    | Nil
    | Cons of 'a * 'a collection
  let empty () = Nil
end

let test = C.empty ()

取得する型testは、期待する'_a C.collectionではなく です。'a C.collectionこれは多相型 ('_aまだ完全には決定されていない単相推論変数) ではなく、ほとんどの場合、これに満足することはありません。

これは、C.empty ()が値ではないため、その型が一般化されていない (~ ポリモーフィックにされている) ためです。緩和された値の制限の恩恵を受けるには、抽象型'a collection共変をマークする必要があります。

module type S = sig
  type +'a collection
  val empty : unit -> 'a collection
end

もちろん、これはモジュールCが署名で封印されているためにのみ発生しますS: module C : S = .... モジュールCに明示的な署名が与えられていない場合、型システムは最も一般的な分散 (ここでは共分散) を推測し、それに気付かないでしょう。

抽象インターフェースに対するプログラミングは、(ファンクターを定義するとき、またはファントム型規則を強制するとき、またはモジュラー プログラムを作成するとき) に役立つことが多いため、この種の状況は確実に発生し、緩和された値の制限について知っておくと役立ちます。

これは、より多くのポリモーフィズムを取得するためにそれを認識する必要がある場合の例です。抽象境界 (抽象型のモジュール シグネチャ) を設定し、それが自動的に機能しないため、抽象型を明示的に指定する必要があるためです。は共変です。

ほとんどの場合、ポリモーフィックなデータ構造を操作するときに、気付かないうちに発生します。緩和のおかげで[] @ []多形型しかありません。'a list

具体的だがより高度な例は、Oleg の Ber-MetaOCaml です。これは、型を使用して、('cl, 'ty) code区分的に構築された引用符で囲まれた式を表します。'tyは、引用されたコードの結果の型を表し、'cl多態性のままである場合、引用されたコード内の変数のスコープが正しいことを保証する一種のファントム領域変数です。これは、引用された式が他の引用された式を構成することによって構築される状況でのポリモーフィズムに依存するため (したがって、一般的には値ではありません)、基本的には、値の制限を緩和しないとまったく機能しません (これは、型に関する彼の優れたまだ技術的なドキュメントの補足的な発言です)。推論）。

于 2013-03-22T07:32:10.667 に答える
1

私はこの理論にあまり詳しくありませんが、それについて質問しました。
ガッシェは私に簡潔な説明を提供してくれました。この例は、OCaml の map モジュールのほんの一部です。見てみな！
たぶん、彼はあなたにより良い答えを提供できるでしょう。@ガッシェ

于 2013-03-22T03:17:20.557 に答える