Uno strano esempio di digitazione in Ocaml

Question

è abbastanza strano che questo frammento di ocaml sia ben digitato dal toplevel. Osserva la struttura, se g è di tipo int-> int come mostrato in toplevel, la parte h x = g x della struttura non sarebbe in grado di ottenere univoco. Quindi qualcuno può chiarire un po '?

module Mymodule : sig 
    val h:int ->int 
    val g: string-> string 
end = struct 
    let g x = x 
    let h x = g x 
end 

Questa è la risposta del topelevel:

module Mymodule : sig val h : int -> int val g : string -> string end 

Answer 1

La cosa importante da capire qui è che OCaml esegue l'inferenza di tipo in modo compositivo, cioè, prima dedurrà il tipo di struct ... end e solo allora corrisponderà ai tipi desunti contro sig ... end per verificare che la struttura implementa realmente la firma.

Ad esempio, se si scrive

module Monkey : sig val f : int -> int end = 
struct 
    let f x = x 
end 

poi OCaml saranno felici, come si vedrà che f ha un tipo polimorfico 'a -> 'a che può essere specializzata per il tipo richiesto int -> int. Dato che lo2 rende Monkey opaco, ovvero la firma nasconde l'implementazione, ti dirà che f ha il tipo int -> int, anche se l'implementazione effettiva ha un tipo polimorfico.

Nel vostro caso particolare OCaml prima ne deduce che g è di tipo 'a -> 'a, e quindi che il tipo di h è 'a -> 'a pure. Quindi conclude che la struttura ha il tipo

sig val g : 'a -> 'a val h : 'a -> 'a end 

Successivamente, la firma viene confrontata con quella data. Poiché una funzione di tipo 'a -> 'a può essere specializzata in int -> int e string -> string OCaml conclude che tutto va bene. Naturalmente, l'intero punto di utilizzo di sig ... end consiste nel rendere la struttura opaca (l'implementazione è nascosta), motivo per cui il numero massimo non espone il tipo polimorfico di g e h.

Ecco un altro esempio che mostra come funziona OCaml:

module Cow = 
struct 
    let f x = x 
    let g x = f [x] 
    let a = f "hi" 
end 

module Bull : sig 
    val f : int -> int 
    val g : 'b * 'c -> ('b * 'c) list 
    val a : string 
end = Cow 

La risposta è

module Cow : 
    sig 
     val f : 'a -> 'a 
     val g : 'a -> 'a list 
     val a : string 
    end 

module Bull : 
    sig 
     val f : int -> int 
     val g : 'a * 'b -> ('a * 'b) list 
     val a : string end 
    end 

Answer 2

direi che la tipizzazione string -> string non viene applicato a g fino a quando è esportato dal modulo. All'interno del modulo (dal momento che non gli viene dato un tipo) ha il tipo 'a -> 'a. (Disclaimer: non sono un esperto di moduli, ma cerco di imparare.)