Słaby polimorfizm w OCaml

Question

Jestem trochę zdezorientowany słabym polimorfizmem w OCaml.

Proszę patrz poniższy fragment, gdzie mogę zdefiniować funkcję remember:

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

Kompilator może wnioskować polimorficzne typu 'a -> 'a i cache jest używany lokalnie.

Ale kiedy zmodyfikować powyższy kod do

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

kompilator wywnioskowała słabo polimorficzny typ '_a -> '_a, również wydaje się, że cache jest wspólna dla wywołań remember.

Dlaczego kompilator wypowiada tutaj typ słabo polimorficzny i dlaczego jest udostępniany jako cache?

Co więcej, gdybym ponownie zmienić kod

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

kompilator wnioskuje rodzaj polimorficzny 'a -> 'a -> 'a i cache zostaje lokalnie używany. Dlaczego tak jest?

Answer 1

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

Tutaj cache jest zamknięty przez zwróconą funkcję. Ale w momencie, gdy deklarujemy cache, nie mamy informacji o tym, jaki będzie typ; będzie to określone niezależnie od typu x i zostanie utworzone cache po zdefiniowaniu remember.

Ale ponieważ jest to zamknięcie możemy zrobić coś takiego:

> remember 1 
    1 

Teraz jest jasne, że cache : int option ref ponieważ mamy rzeczywiście coś w nim przechowywane. Ponieważ zawsze istnieje tylko jeden, można zapisać tylko jeden typ.

W następnej zamykasz 2 rzeczy: x i cache. Ponieważ tworzymy nowy ref cache przy każdym wywołaniu remember, ten typ może być w pełni polimorficzny. Powodem, dla którego typ nie jest słabo polimorficzny, jest to, że wiemy, że będziemy przechowywać w nim x i mamy typ x s w chwili, gdy zostanie utworzone cache.

Answer 2

Wydaje się to robić z ograniczeniem wartości. Pełne ograniczenie wartości (jak w SML) całkowicie odrzuciłoby twój kod. Słabo polimorficzne typy są opisane w artykule „rozluźnienie Restriction Value” Jacques Garrigue, które wprawdzie tylko natknął po przeczytaniu swoje pytanie:

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

Fakt cache jest współużytkowane przez inwokacji powinno być, jeśli oczywiste masz poprawny model mentalny tego, co oznacza kod ML. Definiujesz dwie wartości: remember i cache. Zagnieżdżanie powoduje, że zakres cache jest prywatny dla bloku.

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) 

W powyższych dwóch wersjach remember jest funkcja „bezpośredni”, za każdym razem to nazwać jak remember 1 będzie zainicjować cache do ref None, prawda? Tak naprawdę nic nie pamięta, cache nie jest dzielony między wywołania remember.

---

W innej wersji:

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

jest inaczej. remember wciąż jest funkcją na pewno, jednak prawdziwą częścią, która definiuje jej zawartość jest (fun x -> match ...). Obejmuje on cache, a pamięć podręczna jest inicjowana raz i będzie tylko raz. Tak więc cache jest dzielone między przyszłe połączenie remember.