Type constraints in module type

Learning
1

Hi,

I would like to understand type constraints in module type.

module type PROC = sig
  type t
  val empty : t
end

module type MODULE = sig
  type t
  module Proc : PROC
  val empty : t
end

module type ICFG = sig
  type t
  module Module : MODULE
  module Proc = Module.Proc
end

module Make (M : MODULE) : ICFG = struct
  module Module = M
  module Proc = M.Proc
  type t = int
end

The above code does not compile and reports the following error:

Error: Signature mismatch:
       ...
       In module Proc:
       Modules do not match:
         sig type t = M.Proc.t val empty : t val to_string : t -> string end
       is not included in
         (module Module.Proc)
  • Is it a desired way to impose type constraint module Proc = Module.Proc?
  • What is the difference between the constraint and module Proc : PROC with type t = Module.Proc.t
  • Why does the above code fail to compile?
1 Like
2

Not a full answer to your questions, but note that if you change

module Proc = M.Proc

to

module Proc = Module.Proc

then compilation succeeds.

The type checker does not propagate all equations between types and modules, which can lead to this sort of situation where you need to give the definition with the needed equality explicitly.

1 Like
3

The root issue is a destructive interference between functors and modules aliases.

When you write

this line defines the module Proc as an alias for the module M.Proc. In particular, this means that for any functor F, F(Proc) = F(M.Proc). For instance, this is a valid identity function

module I = Int
let id : Set.Make(I).t -> Set.Make(Int).t = fun x -> x

This is a quite strong notion of equality, which requires to have a full view of the module Module.

In particular, this notion of equality cannot be applied to functor argument because a functor only has a partial view of its arguments. Consequently, a functor body cannot define any aliases to one of its argument, and functor argument that appears in definition, for instance

module F(X:S) = struct
   module Y = X
end

are expanded to

module F(X:S) = struct
  module Y = struct include X end
end

And this is the root of the issue at hand, indeed in your functor body

module Make (M : MODULE) : ICFG = struct
  module Module = M
  module Proc = M.Proc
  ...
end

the two modules definitions are expanded to

module Module = struct include M end
module Proc = struct include M.Proc end

which means that both modules Module are fresh copy of respectively the module M and the module M.Proc. Moreover, since the two copy are unrelated, the body doesn’t satisfy the signature

module Module: Module
module Proc = Module.Proc

because the module Proc is not an alias for Module.Proc but an independent copy of this module.

In your specific case, this can be fixed by rephrasing the definition as

module Module = M (* create a new fresh module *)
module Proc = Module.Proc (* create an alias to the submodule `Proc` from above *)

as suggested by @jjb. However, in general it is often better to avoid creating copy of functor arguments.

7 Likes
4

Thank you so much.

Then, are the following three definitions different?
Probably the first requires an alias as above. The next requires all the types in B.A must be (recursively) the same as A?
The last requires only B.A.t = A.t?

   module B : B_T
   module A = B.A

   module A : A_T
   module B : B_T with module A = A

   module A : A_T
   module B : B_T with type A.t = A.t

In practice which one is more preferred?

5

Yes, the three definitions are different.

The first one makes the module A an alias for B.A

   module B : B_T
   module A = B.A

The second one

 module A : A_T
 module B : B_T with module A = A

replaces the module A inside the module type B_T by

module A: (module type of struct include A end)

if the type of the outer module A is a subtype of the type of the inner submodule A.

While the third one,

   module A : A_T
   module B : B_T with type A.t = A.t

replaces the type t inside the submodule A by

type t = A.t

if the two types are compatibles.

6

Thanks a lot.

Now I better understand but am still not sure what would be a good practice to design a complicated module structures.

It would be appreciated if you could give a general advice.

module type A_T = sig
  type t
end

module type B_T = sig
  module A : A_T

  type t
end

module type C_T = sig
  module B : B_T
  module A = B.A
end

module type D_T = sig
  module C : C_T
  module B = C.B
  module A = B.A
end

(* type checked *)
module MakeC (B : B_T) : C_T = struct
  module B = B
  module A = B.A
end

(* type error *)
module MakeD (C : C_T) : D_T = struct
  module C = C
  module B = C.B
  module A = B.A
end

How can I define MakeD correctly similar to MakeC while exposing the relationship beetween A, B and C? (i.e., B.A = A, C.B = B)

7

It is hard to suggest something without knowing more about what the requirements are on the results of the functor applications in your actual use case. I would proceed by not attempting to have module aliases in the signatures of the results of functor applications (they are not going to work for the reason explained by @octachron). That is, in your use case, what is too weak when replacing C_T and D_T with:

module type C_T = sig
  module B : B_T
  module A : A_T
end

module type D_T = sig
  module C : C_T
  module B : B_T
  module A : A_T
end

I would suggest to try with such definitions of module types and see which additional constraints are needed by the code that uses these functors.

8

OK. Thank you so much.