Functors taking recursive module signature as argument

Learning
1

Hi,

I am working on a project where I have a bunch of mutually recursive modules. I am not very happy for one of the modules (let’s call it A) to be recursive with all the other ones, as logically it makes more sense to have it separate, and have my big mutually recursive modules definition depend on that one module. However, this module A is still inductive with one of the modules (call it B) of the mutually recursive modules.

So I would like to make A into a functor, taking a module with the same signature as B. So far so good, but my issue here is that the signature of B is recursive. So ideally I would like to write something like

module rec A :
functor 
(B : 
  sig
    type t
    val to_a : t -> A(B).t
  end
)  
-> sig
  type t
  val to_b : t -> B.t
end
= 
functor
(B : 
  sig
    type t
    val to_a : t -> A(B).t
  end
)  
-> struct
  type t = int
  let to_b = assert false
end

However, this doesn’t work, for the following reason

|     val to_a : t -> A(B).t
                       ^^^^^^
Error: Unbound module B

Indeed, there is no way to indicate that the module signature B. After some googling, I found out that this is indeed one of the limitations of the module system of OCaml. As a workaround, I tried encapsulating the signature into a wrapper module for B’s signature, that I defined mutually recursively with A as follows:

module rec A :
functor (B : B_wrapper.S)  -> sig
  type t
  val to_b : t -> B.t
end
= 
functor (B : B_wrapper.S) -> struct
  type t = int
  let to_b = assert false
end
and B_wrapper :
sig
  module type S = sig
      type t
      val to_a : t -> A(S).t
    end
end =
  struct
    module type S = sig
      type t
      val to_a : t -> A(S).t
    end
  end

This still doesn’t compile, with the following error message

2 | functor (B : B_wrapper.S)  -> sig
                 ^^^^^^^^^^^
Error: Illegal recursive module reference

I understand that the recursive schemes are guarded to prevent inconsistent schemes, but in my case I am pretty sure that what I am doing is in fact consistent. Indeed, I have a version of this working perfectly well when all the modules are mutually recursive. Is there a standard way to achieve what I am trying to do, or a workaround for that kind of scenario?

2

It’s rare to really need recursive modules, if you can share more code we could advice if they are worth the trouble…

Otherwise, it should be possible to break down the issue in two steps:

module A (B : sig type t end) = struct
  type t = Wrap of B.t

  module Make (Bfun : sig val to_a : B.t -> t end) : sig
    val to_b : t -> B.t
  end = struct
    let to_b (Wrap b) = b
  end
end

module A_int = A (struct type t = int end)
module A_fun = A_int.Make (struct let to_a b = A_int.Wrap b end)
3

Thanks a lot, I could adapt your suggestion to my case and achieve what I wanted.

For context, this is for the following project: GitHub - thibautbenjamin/catt: Coherence typechecker for infinity categories, which is a type checker for a custom dependent type theory, that serves as a sort of proof assistant. I am using mutually recursive modules, each one with an abstract datatype, to represent the contexts/types/terms and substitutions in the theory that have been verified by the system. I have also a module defining the syntax of my language before going through the type checking. However, this syntax allows to carry some chunks that were verified, and so I was defining it mutually recursively with the other modules. With your trick, I managed to separate the unchecked syntax from the other module.

1 Like