escribiendo módulos recursivas

Question

En Leroy's paper sobre cómo los módulos recursiva se escriben en OCaml, está escrito que los módulos se comprueban en un entorno hecho de aproximaciones de los tipos de módulos:

module rec A = ... and B = ... and C = ... 

Un entorno {A -> aprox (A); B -> aproximadamente (B); C -> approx (C)} primero se construye, y luego se usa para calcular los tipos de A, B y C.

Me di cuenta de que, en algunos casos, las aproximaciones no son lo suficientemente buenas y la comprobación de tipos falla. En particular, cuando se colocan fuentes de unidades de compilación en una definición de módulo recursivo, la comprobación de tipo puede fallar, mientras que el compilador pudo compilar las unidades de compilación por separado.

Volviendo a mi primer ejemplo, encontré que una solución sería escribir A en el entorno aproximado inicial, pero luego escribir B en ese entorno inicial extendido con el nuevo tipo calculado de A, y escribir C en el env anterior con el nuevo tipo computado de B, y así sucesivamente.

Antes de investigar más, me gustaría saber si hay algún trabajo previo sobre este tema, mostrando que dicho esquema de compilación para módulos recursivos es seguro o inseguro? ¿Hay un contraejemplo que muestre un programa inseguro correctamente escrito con este esquema?

Answer 1

En primer lugar, tenga en cuenta que Leroy (o Ocaml) no permite module rec sin anotaciones de firma explícitas. Así que es más bien

module rec A : SA = ... and B : SB = ... and C : SC = ... 

y el medio ambiente es aproximativo {R: aprox (SA), B: aprox (SB), C: aprox (SC)}.

No es sorprendente que algunos módulos comprueben el tipo cuando se definen por separado, pero no cuando se definen recursivamente. Después de todo, lo mismo ya es cierto para las declaraciones de lenguaje central: en un 'let rec', las ocurrencias recursivas de las variables vinculadas son monomórficas, mientras que con las declaraciones separadas 'let', puede usar las variables previas polimórficamente. Intuitivamente, la razón es que no puede tener todo el conocimiento que necesitaría para inferir los tipos más liberales antes de que realmente haya verificado las definiciones.

Respecto a su sugerencia, el problema es que hace que la construcción module rec sea asimétrica, es decir, el orden sería importante en formas potencialmente sutiles. Eso viola el espíritu de las definiciones recursivas (al menos en ML), que siempre debe ser indiferente al orden.

En general, el problema con el tipado recursivo no es tanto la solidez, sino más bien la integridad. No desea un sistema de tipo que sea indecidible en general, o cuya especificación dependa de artefactos algorítmicos (como verificar el orden).

En una nota más general, es bien sabido que el tratamiento de Ocaml de los módulos recursivos es bastante restrictivo. Ha habido trabajo, p. por Nakata & Garrigue, que lleva sus límites más allá. Sin embargo, estoy convencido de que, en última instancia, no podrá ser tan liberal como desee (y eso se aplica también a otros aspectos de su sistema de módulos de tipo, por ejemplo, funtores) sin abandonar el enfoque puramente sintáctico de Ocaml para el tipado de módulos. . Pero entonces, soy parcial. :)