Perché OCaml a volte richiede l'espansione di eta?

Question

Se ho la seguente funzione OCaml:

let myFun = CCVector.map ((+) 1);; 

Funziona bene in Utop, e Merlin non segna come un errore di compilazione. Quando provo a compilarlo, però, ottengo il seguente errore:

Errore: Il tipo di questa espressione, (int, '_a) CCVector.t -> (int,' _B) CCVector.t, contiene digitare variabili che non possono essere generalizzati

Se eta-espanderla però allora compila bene:

let myFun foo = CCVector.map ((+) 1) foo;; 

quindi mi chiedevo il motivo per cui non viene compilato in forma eta-ridotta, e anche perché la forma a ridotto contenuto di eta sembra w ork in the toplevel (Utop) ma non durante la compilazione?

Oh, e la documentazione per CCVector è here. La parte '_a può essere `RO o` RW, a seconda che sia di sola lettura o modificabile.

Answer 1

Quello che hai qui è la restrizione del polimorfismo del valore della famiglia di linguaggio ML.

Lo scopo della restrizione è di accorpare let-polymorphism ed effetti collaterali. Ad esempio, nella seguente definizione:

let r = ref None 

r non può avere un tipo polimorfo 'a option ref. Altrimenti:

let() = 
    r := Some 1;  (* use r as int option ref *) 
    match !r with 
    | Some s -> print_string s (* this time, use r as a different type, string option ref *) 
    | None ->() 

è erroneamente tipo controllato come valida, ma si blocca, in quanto la cella di riferimento r viene utilizzato per questi due tipi incompatibili.

Per risolvere questo problema sono state fatte molte ricerche negli anni '80 e il valore del polymoprhism è uno di questi. Limita il polimorfismo solo per consentire binding la cui forma di definizione è "non espansiva". La forma espansa Eta non è espansiva quindi la versione ampliata di eta di myFun ha un tipo polimorfico, ma non per uno ridotto. (Più precisamente parlando, OCaml usa una versione rilassata di questo valore polimorfismo, ma la storia è fondamentalmente la stessa.)

Quando la definizione di let binding è espansiva non c'è alcun polimorfismo introdotto quindi le variabili di tipo sono lasciate non generalizzate . Questi tipi vengono stampati come '_a nel primo livello, e il loro significato intuitivo è: devono essere istanziati ad un certo tipo di cemento in seguito:

# let r = ref None       (* expansive *) 
val r : '_a option ref = {contents = None} (* no polymorphism is allowed *) 
              (* type checker does not reject this, 
               hoping '_a is instantiated later. *) 

Possiamo definire il tipo '_a dopo la definizione:

# r := Some 1;;        (* fixing '_a to int *) 
- : unit =() 
# r;; 
- : int option ref = {contents = Some 1}  (* Now '_a is unified with int *) 

Una volta risolto, non è possibile modificare il tipo, che impedisce il crash sopra.

Questo ritardo di digitazione è consentito fino alla fine della digitazione dell'unità di compilazione. Il livello massimo è un'unità che non ha mai fine e pertanto è possibile avere valori con le variabili di tipo '_a in qualsiasi punto della sessione.Ma nella compilazione separata, '_a variabili devono essere istanziati ad un certo tipo senza variabili di tipo fino alla fine del file di ml:

(* test.ml *) 
let r = ref None (* r : '_a option ref *) 
(* end of test.ml. Typing fails due to the non generalizable type variable remains. *) 

Questo è ciò che sta accadendo con il tuo myFun funzione con il compilatore.

AFAIK, non esiste una soluzione perfetta al problema del polimorfismo e degli effetti collaterali. Come altre soluzioni, la restrizione del valore del polimorfismo ha il suo unico svantaggio: se si desidera avere un valore polimorfico, è necessario rendere la definizione non espansiva: è necessario eta-espandersi myFun. Questo è un po 'pidocchioso ma è considerato accettabile.

È possibile leggere alcune altre risposte:

• http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles
• What is the difference between 'a and '_l?
• o ricerca per tipo "valore di restrizione ml"