battitura moduli ricorsive

Question

In Leroy's paper su come moduli ricorsiva vengono digitati in OCaml, è scritto che i moduli vengono controllati in un ambiente fatto di approssimazioni di tipi di moduli:

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

un ambiente {A -> circa (A); B -> circa (B); C -> approx (C)} viene prima creato e quindi utilizzato per calcolare i tipi di A, B e C.

Ho notato che, in alcuni casi, le approssimazioni non sono abbastanza buone, e il typechecking fallisce. In particolare, quando si inseriscono le origini delle unità di compilazione in una definizione di modulo ricorsiva, il typechecking può fallire mentre il compilatore è in grado di compilare le unità di compilazione separatamente.

Tornando al mio primo esempio, ho trovato che una soluzione sarebbe quella di digitare A nell'ambiente approssimato iniziale, ma poi di digitare B in quell'ambiente iniziale esteso con il nuovo tipo calcolato di A, e di digitare C in l'env precedente con il nuovo tipo di B calcolato e così via.

Prima di indagare di più, vorrei sapere se c'è qualche lavoro precedente su questo argomento, dimostrando che tale schema di compilazione per moduli ricorsivi è sicuro o non sicuro? C'è un contro-esempio che mostra un programma non sicuro correttamente digitato con questo schema?

Answer 1

Innanzitutto, notare che Leroy (o Ocaml) non consente module rec senza annotazioni di firma esplicite. Quindi è piuttosto

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

e l'ambiente approssimativa è {A: circa (SA), B: circa (SB), C: circa (SC)}.

Non sorprende che alcuni moduli di controllo tipo siano definiti separatamente, ma non quando definiti in modo ricorsivo. Dopotutto, lo stesso è già vero per le dichiarazioni del linguaggio core: in un "let rec", le ricorrenze ricorsive delle variabili associate sono monomorfiche, mentre con le dichiarazioni "let" separate, è possibile utilizzare le variabili precedenti in modo polimorfico. Intuitivamente, la ragione è che non puoi avere tutta la conoscenza di cui avresti bisogno per dedurre i tipi più liberali prima di aver effettivamente controllato le definizioni.

Per quanto riguarda il tuo suggerimento, il problema con esso è che rende il module rec costrutto asimmetrico, vale a dire l'ordine sarebbe importante in modi potenzialmente sottili. Ciò viola lo spirito delle definizioni ricorsive (almeno in ML), che dovrebbero essere sempre indifferenti all'ordine.

In generale, il problema con la digitazione ricorsiva non è tanto la solidità, quanto piuttosto la completezza. Non si desidera un sistema di tipi che sia indecidibile in generale o la cui specifica sia dipendente da artefatti algoritmici (come l'ordine di controllo).

In una nota più generale, è noto che il trattamento di Ocaml dei moduli ricorsivi è piuttosto restrittivo. C'è stato un lavoro, ad es. di Nakata & Garrigue, che spinge oltre i suoi limiti. Tuttavia, sono convinto che, alla fine, non sarai in grado di ottenere il più liberale possibile (e questo vale anche per altri aspetti del suo sistema di moduli di tipo, ad esempio i funtori) senza abbandonare l'approccio puramente sintattico di Ocaml alla digitazione dei moduli . Ma poi, sono di parte. :)