Incluso modulo, coercing

Question

Sto scrivendo un post su come utilizzare il sistema di moduli di OCaml al posto del sistema OO di Java (una prospettiva divertente). Mi sono imbattuto in qualcosa che non capisco di coercizione. Di seguito è riportato un modulo base e due moduli che lo include:

module M = struct 
    type t = int 
    let make() = 1 
end 
module A = struct 
    include M 
end 
module B = struct 
    include M 
end 

Ora A.t e B.t è lo stesso tipo! Perché? E 'evidient se fate

let a = A.make();; 
let b = B.make();; 
[a;b] --> A.t list (* ? *) 

So che è possibile prevenire questo con le abbreviazioni di tipo privato, e quindi utilizzare costringere se si vuole metterli nella stessa lista. La mia domanda è: perché non è già stato fatto? Come può il compilatore sapere che A.t e B.t provengono dallo stesso tipo di base?

saluti
Olle

Answer 1

Ci sono molti casi in cui si desidera che quei due moduli siano compatibili. Un caso d'uso più semplice è il seguente:

module Hashtbl = struct ... (* definition in the stdlib *) end 

module ExtHashtbl = struct ... (* my own layer on top of it *) end 

voglio ExtHashtbl.t per essere compatibile con Hashtbl.t, in modo che possa funzioni ExtHashtbl nel bel mezzo di codice utilizzando Hashtbl.t, o di operare su valori che sono state costruite da qualcuno altro che conosce solo la libreria Hashtbl e non le mie cose personali.

Nella teoria dei moduli ML esiste un'operazione denominata "rafforzamento" che arricchisce una definizione di modulo con quante più equazioni possibili, esponendole nella firma. L'idea è che se vuoi avere più astrazione (meno equazioni), puoi sempre usare un tipo di firma per limitarlo, quindi è strettamente più generale avere le equazioni.

La situazione è un po 'diversa nel caso dei funtori. Si consideri che invece di definire A e B come moduli semplici, li funtori sulla firma vuoto aveva fatto:

module A (U : sig end) = struct include M end 
module B (U : sig end) = struct include M end 

Vi sono poi due nozioni distinte functors nei sistemi modulo ML, quelli che vengono chiamati "generativa "(ogni invocazione del funtore genera tipi" freschi "che sono incompatibili con altre invocazioni), e quelli chiamati" applicativi "(tutte le invocazioni del funtore su argomenti uguali hanno tipi compatibili). Il sistema OCaml si comporta in modo applicativo se lo si istanzia con un argomento del modulo che viene denominato (più in generale un percorso ) e in modo generativo se si crea un'istanza con un argomento del modulo non denominato.

Puoi imparare molto di più di quanto tu abbia mai voluto sapere sui sistemi di moduli OCaml nel documento Xavier Leroy 2000 A Modular Module System (PDF) (dalla pagina web A few papers on Caml). Troverete anche esempi di codice di seguito per tutte le situazioni che ho descritto sopra.

Il lavoro recente sui sistemi di moduli ML, in particolare da Anreas Rossberg, Derek Dreyer e Claudio Russo, tende a portare un diverso punto di vista alla classica distinzione tra funtori "applicativi" e "generativi". Affermano che dovrebbero corrispondere a funtori "puri" e "impuri": i funtori la cui applicazione produce effetti collaterali dovrebbero sempre essere generativi, mentre i funtori che portano solo termini puri dovrebbero essere applicativi di default (con qualche costrutto di tenuta per forzare l'incompatibilità, con la presente fornendo astrazione).

module type S = sig 
    type t 
    val x : t 
end;; 

module M : S = struct 
    type t = int 
    let x = 1 
end;; 

(* definitions below are compatible, the test type-checks *) 
module A1 = M;; 
module B1 = M;; 
let _ = (A1.x = B1.x);; 

(* definitions below are each independently sealed with an abstract 
    signature, so incompatible; the test doesn't type-check *) 
module A2 : S = M;; 
module B2 : S = M;; 
let _ = (A2.x = B2.x);; 
(*This expression has type B2.t but an expression was expected of type A2.t*) 


(* note: if you don't seal Make with the S module type, all functor 
    applications will be transparently equal to M, and all examples below 
    then have compatible types. *) 
module Make (U : sig end) : S = M;; 

(* same functor applied to same argument: 
    compatible (applicative behavior) *) 
module U = struct end;; 
module A3 = Make(U);; 
module B3 = Make(U);; 
let _ = (A3.x = B3.x);; 

(* same functor applied to different argument: 
    incompatible (applicative behavior) *) 
module V = struct end;; 
module A4 = Make(U);; 
module B4 = Make(V);; 
let _ = (A4.x = B4.x);; 
(* This expression has type B4.t = Make(V).t 
    but an expression was expected of type A4.t = Make(U).t *) 

(* same functor applied to non-path (~unnamed) arguments: 
    incompatible (generative behavior) *) 
module A5 = Make(struct end);; 
module B5 = Make(struct end);; 
let _ = (A5.x = B5.x);; 
(* This expression has type B5.t but an expression was expected 
    of type A5.t *) 

Answer 2

non capisco ciò che non è già stato fatto, ma:

• Includere in OCaml è più come un # include in C, se si desidera utilizzare le classi e l'ereditarietà, quindi, c'è quella caratteristica: http://caml.inria.fr/pub/docs/manual-ocaml/manual005.html.
• L'ereditarietà del tipo lascia intuire che make() è unità -> t. Se non vuoi che ocaml indovini il tipo, puoi definire la firma della funzione: http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html#toc14.