I am in a situation where I need to create a module Graph that is exactly like Graph0, except that I would like to add a function in Graph.V. Since OCaml does not allow shadowing submodules, the only way I’ve found is to repeat every definition of the original module:
module Graph = struct
type t = Graph0.t
module V = struct
include Graph0.V
let pretty = VImpl.pretty
end
module E = Graph0.E
let fold_pred_e = Graph0.fold_pred_e
let copy = Graph0.copy
(* ... *)
end
It is possible to use destructive substitution of module here:
module type graphm =
module type of struct include Graph0 end with module E := Graph0.E
module Graph = struct
include (Graph0 : graphm)
module E = struct
include Graph0.E
...
end
end
But I don’t think I would go as far as calling this solution less contrived.
@octachron could you explain this? It’s a destructive substitution, but how come E doesn’t appear in the final type of graphm? (I’m trying a simple example in utop)
Because the destructive substitution removes the original definition and replaces all subsequent occurences with the right hand side of the substitution?
This is quite close of the behavior with types and is generally very useful to combine together related signature. For instance, I can start with a ring
module type ring= sig
type t
val (+): t -> t -> t
val ( * ): t -> t -> t
...
end
define a module type for division related operations
module type division= sig type t val (/): t -> t -> t end
and then extend the ring module type to a field module type:
module type field = sig include ring include division with type t := t end
Similarly, if I start with a module type for modules (the abstract algebra ones), it can be quite nice to have an inner submodule for scalars:
module type module' = sig
module Scalar: ring
type vec
type matrix
val det: matrix -> Scalar.t ...
end
But then if I want to extend this module type to a module type for a vector space, I need to promote the Scalar module to a field, and not a ring. At this point, destructive substitution of module is the right solution:
module type vector_space = sig
module Scalar: field
include (module' with module Scalar := Scalar )
...
end
These other examples make sense. But let me make a simple one that matches the OP’s case:
module A = struct
type t = int
module B = struct
let foo x = x
end
end;;
> module A : sig type t = int module B : sig val foo : 'a -> 'a end end
module AP = struct include A end;;
> module AP : sig type t = int module B = A.B end
module AP = struct
include A
module B = struct
include A.B
let bar y = y
end
end;;
> Error: Multiple definition of the module name B.
Names must be unique in a given structure or signature.
(* OK, trying @octachron's trick *)
module type AT = module type of struct include A end with module B := A.B;;
> module type AT = sig type t = int end (* huh? where did B go? *)
module AP = struct
include (A:AT)
module B = struct
include A.B
let bar y = y
end
end;;
> module AP :
sig type t = int module B : sig val foo : 'a -> 'a val bar : 'a -> 'a end end
It succeeded because we got rid of B in AT… but why did B go away in the first place?
First, in this case, since A does not define new types, it is possible to go with the simpler
module type AT = module type of A with module B:= A.B
Then, we can extend
module type a = module type of A
(* ≡ sig type t = int module B : sig val foo : 'a -> 'a end *)
The substitution a with module B := A.B then implies to remove the definition of B, aka module B: sig ... end and replace all ulterior apparition of B by A.B (which is an already defined module). Since no components of B is used after its definition this means that we can simply erase B from the signature
module type at = a with module B:= A.B (* ≡ sig type t =int end *)
It is essentially the same thing as
module type empty = sig type t end with type t := int
(* ≡ sig end *)
I’m not clear about this part. No component of B is used within A, but B has a function foo that can be used from the outside: shouldn’t that appear as part of the signature of A? What made the typechecker decide that B is now irrelevant? I’m missing how the destructive substitution works in this case.
I think that you are confusing the module type level and the module level. At the module type level, there is no concrete values, just a high-level specification of the components of potential modules. All the with constraints manipulate this high-level specification but not modules per se. It is thus perfectly fine to remove mention of a function B.f in a specification.
OK, but how does the typechecker know that this is what we wanted? We never told it to hide B – we just said we’ll substitute the current B with another one (that happened to be the exact same one). It seems like we should be able to remove elements from module types (is weaken the right word for this?), but what we did doesn’t seem like it should have any impact on the type, at least not in a way that seems obvious to me.
Are we expressing weakening (again, not sure if correct here) by tautology? Is that the idea? Would a different syntax like with B :=# signifying deletion make more sense? What am I missing?
The aim of destructive substitution is exactly to remove a component. The substitution part is here to fill any gaping hole in the heart of the signature left by such removal. Consider a universe containing only
`module type s = sig
module Unique: sig type t end
val do_singular_things: Unique.t -> Unique.t -> Unique.t -> Unique.t
end
If we could simply remove the Unique module from the module type s what would be the type of do_singular_things ? 🕳.t -> 🕳.t -> 🕳.t ->🕳.t ? After all, there are no more a type Unique.t to refer to.
Having a substitution part in module type s with module Unique := Example makes it possible to both remove the Unique module and replace its components appearing in s with the corresponding Example component.
Let me say that the fact that this is confusing means it also should get some sort of improved documentation in the manual. I don’t feel qualified to write it, but if @octachron is willing, I’ll be happy to proofread etc.