Perché c'è un segno più prima di questo tipo?

Question

Stavo navigando nella libreria standard di ocaml e ho trovato questo codice nel file map.ml.

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

mi chiedo perché c'è type +'a t, e perché l'autore usarlo invece di 'a t.
Il suo comportamento è strano e non posso dedurne l'utilizzo.

# 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 

Grazie

Answer 1

Per costruire sulla risposta di Jeffrey, il motivo gli sviluppatori hanno fatto il lavoro di marcatura tipo astratto come covariante qui è probabile che non che facilitano l'utilizzo sottotipizzazione (essenzialmente nessuno usa subtyping in OCaml, come polymorphis parametrici è generalmente preferito), ma per utilizzare un aspetto ancora meno noto del sistema di tipi chiamato "restrizione del valore rilassato", grazie al quale i tipi astratti covarianti consentono più polimorfismo.

Si può tranquillamente ignorare tali sottigliezze fino a quando, un giorno, si verifica un problema con un tipo astratto che non è così polimorfico come si vorrebbe, e quindi si dovrebbe ricordare che un'annotazione di covarianza nella firma può aiutare.

Ne abbiamo discusso on reddit/ocaml a pochi mesi fa:

Si consideri il seguente esempio di codice:

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

Il tipo che si ottiene per test è '_a C.collection, al posto del 'a C.collection che ci si aspetterebbe. Non è un tipo polimorfico ('_a è una variabile di inferenza monomorfica che non è stata ancora completamente determinata) e nella maggior parte dei casi non ne sarete soddisfatti.

Questo perché C.empty() non è un valore, quindi il suo tipo non è generalizzato (~ fatto polimorfico). Per beneficiare del valore di restrizione rilassato, è necessario evidenziare l'abstract tipo 'a collection covariante:

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

Naturalmente questo accade solo perché il modulo C è sigillata con la firma S: module C : S = .... Se al modulo C non è stata assegnata una firma esplicita, il sistema tipo avrebbe dedotto la varianza più generale (qui covarianza) e uno non lo noterebbe.

La programmazione con un'interfaccia astratta è spesso utile (quando si definisce un funtore, o si applica una disciplina del tipo fantasma o si scrivono programmi modulari), quindi questo tipo di situazione si verifica sicuramente ed è quindi utile conoscere la restrizione del valore rilassato.

Se si vuole capire la teoria, la restrizione valore e la sua relax sono discussi nel articolo del 2004 di ricerca Relaxing the value restriction da Jacques Garrigue, la cui prima pagina pochi sono un'introduzione piuttosto interessante e accessibile al tema e idea principale.

Answer 2

Questo segna il tipo covariante rispetto al tipo di modulo. Supponiamo di avere due mappe le cui chiavi sono dello stesso tipo. Questo + dice che se i valori di una mappa A sono di un sottotipo dei valori dell'altra mappa B, allora il tipo generale di mappa A è un sottotipo di tipo di mappa B. Ho trovato una buona descrizione di questo nel Jane Street blog.