Un extraño ejemplo de tipeo en Ocaml

Question

es bastante extraño que este fragmento de ocaml esté bien escrito por el topevel. Mire la estructura, si g es del tipo int-> int como se muestra en el toplevel, la parte h x = g x de la estructura no podría obtener unificado por tipo. Entonces, ¿alguien puede aclarar un poco?

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

Esta es la respuesta del topelevel:

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

Answer 1

Lo importante para entender aquí es que OCaml realiza la inferencia de tipo de forma compositiva, es decir, inferirá primero el tipo de struct ... end y solo entonces coincidirá con los tipos inferidos contra sig ... end para verificar que la estructura realmente implementa la firma.

Por ejemplo, si se escribe

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

continuación OCaml estarán contentos, ya que verá que f tiene un tipo polimórfico 'a -> 'a que puede ser especializado para el tipo requerido int -> int. Como el sig ... end hace Monkey opaco, es decir, la firma oculta la implementación, le dirá que f tiene el tipo int -> int, aunque la implementación real tiene un tipo polimórfico.

En su caso particular OCaml primera infiere que g tiene tipo 'a -> 'a, y después de que el tipo de h es 'a -> 'a también. Por lo tanto, concluye que la estructura tiene el tipo

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

A continuación, la firma se compara con la dada. Como una función del tipo 'a -> 'a se puede especializar en int -> int y string -> string OCaml concluye que todo está bien. Por supuesto, el objetivo de utilizar sig ... end es opacar la estructura (la implementación está oculta), por lo que el toplevel no no expone el tipo polimórfico de g y h.

Aquí es otro ejemplo que muestra cómo funciona 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 respuesta es

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

diría que la tipificación string -> string no se aplica a g hasta que se exporta del módulo. Dentro del módulo (ya que no le da un tipo) tiene el tipo 'a -> 'a. (Descargo de responsabilidad: no soy un experto en módulos, intento aprender sin embargo)