haskell - ¿Por qué OCaml a veces requiere expansión eta?

functional-programming

Question

Si tengo la siguiente función OCaml:

let myFun = CCVector.map ((+) 1);;

Funciona bien en Utop, y Merlin no lo marca como un error de compilación. Sin embargo, cuando intento compilarlo, aparece el siguiente error:

Error: el tipo de esta expresión, (int, ''_a) CCVector.t -> (int,'' _b) CCVector.t , contiene variables de tipo que no pueden generalizarse

Sin embargo, si lo extiendo, lo compilo bien:

let myFun foo = CCVector.map ((+) 1) foo;;

Así que me preguntaba por qué no se compila en forma eta-reducida, y también por qué la forma eta-reducida parece funcionar en el nivel superior (Utop) pero no cuando se compila.

Ah, y la documentación para CCVector está here . La parte ''_a puede ser `RO o` RW, dependiendo de si es de solo lectura o mutable.

Answer 1

Lo que tienes aquí es la restricción de polimorfismo de valor de la familia de lenguaje ML.

El objetivo de la restricción es establecer juntos el polimorfismo letar y los efectos secundarios. Por ejemplo, en la siguiente definición:

let r = ref None

r no puede tener un tipo polimórfico ''a option ref . De otra manera:

let () =
r := Some 1; (* use r as int option ref *)
match !r with
| Some s -> print_string s (* this time, use r as a different type, string option ref *)
| None -> ()

se marca incorrectamente el tipo de verificación como válido, pero se bloquea, ya que la celda de referencia r se usa para estos dos tipos incompatibles.

Para solucionar este problema, se realizaron muchas investigaciones en los años 80, y el polimoprismo de valor es uno de ellos. Restringe el polimorfismo solo para permitir los enlaces cuya forma de definición es "no expansiva". La forma expandida de Eta no es expansiva, por lo tanto, su versión eta expandida de myFun tiene un tipo polimórfico, pero no para la versión eta reducida. (Más precisamente hablando, OCaml usa una versión relajada de este polimorfismo de valor, pero la historia es básicamente la misma).

Cuando la definición de dejar vinculación es expansiva, no se introduce ningún polimorfismo, por lo que las variables de tipo se dejan sin generalizar. Estos tipos se imprimen como ''_a en el nivel superior, y su significado intuitivo es: se deben crear instancias de algún tipo concreto más adelante:

# let r = ref None (* expansive *)
val r : ''_a option ref = {contents = None} (* no polymorphism is allowed *)
(* type checker does not reject this,
hoping ''_a is instantiated later. *)

Podemos arreglar el tipo ''_a después de la definición:

# r := Some 1;; (* fixing ''_a to int *)
- : unit = ()
# r;;
- : int option ref = {contents = Some 1} (* Now ''_a is unified with int *)

Una vez corregido, no puede cambiar el tipo, lo que evita el bloqueo anterior.

Este retraso de escritura se permite hasta el final de la escritura de la unidad de compilación. El nivel superior es una unidad que nunca termina y, por lo tanto, puede tener valores con ''_a tipo de variables en cualquier parte de la sesión. Pero en la compilación separada, ''_a variables deben ser instanciadas en algún tipo sin tipo de variables hasta el final del archivo ml :

(* test.ml *)
let r = ref None (* r : ''_a option ref *)
(* end of test.ml. Typing fails due to the non generalizable type variable remains. *)

Esto es lo que está sucediendo con su función myFun con el compilador.

AFAIK, no hay una solución perfecta para el problema del polimorfismo y los efectos secundarios. Al igual que otras soluciones, la restricción del polimorfismo de valor tiene su propio inconveniente: si desea tener un valor polimórfico, debe hacer que la definición sea no expansiva: debe expandir myFun . Esto es un poco malo pero se considera aceptable.

Puedes leer algunas otras respuestas:

• http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles
• ¿Cuál es la diferencia entre ''a y'' _l?
• o buscar por como "valor de restricción ml"