16

私は ocaml の標準ライブラリを閲覧していて、map.ml ファイルでこのコードを見つけました。

module type S =
  sig
    type key
    type +'a t
    val empty: 'a t'

type +'a tなぜ が存在するのか、なぜ作者が単に の代わりにそれを使用するのか疑問に思ってい'a tます。
その動作は奇妙で、その使用法を推測することはできません。

# type +'a t = 'a list;;
type 'a t = 'a list
# type +'a t = +'a list;;
Characters 13-14:
  type +'a t = +'a list;;
               ^
Error: Syntax error

ありがとう

4

2 に答える 2

16

Jeffrey の回答を基に、開発者がここで抽象型を共変としてマークする作業を行った理由は、サブタイピングの使用に役立たない可能性があります (パラメトリック ポリモーフィスが一般的に好まれるため、OCaml では基本的に誰もサブタイピングを使用しません)。 「緩和された値の制限」と呼ばれる型システムのあまり知られていない側面です。これにより、共変の抽象型がより多くのポリモーフィズムを可能にします。

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

これについては、数か月前に 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に明示的な署名が与えられていない場合、型システムは最も一般的な分散 (ここでは共分散) を推測し、それに気付かないでしょう。

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

理論を理解したい場合は、値の制限とその緩和について、Jacques Garrigue による 2004 年の研究記事「値の制限を緩和する」で説明しています。

于 2013-03-09T06:55:55.040 に答える
13

これは、型をモジュール型に関して共変としてマークします。キーが同じタイプの 2 つのマップがあるとします。これ+は、一方のマップ A の値が他方のマップ B の値のサブタイプである場合、マップ A の全体的なタイプはマップ B のタイプのサブタイプであるということです。これについては、 Jane Street のブログでかなり適切な説明を見つけました。

于 2013-03-09T00:30:17.983 に答える