Tipi di modulo OCaml e compilazione separata

Question

Sto leggendo tramite OCaml lead designer's 1994 paper on modules, types, and separate compilation. (gentilmente indicato da Norman Ramsey in another question). Comprendo che il documento discute le origini del sistema di firma/tipo di modulo presente in OCaml. Si, l'autore propone l'interpretazione opaca delle dichiarazioni di tipo nelle firme (per consentire la compilazione separata) insieme alle dichiarazioni del tipo manifest (per espressività). Il tentativo di mettere insieme alcuni esempi del mio per dimostrare il tipo di problemi la firma del modulo di notazione OCaml sta cercando di risolvere Ho scritto il seguente codice in due file:

Nel file di ordering.ml (o .mli - Ho provato sia) (file a):

module type ORDERING = sig 
type t 
val isLess : t -> t -> bool 
end 

e nel file di useOrdering.ml (file di B):

open Ordering 
module StringOrdering : ORDERING 
    let main() = 
    Printf.printf "%b" StringOrdering.isLess "a" "b" 
    main() 

L'idea è di aspettarsi che il compilatore si lamenta (durante la compilazione del secondo file) che non sono disponibili sufficienti informazioni sul modulo sul modulo StringOrdering per digitare l'applicazione StringOrdering.isLess (e quindi motivare la necessità della sintassi with type). Tuttavia, sebbene il file A compili come previsto, il file B fa sì che il 3.11.2 ocamlc si lamenti per un errore di sintassi. Ho capito che le firme avevano lo scopo di permettere a qualcuno di scrivere codice basato sulla firma del modulo, senza accesso all'implementazione (la struttura del modulo).

Confesso che io non sono sicuro circa la sintassi: module A : B che ho incontrato in this rather old paper on separate compilation ma mi fa chiedere se esiste la sintassi tale o simile (senza coinvolgere funtori) per permettere a qualcuno di scrivere il codice solo sulla base del tipo di modulo, con l'attuale struttura del modulo fornita al momento del collegamento, simile a come si possono usare i file *.h e *.c in C/C++. Senza una tale capacità sembrerebbe che i tipi di modulo/le firme siano fondamentalmente per sigillare/nascondere l'interno dei moduli o più controlli/annotazioni di tipo esplicito, ma non per la compilazione separata/indipendente.

In realtà, guardando il OCaml manual section on modules and separate compilation sembra che la mia analogia con unità di compilazione C è rotto perché il manuale di OCaml definisce l'unità di compilazione OCaml di essere il duo A.ml e A.mli, mentre in C/C++ i file .h vengono incollati al unità di compilazione di qualsiasi file importato .c.

Answer 1

Il modo giusto di fare una cosa del genere è quello di effettuare le seguenti operazioni:

1. In ordering.mli scrittura:

   (* This define the signature *) 
   module type ORDERING = sig 
       type t 
       val isLess : t -> t -> bool 
   end 
   
   (* This define a module having ORDERING as signature *) 
   module StringOrdering : ORDERING 
   

2. compilare il file: ocamlc -c ordering.mli

3. In un altro file, fare riferimento alla firma compilata:

   open Ordering 
   
   let main() = 
       Printf.printf "%b" (StringOrdering.isLess "a" "b") 
   
   let() = main() 
   

   Quando si compila il file, si ottiene l'errore di tipo previsto (es. string non è compatibile con Ordering.StringOrdering.t). Se si desidera rimuovere l'errore di tipo, è necessario aggiungere il vincolo with type t = string alla definizione di StringOrdering in ordering.mli.

Così rispondere a voi seconda domanda: sì, in modalità bytecode il compilatore ha solo bisogno di conoscere le interfacce vostro stanno a seconda, e si può scegliere quale applicazione utilizzare in fase di collegamento. Per impostazione predefinita, ciò non è vero per la compilazione del codice nativo (a causa delle ottimizzazioni tra moduli) ma è possibile disabilitarlo.

