OCaml recursive types crossing a "module type ="

Question

I've got a complicated set of constraints (mostly pedagogical) that result in me wanting to do something like this:

type alpha = ... ENV.env ...
and module type ENV = sig
    type env
    val foo : ...alpha...
end

But that's not legal OCaml. For one, you can't have module type ENV = as part of a recursive type definition. (I don't think there's even any version of recursive declarations limited just to module type declarations.) For two, you can't have ENV.env invoking a component of a module type; you can only write M.env where M is an implemented module structure. But if something like the above were legal, it would capture what I'm aiming to do.

Here's a simplified test case that exhibits some of my constraints.

(* M1 is really the contents of an .mli file, not a module *)
module M1 = struct
  type env (* I want env to be opaque or abstract at this point ... *)
  type alpha = A of int | B of env * int
  type beta = C of int | D of alpha
  module type ENV = sig
    type env (* ...but to be unified with this env *)
    val foo : unit -> beta -> unit
    val empty : env
  end
end

(* M2 needs to be in another_file.ml *)
module M2 = struct
  (* here we provide an implementation of M1.ENV *)
  module E1 : M1.ENV = struct
    type env = char
    let foo () _ = ()
    let empty = 'X'
  end

  (* then I'd want this to typecheck, but it doesn't *)
  let _ = M1.B(E1.empty, 0)
end

In M1, the part before the declaration of ENV needs to refer to the env type, but then the declaration of ENV itself needs to refer to some of what occurs in the other part of M1. So it's not clear which should come first. If ENV didn't need to refer to beta, which in turn refers to alpha, I could put ENV at the start of the file and include ENV (as I say above, this is really an .mli file) in order to have access to the env type for the declaration of alpha. I'm not sure if that would really result in the env in alpha being the same as the env in M1.ENV (in OCaml include-ing a module type is said to be just a textual copy of its contents); but in any case I can't do it here because of the interdependencies. So I have to pre-declare type env at the start of M1. It's essential to my needs that we're not in a position in M1 to specify an implementation for env.

The declaration I gave above for M1 is accepted by OCaml, but the two types env aren't unified. That's not surprising, but my task is to find some contortions that will unify them. When we provide an implementation for ENV later, as in M2 above, we want to be able to use it to provide instances of M1.alpha. But currently we're not: M1.B(E1.empty, 0) won't typecheck.

Now there is one solution. I could have M1.alpha use a type variable 'env rather than an abstract type env. But then M1.alpha would need to be parameterized on 'env, and then so too would M1.beta be, and because of the interdependencies in my types, just about every type in the whole project then needs to carry a parameterization on the 'env type, a concrete instance of which we're not able to supply until we get to module M2, further down in the buildchain. This is pedagogically undesirable, as it makes all the types harder to understand, even in contexts where the environments have no immediate relevance.

So I've been trying to figure out if there's some trick I could perform with functors or with first-class modules that would enable me to get the kinds of interdependencies I'm looking for in module M1, and provide an implementation of the env type in a later file, here represented by module M2. I haven't been able to figure such a thing out yet.

Answer 1

I don't know if this is helpful at all, but this tiny example works for me:

# module rec A : sig
    type alpha = B.env list
  end = A    
  and B : sig
    type env
    val foo: A.alpha
  end = struct
    type env = int
    let foo = [3]
  end;;
module rec A : sig type alpha = B.env list end
and B : sig type env val foo : A.alpha end
# B.foo
- : A.alpha = [<abstr>]

It seems to have a structure reminiscent of your initial example, with the restriction that alpha ends up wrapped in a module.