Create copy of module with modified submodule

Hi,

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

Is there a less contrived way to write that?

2 Likes

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.

2 Likes

@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)

But I don’t think I would go as far as calling this solution less contrived.

But it works, and it is better than repeating all the defnitions. Thank you!

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
2 Likes

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 *)
1 Like

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.

1 Like

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.

I suspect a couple of paragraphs may be enough.