I’m confused about how to handle module equalities when building up a hierarchy of functor applications. Here is a shortened version of my situation:
module A = (struct module Asub end : SA)
module B = (struct module Bsub end : SB)
module C (A:SA) (B:SB) = struct module A = A module B = B ... end
module D (A:SA) (B:SB) = struct module C' = C (A) (B) ... end
In reality, D is a sort of add-on module providing optional functionality that is sometimes needed. Then I have both an instance of C and and instance of D available at top-level:
module Ctop = C (A) (B)
module Dtop = D (A) (B)
and I would like to ensure that C' inside Dtop and Ctop are seen as identical. I tried something along the lines of
module Dtop_ = D (A) (B)
module Dtop = (Dtop_ : module type of Dtop_ with module C' = Ctop)
but this is rejected because of missing type equalities in submodules of C' (at least that’s how I interpret the errors).
How can I handle this situation in an ergonomic way? Or can I restructure the hierarchy in a simpler way?
FWIW, For the functionality in D I actually only need the values in C. I made D a functor of A and B only because I don’t have an input signature for a C argument available: the functor C is not applied yet with concrete inputs when D is defined.
[Edit] TL; DR for posterity: The root cause was that in
module F (X:S) : sig
module X : S
= struct
module X = X
end
X.t and F(X).X.t are not known to be the same type. If X.t is abstract, they will be incompatible! For this reason, re-exporting input modules from functors requires great care in adding type equalities and is perhaps best avoided!
Otherwise, this is kinda weird but module type of struct include M end can have more equalities than module type of M so maybe module Dtop = (Dtop_ : module type of struct include Dtop_ end with module C' = Ctop) would work.
Yes, I think this would work. But it’s contrary to the importance/size of the modules: C is used often and is big, D is small and used only sometimes as an add-on, typically further down in application code.
That’s interesting and mysterious: why/when is struct include D end something different than D? I could see a difference if D is constrained by a signature perhaps?
This is discussed briefly in the manual. The crux of the distinction is that module type of struct include D end produces a signature where the type (and module?) fields are strengthened with equations to their correspondents in D, while include module type of D more literally includes the inferred signature or D, without strengthening it with equations back to D.
Can you show an actual simplified example that (fails to) compile, including the exposed types of C and D ? What you want is perfectly possible thanks to applicative functors, but it depends on the details of the various module types involved.
Ok, i managed to put together an example which I think shows the same problem. In so doing, I also learned that module F (I:S) = struct module I = I end does not actually constrain the signature of F.I to S which came as a surprise to me. Anyway, after adding signatures inside of functor bodies, I ended up with this:
module type SA = sig type t val of_int: int -> t val print: t -> unit end
module A = struct
type t = int
let of_int i = i
let print = print_int
end
module B (A:SA) = struct
module A = (A:SA)
let print_twice i = A.print i; A.print i
end
module C (A:SA) = struct
module A = (A:SA)
module Bsub = B (A)
let a = Bsub.A.of_int 5
end
module Btop = B (A)
module Ctop = C (A)
let _does_not_work = Btop.print_twice Ctop.a
Actually a simpler example of the same thing may be
module type SA = sig type t val of_int: int -> t val print: t -> unit end
module A = (struct
type t = int
let of_int i = i
let print = print_int
end : SA)
module B (A:SA) = struct
module A = (A:SA)
let print_twice i = A.print i; A.print i
end
module Btop = B (A)
let _does_not_work = Btop.print_twice (A.of_int 3)
One thing I tried was
module Btop' = (Btop: module type of Btop with module A = A)
So, there are sort of several issues. They all stem from the fact that, from the point of view of the module system and equalities of modules (M : T) ≠ M. Let’s detail:
You over annotate your module types. Unlike what you said, A will be constrained by SA inside the module, but with additional type equalities. Your type annotation only make it so that B.A ≠ C.A ≠ int. As a consequence, if you replace module A = (A : SA) by module A = A, it immediately works. The type infered will be of the form module A : module type of A, which is fully correct.
If you really want the annotation, you need to relay the equality: module A = (A : SA with type t = A.t).
In your first example, the problem is not directly that C(A).Bsub ≠ B(A), but rather that C.A ≠ B.A (since you re-annotated, see the previous remark). Applicativeness then fails. This is because your rebind A and hide its type. If you replace C (without changing B!) by a less ambiguous version as below, it works:
module C (AOrig:SA) = struct
module A = (AOrig:SA)
module Bsub = B (AOrig)
let a = Bsub.A.of_int 5
end
In this case, we see clearly that C(A).Bsub.A = B(A).A = A thanks to the applicative behavior of functors.
Note that there is a WIP extension of the module system called “transparent ascriptions”, written (M <: T), which probably corresponds more to your understanding of what module type constraints should do: (M <: T) preserve equalities on M. In that case, the module system knows that M = (M <: T) (but with a “filtered view”).
Thanks for the explanations. You’re right that removing the :SA constraint in the body of B makes it compile. Great!
As I try to understand the logic here, some comments:
I wrote this because in the following example:
module type SA = sig type t val of_int: int -> t val print: t -> unit end
module A = struct
type t = int
let of_int i = i
let print = print_int
end
module B (A:SA) = struct
module A = A
let print_twice i = A.print i; A.print i
end
module Btop = B (A)
the type of Btop.print_twice is inferred as int -> unit. So (A:SA) in the functor input signature is not enough to make the type abstract when the functor is applied.
I wanted to make A.t abstract because in the real code A is a functor and A.t is a record with fields whose types are inherited from the functor arguments. So outside modules would not know how to work with values of type A.t anyway.
[Edit]: One basic thing I don’t understand, related to your comment
A will be constrained by SA inside the module, but with additional type equalities. Your type annotation only make it so that B.A ≠ C.A ≠ int .
is the following:
module A = (struct ... end : SA)
module B (A:SA) = struct module A = A end
module B_constrained (A:SA) = struct module A = (A:SA) end
Why is B_constrained different from B? To me it would seem natural to think: “A already has module type SA, so nothing more can happen if I constrain it again to the same signature.” This sounds right to me (regular types work like this afaict) but it is incorrect. In fact B_constrained.A is inferred to be of sig type t = B_constrained(A).A.t ...end while B.A is just of sig type t = A.t.
[Edit2]: After reading your entire post, it seems that the proposed (A<:SA) may indeed correspond to my expectation.
[Edit3]: Is this a more correct way of thinking about signature constraints: " Each time I constrain a module as M:SA a fresh type t is generated and ascribed to M.t? This then would break the identity of types even when the same module is constrained twice. This seems to be more or less correct, because the following fails
Signature constraints make a fresh copy of the constrained modules. In other words, in
module M : S = Original
the module M is a new module unrelated to Original, and the only type equalities between the components of M and Original are the one explicitly present in S (for instance if S is sig type t = Original.t end.
So, loosely speaking, “module type constraints can break applicativity.”
I’m trying to apply this insight to solve my original problem. Somehow the signature requirements still get in the way. Here is another version of what I think one of my problems still is.
file basic.mli
module type S = sig
type t
val v : t
val f : t -> unit
end
module Bd (V:S) : sig
module V : module type of V
...
end
file basic.ml
module type S = sig ... end
module Bd (V:S) = struct
module V = V
...
end
The functor Basic.Bd is then called in another functor taking the same arguments, which is meant to extend the functionality in some situations.
file extension.mli
module O (V:Basic.S) : sig
module V : module type of V
module Bd : module type of Basic.Bd (V)
end
file extension.ml
module O (V:Basic.S) = struct
module V = V
module Bd = Basic.Bd (V)
end
now trying to use these modules, in a file application.ml, gives me trouble:
The error message complains that Bd_.v has type Bd_.t while E_.Bd.t was expected.
I was able to get rid of this particular error by adding with module V = V after the signature of Bd in basic.mli. It’s not clear to me why this is needed. Is it because the signature in the .mli acts as a constraint generating fresh types? I don’t want that! But I see no way to get around it since I need to put some signature for Bd in basic.mli in order for it to appear to the outside!
I wonder if the aliasing is not helping. Consider that this is equivalent to:
module Bd (W:S) : sig
module V : module type of W
...
end
In particular, module V : module type of V does not guarantee that the V module returned by the Bd functor has anything to do with the argument of the functor, other than that they both happen to satisfy the same signature. That is not enough for applicativity. For that you need that the returned module is the same as the argument one. Perhaps it would work to use:
Unfortunately that does not help. When I replace module V : module type of V by module V = V in basic.mli, I get a complaint about signature mismatch between
File "basic.ml", line 49, characters 2-14:
Definition of module V/1
File "_none_", line 1:
Definition of module V/2
which is rather enigmatic. (I have also removed the with module V = V constraint)
As a side remark, just to show that in principle all module types are compatible, I can follow @SkySkimmer 's advice and define module Bd_ = O_.Bd in the application file, which fixes the problems but seems like a kludge. It would be more satisfying to be able to have “applicativity all the way through” the functor stack. Or at least to know what would be required to get it or else why it may not be a good idea.
[Edit:] I have also now tried to rename the argument in order to remove shadowing. the version with module Bd (W:S) = struct module V = W ... end and module Bd (W:S) : sig module V : S ... end does seem to work without with constraint! So that’s some progress. Shadowing may have messed something up (although I can’t see where it could have, at present)
Yes, I meant M.
You can’t re-export an argument (without transparent module ascription) because you don’t have a full view of the argument, only a slice constrained by the argument signature.