Implementing Okasaki's bootstrapped heaps in OCaml, why doesn't it compile?

Question

(A minimal non-compiling example can be found at https://gist.github.com/4044467, see more background below.)

I am trying to implement Bootstrapped Heaps introduced in Chapter 10 of Okasaki's Purely Functional Data Structure. The following is a simplified version of my non-compiling code.

We're to implement a heap with following signature:

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

We say a data structure is bootstrapped when its implementation depends on another implementation of the same kind of data structure. So we have a heap like this (the actual implementation is not important):

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 

Then, the bootstrapped heap we're going to implement, which can depend on any heap implementation, is supposed to have the following signature:

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

So we can use it like this:

module StringHeap = BootstrappedHeap(SomeHeap)(String)

The implementation of BootstrappedHeap, according to Okasaki, is like this:

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

But this is not compiling! The error message is:

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

The line 52 is the line

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

I think BootstrappedElem did implement ORDERED as it has both t and compare, but I failed to see why the compiler fails to find the compare function.

Change the signature of BootstrappedElem to

module rec BootstrappedElem : ORDERED

will make it compiling but this will hide the type constructor E and T in BootstrappedElem to make it impossible to implement the later parts.

The whole non-compiling code can be downloaded at https://raw.github.com/gist/4044281/0ce0336c40b277e59cece43dbadb9b94ce6efdaf/ordered.ml

Answer 1

I believe this might be a bug in the type-checker. I have reduced your code to the following example:

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

I don't understand why the first code works and the second (which seems equivalent) doesn't. I suggest you wait a bit to see if an expert comes with an explanation (Andreas?), then consider sending a bug report.

In this case, a solution is to first bind the signature that seems mishandled:

(* 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

However, that is not possible in your setting, because the signature of BootstrappedElem is mutually recursive with BootstrappedHeap.

A workaround is to avoid the apparently-delicate with module ... construct and replace it with a simple type equality 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

You could also avoid the mutual recursion and define both BootstrappedElem and BootstrappedHeap in one recursive knot, by defining BootstrappedElem inside the recursive 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

This style corresponds naturally to your decision of embedding Elem in the HEAP signature and using with module ... for refinement. Another solution would have been to define HEAP as a functor returning a signature, used as HEAP(Elem).S, and I suppose a different recursive style could have been chosed. Not to say that this would have been better: I think the "abstract module" style is more convenient.