tipo di funzioni di ordine elevato

Question

se si specifica il tipo (credo) corretto per una funzione di ordine elevato, il compilatore OCaml rifiuta l'utilizzo di secondo secondo tale funzione.

Il codice

let foo():string = 
    let f: ('a -> string) -> 'a -> string = fun g v -> g v 
    in let h = string_of_int 
    in let i = string_of_float 
    in let x = f h 23 
    in let y = f i 23.0 
    in x^y 

conduce alla seguente messaggio di errore

File "test.ml", line 6, characters 14-15: 
Error: This expression has type float -> string 
     but an expression was expected of type int -> string

Quindi il primo utilizzo di f sembra definire il tipo del suo primo parametro da int -> string. Potrei capirlo. Ma quello che non capisco è che l'omissione della restrizione di tipo su f risolve il problema.

let foo():string = 
    let f g v = g v 
    in let h = string_of_int 
    in let i = string_of_float 
    in let x = f h 23 
    in let y = f i 23.0 
    in x^y

E spostando f di portata globale risolve il problema, anche:

let f: ('a -> string) -> 'a -> string = fun g v -> g v 

let foo():string = 
    let h = string_of_int 
    in let i = string_of_float 
    in let x = f h 23 
    in let y = f i 23.0 
    in x^y

Perché è che il primo esempio non compila, mentre quelle successive fanno?

Answer 1

Lasciatemi usare un esempio più semplice che illustra il problema.

# let cons0 (x : 'a) (y : 'a list) = x :: y;; 
val cons0 : 'a -> 'a list -> 'a list = <fun> 
# let cons1 (x : 'a) (y : 'a list) = x :: y in cons1 1 [];; 
- : int list = [1] 
# let cons2 (x : 'a) (y : 'a list) = x :: y in (cons2 1 [], cons2 true []);; 
This expression has type bool but is here used with type int 
# let cons3 x y = x :: y in (cons3 1 [], cons3 true []);; 
- : int list * bool list = ([1], [true]) 

cons0 è una definizione funzione polimorfica, definita nell'ambito globale. È solo un involucro banale per l'operatore ::. Non sorprende che la definizione funzioni. cons1 è quasi lo stesso di cons0, con la differenza che il suo ambito è limitato all'espressione nel corpo in. Il cambio di scopo sembra innocuo, e abbastanza sicuro, è tipologicamente. cons3 ha di nuovo la stessa funzione, senza annotazioni di tipo, e possiamo usarlo polimorficamente nel corpo in.

Quindi cosa c'è che non va con cons2? Il problema è l'ambito di 'a: è l'intera frase di livello superiore.La semantica della frase che definisce cons2 è

for some type 'a, (let cons2 (x : 'a) (y : 'a list) = ... in ...) 

Da 'a devono essere compatibili con int (dovuto cons3 1 []) e con bool (a causa di cons3 true [], non v'è alcuna possibilità di istanziazione 'a. Pertanto la frase è mal digitato.

Se vi piace pensare a ML digitazione in termini del suo algoritmo di solito tipo di inferenza, ogni variabile esplicita dell'utente introduce una serie di vincoli nella algoritmo di unificazione. Qui i vincoli sono 'a = "type of the parameter x" e ' = "type of the parameter y". Ma la sco pe di 'a è l'intera frase, non è generalizzata in alcun ambito interno. Quindi, int e bool terminano entrambi unificati per lo 'a non generalizzato.

Versioni recenti OCaml introduce variabili di tipo scoped (come in Niki Yoshiuchi's answer). Lo stesso effetto si sarebbe potuto ottenere con un modulo locale nelle versioni precedenti (≥2.0):

let module M = struct 
    let cons2 (x : 'a) (y : 'a list) = x :: y 
    end in 
(M.cons2 1 [], M.cons2 true []);; 

(standard MLers nota:. Questo è un posto dove OCaml e SML differiscono)

Answer 2

Questo è un vero capolavoro e non sarei sorpreso se si tratta di un bug del compilatore. Detto questo, si può fare ciò che si vuole nominando esplicitamente il tipo:

let f (type t) (g: t->string) (v: t) = g v in 

Dal manuale: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#htoc108

Edit:

questo funziona anche:

let f g v:string = g v in 

che ha il tipo di firma che stai cercando: ('a -> string) -> 'a -> string

Strano che non funzioni quando si annota il tipo degli argomenti.

EDIT:

annotazioni di tipo polimorfici hanno una sintassi speciale:

let f: 'a. ('a -> string)-> 'a -> string = fun g v -> g v in 

E il tipo è richiesto di essere polimorfico: http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc79

Answer 3

Come punto di riferimento , l'equivalente F #

let foo():string = 
    let f: ('a -> string) -> 'a -> string = fun g v -> g v 
    let h = string 
    let i = string 
    let x = f h 23 
    let y = f i 23.0 
    x^y 

compila.