Warum gibt es ein Pluszeichen vor diesem Typ?

Question

Ich habe die Standardbibliothek von ocaml durchsucht und bin in der map.ml-Datei auf diesen Code gestoßen.

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

Ich frage mich, warum gibt es type +'a t, und warum der Autor es einfach statt 'a t verwenden.
Sein Verhalten ist seltsam und ich kann die Verwendung davon nicht ableiten.

# 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 

Dank

Answer 1

Um oben auf Jeffrey Antwort zu bauen, der Grund, warum die Entwickler die Arbeit getan zu markieren hier den abstrakten Typen als covariant wahrscheinlich nicht ist Ihnen (im Wesentlichen verwenden Subtypisierung zu helfen, niemand nutzt Subtyping in OCaml, als parametrischen polymorphis ist im allgemeinen bevorzugt), sondern einen noch weniger bekannten Aspekt des Typsystems zu verwenden, der als "relaxed value restriction" bezeichnet wird, dank dessen kovariante abstrakte Typen mehr Polymorphismus erlauben. Sie können diese Feinheiten sicher ignorieren, bis Sie eines Tages ein Problem mit einem abstrakten Typ von Ihnen treffen, der nicht so polymorph ist, wie Sie möchten, und dann sollten Sie sich daran erinnern, dass eine Kovarianz-Annotation in der Signatur hilfreich sein kann.

Wir haben darüber on reddit/ocaml vor ein paar Monaten:

das folgende Codebeispiel vor:

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() 

Der Typ, den Sie für test bekommen ist '_a C.collection anstelle des 'a C.collection, die Sie erwarten. Es ist kein polymorpher Typ ('_a ist eine monomorphe Inferenzvariable, die noch nicht vollständig bestimmt ist), und Sie werden in den meisten Fällen nicht damit zufrieden sein.

Dies ist, weil C.empty() kein Wert ist, so ist sein Typ nicht verallgemeinert (~ gemacht polymorph). Um von der entspannten Wert Einschränkung profitieren, müssen Sie die abstrakten Typ 'a collection covariant markieren:

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

Natürlich geschieht dies nur, weil das Modul C mit der Signatur versiegelt ist S: module C : S = .... Wenn das Modul C keine explizite Signatur erhalten hat, würde das Typsystem auf die allgemeinste Varianz (hier Kovarianz) schließen, und das würde man nicht bemerken. Die Programmierung gegen eine abstrakte Schnittstelle ist oft nützlich (wenn man einen Funktor definiert oder eine Disziplin vom Phantomtyp durchsetzt oder modulare Programme schreibt), so dass diese Art von Situation definitiv passiert und es dann nützlich ist, über die Lockerung der Werte zu wissen.

Wenn Sie die Theorie verstehen wollen, ist die Wert Einschränkung und seine Entspannung in dem 2004 Forschungsartikel Relaxing the value restriction von Jacques Garrigue, deren ersten Seite ist eine recht interessante und zugängliche Einführung in das Thema und Hauptidee diskutiert.

Answer 2

Dies markiert den Typ als covariant in Bezug auf den Modultyp. Angenommen, Sie haben zwei Maps, deren Schlüssel vom selben Typ sind. Diese + sagt, wenn die Werte einer Karte A von einem Subtyp der Werte der anderen Karte B sind, dann ist der Gesamttyp der Karte A ein Subtyp des Typs der Karte B. Ich fand eine ziemlich gute Beschreibung davon in der Jane Street blog.