Polymorphism debole in OCaml

Question

Sono un po 'confuso su polimorfismo debole in OCaml.

vedere il seguente frammento di codice, dove mi definisco una funzione remember:

let remember x = 
    let cache = ref None in 
     match !cache with 
     | Some y -> y 
     | None -> cache := Some x; x 
;; 

Il compilatore può dedurre il tipo polimorfico 'a -> 'a, e cache viene utilizzato a livello locale.

Ma quando modifico il codice sopra in

let remember = 
    let cache = ref None in 
    (fun x -> match !cache with 
     | Some y -> y 
     | None -> cache := Some x; x) 
;; 

il compilatore deduce il tipo debolmente polimorfico '_a -> '_a, anche, sembra che cache è condivisa attraverso invocazioni di remember.

Perché il compilatore deduce qui un tipo debolmente polimorfico e perché è cache condiviso?

Per di più, se cambio nuovamente il codice

let remember x = 
    let cache = ref None in 
    (fun z -> match !cache with 
     | Some y -> z 
     | None -> cache := Some x; x) 
;; 

il compilatore deduce il tipo polimorfico 'a -> 'a -> 'a e cache si abitua a livello locale. Perché è così?

Answer 1

let remember = 
let cache = ref None in 
    (fun x -> match !cache with 
     | Some y -> y 
     | None -> cache := Some x; x) 
;; 

Qui cache viene chiuso dalla funzione restituita. Ma al punto in cui dichiariamo cache, non abbiamo informazioni su quale sarà il tipo; verrà determinato indipendentemente dal tipo di x e cache viene creato quando viene definito remember.

ma poiché questa è una chiusura che possiamo fare qualcosa di simile:

> remember 1 
    1 

Ora è chiaro che cache : int option ref dal momento che abbiamo in realtà memorizzati qualcosa in esso. Poiché c'è sempre uno solo cache, remember è possibile memorizzare solo un tipo.

Nel prossimo si chiudono più di 2 elementi, x e cache. Dal momento che creiamo un nuovo riferimento cache con ciascuna chiamata di remember, il tipo può essere di nuovo completamente polimorfo. Il motivo per cui il tipo non è debolmente polimorfico è perché sappiamo che stiamo per memorizzare x in esso e abbiamo il tipo x s nel momento in cui viene creato cache.

Answer 2

Questo sembra fare con la restrizione del valore. La restrizione del valore completo (come in SML) rigetterebbe del tutto il tuo codice. Leggermente tipi polimorfici sono descritte nel documento "Rilassante restrizione Valore" di Jacques Garrigue, che ho certamente appena imbattuto dopo aver letto la tua domanda:

http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

Il fatto che cache è condivisa attraverso invocazioni dovrebbe essere ovvio se hai un modello mentale corretto di cosa significa il codice ML. Stai definendo due valori, remember e cache. La nidificazione rende semplicemente l'ambito di cache privato al blocco.

Answer 3

let remember x = 
    let cache = ref None in 
     match !cache with 
     | Some y -> y 
     | None -> cache := Some x; x 


let remember x = 
    let cache = ref None in 
    (fun z -> match !cache with 
     | Some y -> z 
     | None -> cache := Some x; x) 

In queste due versioni, remember è una funzione "diretta", ogni volta che si chiama come remember 1, sarà inizializzare cache-ref None, non è vero? Quindi, in realtà, non ricorda nulla, lo cache non è condiviso tra le chiamate remember.

---

nell'altra versione:

let remember = 
    let cache = ref None in 
    (fun x -> match !cache with 
     | Some y -> y 
     | None -> cache := Some x; x) 

è diverso. remember è ancora una funzione di sicuro, tuttavia, la parte reale che definisce il suo contenuto è (fun x -> match ...). Include cache e la cache viene inizializzata una volta e sarà una sola volta. Quindi cache viene condiviso tra la chiamata futura remember.