Implementare gli heap bootstrap di Okasaki in OCaml, perché non lo compila?

Question

(Un non-compilazione esempio minimo può essere trovato alla https://gist.github.com/4044467, vedere di più sfondo di seguito.)

Sto cercando di implementare bootstrap Cumuli introdotti nel capitolo 10 del puramente funzionale struttura dati di Okasaki. Quanto segue è una versione semplificata del mio codice non compilato.

stiamo per implementare un heap con seguente firma:

module type ORDERED = 
sig 
    type t 
    val compare : t -> t -> int 
end 

module type HEAP = 
sig 
    module Elem : ORDERED 

    type heap 

    val empty : heap 
    val insert : Elem.t -> heap -> heap 
    val find_min : heap -> Elem.t 
    val delete_min : heap -> heap 
end 

Diciamo una struttura dati è bootstrap quando la sua attuazione dipende da un'altra implementazione dello stesso tipo di struttura dati. Quindi abbiamo un mucchio come questo (l'effettiva implementazione non è importante):

module SomeHeap (Element : ORDERED) : (HEAP with module Elem = Element) = 
struct 
    module Elem = Element 

    type heap 

    let empty = failwith "skipped" 
    let insert = failwith "skipped" 
    let find_min = failwith "skipped" 
    let delete_min = failwith "skipped" 
end 

Poi, l'heap bootstrap che andremo a realizzare, che può dipendere da qualsiasi implementazione mucchio, dovrebbe avere la seguente firma :

module BootstrappedHeap 
    (MakeH : functor (Element : ORDERED) -> HEAP with module Elem = Element) 
    (Element : ORDERED) : (HEAP with module Elem = Element) 

in modo che possiamo usare in questo modo:

module StringHeap = BootstrappedHeap(SomeHeap)(String) 

L'attuazione di BootstrappedHeap, secondo Okasaki, è come questo:

012.351.641,061 mila

module BootstrappedHeap 
    (MakeH : functor (Element : ORDERED) -> HEAP with module Elem = Element) 
    (Element : ORDERED) : (HEAP with module Elem = Element) = 
struct 
    module Elem = Element 

    module rec BootstrappedElem : 
    sig 
    type t = 
     | E 
     | H of Elem.t * PrimH.heap 
    val compare : t -> t -> int 
    end = 
    struct 
    type t = 
     | E 
     | H of Elem.t * PrimH.heap 
    let compare t1 t2 = match t1, t2 with 
     | H (x, _), H (y, _) -> Elem.compare x y 
     | _ -> failwith "unreachable" 
    end 
    and PrimH : (HEAP with module Elem = BootstrappedElem) = 
    MakeH(BootstrappedElem) 

    type heap 

    let empty = failwith "not implemented" 
    let insert = failwith "not implemented" 
    let find_min = failwith "not implemented" 
    let delete_min = failwith "not implemented" 
end 

Ma questa non è la compilazione! Il messaggio di errore è:

File "ordered.ml", line 52, characters 15-55: 
Error: In this `with' constraint, the new definition of Elem 
     does not match its original definition in the constrained signature: 
     Modules do not match: 
     sig type t = BootstrappedElem.t end 
     is not included in 
     ORDERED 
     The field `compare' is required but not provided 

La linea 52 è la linea

and PrimH : (HEAP with module Elem = BootstrappedElem) = 

Penso BootstrappedElem ha attuato ORDERED in quanto ha sia t e compare, ma non sono riuscito a vedere il motivo per cui il compilatore non riesce a trovare la funzione compare.

Modificare la firma del BootstrappedElem per

module rec BootstrappedElem : ORDERED 

renderà la compilazione, ma questo nasconde il tipo di costruttore di E e T in BootstrappedElem per l'impossibilità di attuare le parti successive.

Il non-compilazione del codice intero possono essere scaricate dal https://raw.github.com/gist/4044281/0ce0336c40b277e59cece43dbadb9b94ce6efdaf/ordered.ml

Answer 1

Credo che questo potrebbe essere un bug nel tipo-checker. Ho ridotto il codice al seguente esempio:

module type ORDERED = 
sig 
    type t 
    val compare : t -> t -> int 
end 


module type CARRY = sig 
    module M : ORDERED 
end 

(* works *) 
module HigherOrderFunctor 
    (Make : functor (X : ORDERED) -> (CARRY with module M = X)) 
