Request: Replace/rename/remove module types

[vicuna]

Original bug ID: 5460
Reporter: @hcarty
Assigned to: @garrigue
Status: assigned (set by @hcarty on 2013-07-30T17:06:25Z)
Resolution: open
Priority: normal
Severity: feature
Version: 3.12.1
Category: typing
Tags: patch
Has duplicate: #6209
Related to: #5514
Monitored by: @gasche @protz thelema @jberdine @yallop @hcarty @garrigue

Bug description

As of the 3.12.x releases, we can replace types (... with type t := t') and remove modules (... with module M := M) in module signatures. It would be useful to be able to do the same thing with module types.

Steps to reproduce

(* This works - module H will not have a Make module in it *)
module H = struct
include (Hashtbl : module type of Hashtbl with module type S := Hashtbl.S)
end

(* In the toplevel (both 3.12.1 and 3.13.0+dev8) this fails with:
"Syntax error: ')' expected, the highlighted '(' might be unmatched"
on "type" in "... with module type S ..." *)
module type S' = sig type t end
module H = struct
include (Hashtbl : module type of Hashtbl with module type S := S')
end

Additional information

This would be useful when extending modules, particularly ones which provide functors and matching signatures.

File attachments

• ocamlbrew.wrMNQO.log
• with-module-type.diffs

[vicuna]

Comment author: @garrigue

I'm not sure I understand the intended semantics.
The constructs with type t := ... and with module M := ... just replace t and M by the corresponding definitions, but you seem to imply that "with module type S := ..." should also remove modules and functors containing S in their signature.
I don't think this new approach would make sense: since module types are purely structural, there is no way to distinguish S from its definition.

Concerning the possibility to substitute a module type, I see no reason it wouldn't be possible.
Note however that this is actually two new constructs:
with module type S = ...
with module type S := ...
I don't see why we should have the second without the first.

[vicuna]

Comment author: @hcarty

I would be quite happy with those two new "with module type" constructs. I don't see any reason why only one or the other should be added.

For some clarification on the original request - "with type t := t'" does replace t with t', but "with module M := M" (where both M modules are the same) removes that module from the signature:

module H = struct
include (Hashtbl : module type of Hashtbl with module Make := Hashtbl.Make)
end

I apologize - looking back at the original post, this is the code I meant to include as the first example. The H module will now be just like Hashtbl, except that there is no H.Make module included.

I don't know if removal makes sense for a module type any more than it does for a normal type. There may be situations where it is useful, but being able to substitute a module type seems more useful.

[vicuna]

Comment author: @garrigue

I implemented the above features experimentally in trunk/experimental/garrigue/with-module-type.diffs
The two syntaxes are available (= and :=), and the right hand side may be any module type.

Your example goes through modulo an instantiation of "statistics":

module H = struct
include (Hashtbl : module type of Hashtbl with
type statistics = Hashtbl.statistics
and module type S := Hashtbl.S)
end

Could you try it and verify that it does what you expect?

[vicuna]

Comment author: @hcarty

I tried to build trunk with this patch applied but I received an error. I can attach the entire build log if that would be helpful.

cd tools; make all
make[2]: Entering directory /home/hcarty/ocamlbrew/mod-diff/build/build/tools' ../boot/ocamlrun ../boot/ocamlc -strict-sequence -nostdlib -I ../boot -c -warn-error A -I ../utils -I ../parsing -I ../typing -I ../bytecomp -I ../asmcomp -I ../driver depend.mli ../boot/ocamlrun ../boot/ocamlc -strict-sequence -nostdlib -I ../boot -c -warn-error A -I ../utils -I ../parsing -I ../typing -I ../bytecomp -I ../asmcomp -I ../driver depend.ml File "depend.ml", line 181, characters 8-261: Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (_, (Pwith_modtype _|Pwith_modtypesubst _)) File "depend.ml", line 1: Error: Error-enabled warnings (1 occurrences) make[2]: *** [depend.cmo] Error 2 make[2]: Leaving directory /home/hcarty/ocamlbrew/mod-diff/build/build/tools'
make[1]: *** [ocamltools] Error 2
make[1]: Leaving directory `/home/hcarty/ocamlbrew/mod-diff/build/build'
make: *** [world.opt] Error 2

[vicuna]

Comment author: @hcarty

Is there any chance that this could be updated and applied to 4.01 before release? If not, is there an updated patch to test against trunk?

[vicuna]

Comment author: @garrigue

I have uploaded (and committed in trunk/experimental/garrigue) a new patch that applies to current trunk and 4.01.
Note that this is a patch for the compiler only, not other tools.
So you should just do "make ocamlc ocaml".

I want this included, I suppose that some lobbying is needed.
Are there other useful examples, where this is not only used to delete components?

[vicuna]

Comment author: @hcarty

It would be useful any time you want to extend a module type. For example, a module type defining the output of a functor. Adding anything to a MyHashtbl.S module type without this patch requires either having duplicate signatures (module MyHashtbl = struct include Hashtbl module type S' = sig include S ... end ... end) or copying and pasting the contents of S to a new file and modifying the result.

In the first case the original S still exists in MyHashtbl which is confusing for someone using the module. In the second case there is a lot of code duplication which would be useful and safer to avoid.

[vicuna]

Comment author: @gasche

I suspect it a bit late to be applied to the release branch (at this point, it would be better if only fixes that do not break things are applied to parts as sensible as the type-checker). But Jacques, I don't see any reason not to apply it to trunk if this is a feature that you want -- you are, after all, the type-system maintainer. It seems to me that it adds regularity to the module/interface language, which is a very good thing.

[vicuna]

Comment author: @garrigue

There was a typo in my note: "I want" -> "If you want".
And to clarify things: as maintainer of the type checker, my job is to fix bugs, but not to add features without first discussing it with other maintainers.
Also, this is too late for 4.01 (but not for 4.02).

Now, on this specific one, my main concern is that the only application example seems to be Hashtbl.
Namely, when a module contains both a direct and a functorial interface, this is needed to fully discard the functor part. I agree that copying the signature by hand is a pain, but adding a feature only for making easier extending one specific module in the standard library seems far-fetched.
This would be more interesting if there were examples using abstract signatures; i.e. substitution, not only removal. Or just demonstrating that this pattern is common enough.

It is also useful to understand better the original role of "with". Namely, it was only intended to allow turning abstract types into type abbreviations. In particular the semantics of "with module" was just to do it for all types in the module (there was no module substitution involved). The introduction of ":=" changed that a bit, as the module is now substituted (in functor applications). However handling module types is another story, so adding it is really an extension, not just adding some "forgotten" case, albeit the code is almost trivial.

To be clear, I'm not at all opposed to this feature, and I do think that it makes sense, but I would like to see more examples before committing to it.

[vicuna]

Comment author: @hcarty

BatMap and BatSet from Batteries are two more examples. It looks like the equivalent modules in Core are too.

[vicuna]

Comment author: @garrigue

Actually, the BatMap and BatSet modules have no such problem, since they define respectively a PMap and a PSet submodule, whose interface can be used for this purpose.

So an alternative proposal would be to add such a submodule in Hashtbl too.
I suppose it is useful for other things too.

[vicuna]

Comment author: @garrigue

Or maybe you meant that adding removal for module types would completely avoid the need for those extra submodules. But we need to be sure that removal is not too cumbersome, and that those submodules are not needed for anything else.

[vicuna]

Comment author: jpdeplaix

I've two more (similar) examples:

• I wanted to do a Exceptionless « pack » module for batteries. So for example, it's easy for BatArray as a:
  module Array = struct
  include BatArray
  include BatArray.Exceptionless
  end
  But some modules contains module signature with an Exceptionless module (BatMap, BatSet, BatHashbtl, …) and I can't override this module type (easily) without this feature.

• The other example is similar: I have a library that provides exception monads and I want a wrapper for the stdlib. So there is the same problems with almost the same modules (Map, Set, …).