How exactly do type constraints work?

Learning
1

Hi all, I have two modules, A and B, which I’d like to type with signatures as shown below. These modules are recursive (A.t refers to B.t and vice-versa), but I’d like their signatures to be independent, both because I want to give them separate names and to avoid unexpected (?) typing error related to aliasing of types defined in recursive modules · Issue #7622 · ocaml/ocaml · GitHub.

module type A_s = sig
  type b_t
  type t = Empty_a | A_of_b of b_t
end

module type B_s = sig
  type a_t
  type t = Empty_b | B_of_a of a_t
end

module type S = sig
  type a_t
  type b_t
  module Term : A_s with type t = a_t and type b_t = b_t
  module Scope : B_s with type t = b_t and type a_t = a_t
end

My hope was that by including b_t in A_s and a_t in B_s I could write the signatures without reference to each other. Unfortunately this doesn’t compile with a message that (I don’t really think makes sense, but) seems to be the same as in the Github issue linked above.

❯ ocaml test.ml
File "./test.ml", line 14, characters 25-37:
14 |   module Term : A_s with type t = a_t and type b_t = b_t
                              ^^^^^^^^^^^^
Error: This variant or record definition does not match that of type a_t
       Their kinds differ.

I also tried a variation on this:

module type S = sig
  type a_t = Empty_a | A_of_b of b_t
  and b_t = Empty_b | B_of_a of a_t
  module Term : A_s with type t = a_t and type b_t = b_t
  module Scope : B_s with type t = b_t and type a_t = a_t
end

No luck.

❯ ocaml test.ml
File "./test.ml", line 14, characters 25-37:
14 |   module Term : A_s with type t = a_t and type b_t = b_t
                              ^^^^^^^^^^^^
Error: This variant or record definition does not match that of type a_t
       Constructors do not match:
         A_of_b of b_t
       is not compatible with:
         A_of_b of b_t/2
       The types are not equal.

So, my question is twofold. (1) Is there a way to do what I’m trying? (hopefully it’s clear) And (2) what’s a good source of information on how type constraints work? The OCaml manual is great but doesn’t seem to go into as much depth as I need here.

2

Your second variant works if your order correctly the substitutions:

module type S = sig
  type a_t = Empty_a | A_of_b of b_t
  and b_t =  Empty_b | B_of_a of a_t
  module Term : A_s with type b_t = b_t and type t = a_t
  module Scope : B_s with type a_t = a_t and type t = b_t
end
3

What determines the correctness of the order here?

4

In brief, the substitutions are done in order.

The substitution with type b_t = b_t adds the equality between the type b_t defined in A_s and the external type b_t. This substitution is always valid because b_t is abstract in A_s.

The second substitution with type t = a_t adds an equality the two types. However, since the definition of a_t in A_s is not abstract, the two definitions must match. In other words, the A_s version of

type a_t = Empty_a | A_of_b of b_t

should be compatible with the outer S version. This is only the case if the inner b_t in A_s and the outer b_t in S are equal.

2 Likes
5

Thanks @octachron! This was exactly what I needed.

I ended up using octachron’s solution, with the small tweak of destructive substitution, to prevent exposing a_t and b_t.

module type S = sig
  type a_t = Empty_a | A_of_b of b_t
  and b_t = Empty_b | B_of_a of a_t
  module Term : A_s with type b_t := b_t and type t = a_t
  module Scope : B_s with type a_t := a_t and type t = b_t
end

Also, I’ve only started to read it, but Leroy’s Manifest types, modules, and separate compilation looks like a good reference.

1 Like