Understanding functors in OCaml

Question

I'm quite stuck with the following functor problem in OCaml. I paste some of the code just to let you understand. Basically

I defined these two modules in pctl.ml:

module type ProbPA = sig
  include Hashtbl.HashedType  
  val next: t -> (t * float) list
  val print: t -> float -> unit
end

module type M = sig
  type s  
  val set_error: float -> unit
  val check: s -> formula -> bool
  val check_path: s -> path_formula -> float
  val check_suite: s -> suite -> unit
end

and the following functor:

module Make(P: ProbPA): (M with type s = P.t) = struct
  type s = P.t
  (* implementation *)
end

Then to actually use these modules I defined a new module directly in a file called prism.ml:

type state = value array
type t = state
type value =
  | VBOOL of bool
  | VINT of int
  | VFLOAT of float
  | VUNSET
(* all the functions required *)

From a third source (formulas.ml) I used the functor with Prism module:

module PrismPctl = Pctl.Make(Prism)
open PrismPctl

And finally from main.ml

open Formulas.PrismPctl
(* code to prepare the object *)
PrismPctl.check_suite s.sys_state suite (* error here *)

and compiles gives the following error

Error: This expression has type Prism.state = Prism.value array but an expression was expected of type Formulas.PrismPctl.s

From what I can understand there a sort of bad aliasing of the names, they are the same (since value array is the type defined as t and it's used M with type s = P.t in the functor) but the type checker doesn't consider them the same.

I really don't understand where is the problem, can anyone help me?

Thanks in advance

Answer 1

(You post non-compilable code. That's a bad idea because it may make it harder for people to help you, and because reducing your problem down to a simple example is sometimes enough to solve it. But I think I see your difficulty anyway.)

Inside formulas.ml, Ocaml can see that PrismPctl.s = Pctl.Make(Prism).t = Prism.t; the first equality is from the definition of PrismPctl, and the second equality is from the signature of Pctl.Make (specifically the with type s = P.t bit).

If you don't write an mli file for Formulas, your code should compile. So the problem must be that the .mli file you wrote doesn't mention the right equality. You don't show your .mli files (you should, they're part of the problem), but presumably you wrote

module PrismPctl : Pctl.M

That's not enough: when the compiler compiles main.ml, it won't know anything about PrismPctl that's not specified in formulas.mli. You need to specify either

module PrismPctl : Pctl.M with type s = Prism.t

or, assuming you included with type s = P.t in the signature of Make in pctl.mli

module PrismPctl : Pctl.M with type s = Pctl.Make(Prism).s