Answer 2

Probabilmente siete semplicemente confusi dalla relazione tra le definizioni di modulo e firma esplicite e la definizione implicita di moduli tramite file .ml/.mli.

In sostanza, se si dispone di un file a.ml e utilizzarlo all'interno di qualche altro file, allora è come se tu avessi scritto

module A = 
struct 
    (* content of file a.ml *) 
end 

Se avete anche a.mli, allora è come se avevi scritto

module A : 
sig 
    (* content of file a.mli *) 
end = 
struct 
    (* content of file a.ml *) 
end 

si noti che questo definisce solo un modulo denominati a, non è un modulo tipo. La firma di A non può avere un nome attraverso questo meccanismo.

Un altro file che utilizza A può essere compilato solo con a.mli, senza fornire a.ml del tutto. Tuttavia, si desidera assicurarsi che tutte le informazioni sul tipo siano rese trasparenti laddove necessario. Ad esempio, si supponga di definire una mappa su interi:

(* intMap.mli *) 
type key = int 
type 'a map 
val empty : 'a map 
val add : key -> 'a -> 'a map -> 'a map 
val lookup : key -> 'a map -> 'a option 
... 

Qui, key è reso trasparente, perché qualsiasi codice client (del modulo IntMap che questa firma descrive) ha bisogno di sapere che cosa è di essere in grado aggiungere qualcosa alla mappa. Il tipo map, tuttavia, può (e dovrebbe) essere mantenuto astratto, poiché un client non deve interferire con i dettagli dell'implementazione.

La relazione con i file di intestazione C è che quelli sostanzialmente solo consentono tipi trasparenti. In Ocaml, hai la scelta.

Answer 3

module StringOrdering : ORDERING è una dichiarazione di modulo. È possibile utilizzare questo in una firma, per dire che la firma contiene un campo modulo chiamato StringOrdering e con la firma ORDERING. Non ha senso in un modulo.

È necessario definire un modulo da qualche parte che implementa le operazioni necessarie. La definizione del modulo può essere qualcosa come

module StringOrderingImplementation = struct 
    type t = string 
    let isLess x y = x <= y 
end 

Se si desidera nascondere la definizione del tipo t, è necessario effettuare un modulo diverso in cui la definizione è astratta. L'operazione di creazione di un nuovo modulo rispetto a una vecchia è denominata tenuta e viene espressa tramite l'operatore :.

module StringOrderingAbstract = (StringOrdering : ORDERING) 

Poi StringOrderingImplementation.isLess "a" "b" è ben tipato, mentre StringOrderingAbstract.isLess "a" "b" non può essere digitato dal StringOrderingAbstract.t è un tipo astratto, che non è compatibile con string o qualsiasi altro tipo preesistente. In effetti, è impossibile creare un valore di tipo StringOrderingAbstract.t, poiché il modulo non include alcun costruttore.

Quando si ha un'unità di compilazione foo.ml, è un modulo Foo, e la firma di questo modulo è proposta dal file di interfaccia foo.mli. Cioè, i file foo.ml e foo.mli sono equivalenti alla definizione del modulo

module Foo = (struct (*…contents of foo.ml…*) end : 
       sig (*…contents of foo.mli…*) end) 

Quando si compila un modulo che utilizza Foo, il compilatore guarda solo al foo.mli (o piuttosto il risultato della sua compilazione: foo.cmi), non a foo.ml ¹. Questo è il modo in cui interfacce e compilazione separata si adattano. C ha bisogno di #include <foo.h> perché manca qualsiasi forma di spazio dei nomi; in OCaml, Foo.bar si riferisce automaticamente a bar definito nell'unità di compilazione foo se non è presente alcun altro modulo denominato Foo in ambito.

¹ _{In realtà, il compilatore di codice nativo esamina l'implementazione di Foo per eseguire le ottimizzazioni (inlining). Il controllo del tipo non guarda mai nulla, ma ciò che è nell'interfaccia.}