爲什麼在這種類型之前有一個加號？

Question

我正在瀏覽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 

由於

Answer 1

要在傑弗裏的答案建立，開發商在這裏做標記抽象類型作爲協工作的原因可能是不幫助您使用子類型（基本沒人用的子類型OCaml中，爲參數polymorphis一般是優選），但是要使用稱爲「寬鬆值限制」的類型系統中一個不那麼廣爲人知的方面，這要歸功於協變抽象類型允許更多的多態性。

您可能會安全地忽略這些細微之處，直到有一天您遇到了一個與您的抽象類型不一樣多態的問題，然後您應該記住，簽名中的協方差註釋可能會有所幫助。

我們在幾個月前討論過這個on reddit/ocaml：

考慮下面的代碼示例：代替'a C.collection，你會期望

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.empty()不是一個值，所以它的類型不是泛化的（〜made polymorphic）。從鬆弛值限制中獲益，你必須標記抽象'a collection類型協變：

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

當然是因爲該模塊C與簽名S密封這只是發生：module C : S = ...。如果模塊C沒有給出明確的簽名，那麼類型系統會推斷出最一般的方差（這裏是協方差），並且人們不會注意到這一點。對定義一個函子，或者強制執行一個虛幻類型的規則，或者編寫模塊化程序時，編程對一個抽象接口通常是有用的，所以這種情況肯定會發生，因此知道寬鬆的值限制是很有用的。

如果你想了解的理論，價值約束與放鬆從雅克常綠矮灌木叢，它的前幾頁都是一個相當有趣和方便的介紹主題和中心思想2004年的研究文章Relaxing the value restriction進行了討論。

Answer 2

這標誌着相對於所述模塊的類型的類型作爲協變。假設您有兩個鍵的鍵是相同類型的映射。這+說，如果一個地圖A的值是另一個地圖B的值的子類型，那麼地圖A的整體類型是地圖B的類型的子類型。我在Jane Street blog中發現了相當不錯的描述。