= struct 
    module rec Base 
    : (ORDERED with type t = string) 
    = String 
    and Other 
    : (CARRY with module M = Base) 
    = Make(Base) 
end 

(* does not work *) 
module HigherOrderFunctor 
    (Make : functor (X : ORDERED) -> (CARRY with module M = X)) 
= struct 
    module rec Base 
    : sig 
     (* 'compare' seems dropped from this signature *) 
     type t = string 
     val compare : t -> t -> int 
    end 
    = String 
    and Other 
    : (CARRY with module M = (Base : sig type t = string val compare : t -> t -> int end)) 
    = Make(Base) 
end 

non capisco il motivo per cui il primo codice funziona e il secondo (che sembra equivalente) non lo fa. Ti suggerisco di aspettare un po 'per vedere se un esperto viene fornito con una spiegazione (Andreas?), Quindi prendere in considerazione l'invio di a bug report.

In questo caso, una soluzione è quella di legare prima la firma che sembra gestito male:

(* works again *) 
module HigherOrderFunctor 
    (Make : functor (X : ORDERED) -> (CARRY with module M = X)) 
= struct 
    (* bind the problematic signature first *) 
    module type S = sig 
    type t = string 
    val compare : t -> t -> int 
    end 

    module rec Base : S = String 
    and Other : (CARRY with module M = Base) = Make(Base) 
end 

Tuttavia, ciò non è possibile nel vostro ambiente, perché la firma di BootstrappedElem è reciprocamente ricorsivo con BootstrappedHeap.

Una soluzione è evitare apparentemente-delicato with module ... costrutto e sostituirlo con un semplice uguaglianza tipo with type Elem.t = ...:

module BootstrappedHeap 
    (MakeH : functor (Element : ORDERED) -> HEAP with module Elem = Element) 
    (Element : ORDERED) : (HEAP with module Elem = Element) = 
struct 
    module Elem = Element 

    module rec BootstrappedElem : 
    sig 
    type t = 
     | E 
     | H of Elem.t * PrimH.heap 
    val compare : t -> t -> int 
    end = 
    struct 
    type t = 
     | E 
     | H of Elem.t * PrimH.heap 
    let compare t1 t2 = match t1, t2 with 
     | H (x, _), H (y, _) -> Elem.compare x y 
     | _ -> failwith "unreachable" 
    end 
    and PrimH : (HEAP with type Elem.t = BootstrappedElem.t) = 
    MakeH(BootstrappedElem) 

    type heap 

    let empty = failwith "not implemented" 
    let insert = failwith "not implemented" 
    let find_min = failwith "not implemented" 
    let delete_min = failwith "not implemented" 
end 

Si potrebbe anche evitare la ricorsione reciproca e definire sia BootstrappedElem e BootstrappedHeap in un nodo ricorsiva, definendo BootstrappedElemall'interno di il ricorsivo BootstrappedHeap.

module BootstrappedHeap 
    (MakeH : functor (Element : ORDERED) -> HEAP with module Elem = Element) 
    (Element : ORDERED) : (HEAP with module Elem = Element) = 
struct 
    module rec BootstrappedHeap : sig 
    module Elem : sig 
     type t = E | H of Element.t * BootstrappedHeap.heap 
     val compare : t -> t -> int 
    end   
    include (HEAP with module Elem := Elem) 
    end = struct 
    module Elem = struct 
     type t = E | H of Element.t * BootstrappedHeap.heap 
     let compare t1 t2 = match t1, t2 with 
     | H (x, _), H (y, _) -> Element.compare x y 
     | _ -> failwith "unreachable" 
    end 
    include (MakeH(Elem) : HEAP with module Elem := Elem) 
    end 

    module Elem = Element 

    type heap 

    let empty = failwith "not implemented" 
    let insert = failwith "not implemented" 
    let find_min = failwith "not implemented" 
    let delete_min = failwith "not implemented" 
end 

Questo stile corrisponde naturalmente alla vostra decisione di incorporare Elem nella firma HEAP e utilizzando with module ... per la raffinatezza. Un'altra soluzione sarebbe stata quella di definire HEAP come un functor che restituisce una firma, usata come HEAP(Elem).S, e suppongo che uno stile ricorsivo differente avrebbe potuto essere scelto. Per non dire che sarebbe stato meglio: penso che lo stile del "modulo astratto" sia più conveniente.