Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Keep equation on module type while strengthening #6333

Closed
vicuna opened this issue Feb 28, 2014 · 5 comments
Closed

Keep equation on module type while strengthening #6333

vicuna opened this issue Feb 28, 2014 · 5 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Feb 28, 2014

Original bug ID: 6333
Reporter: @alainfrisch
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:27:04Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.02.0+dev
Fixed in version: 4.02.0+dev
Category: typing
Tags: patch
Related to: #6159
Monitored by: @yallop @yakobowski

Bug description

I suggest to modify the strengthening of module type bindings in signatures in order to keep the equation to the original module type (as we currently do for abstract module types). Concretely, one would change in Mtype.strengthen_sig:

| Sig_modtype(id, decl) :: rem ->
let newdecl =
match decl.mtd_type with
None ->
{decl with mtd_type = Some(Mty_ident(Pdot(p, Ident.name id, nopos)))}
| Some _ ->
decl
in
...

into:

| Sig_modtype(id, decl) :: rem ->
let newdecl =
{decl with mtd_type = Some(Mty_ident(Pdot(p, Ident.name id, nopos)))}
in
...

This changes makes sense, since module type now have a nominal aspect, because of first-class modules.

Several examples of code which would benefit from the change have been posted on the caml-list ("First class modules aliases" thread, Feb. 2014).

Would there be any drawback from this change?

File attachments

@vicuna
Copy link
Author

vicuna commented Mar 3, 2014

Comment author: @garrigue

There is the same problem as with module aliases: since type information is not duplicated, a new dependence on the source is introduced.
Here is an example:
a/a.ml:
module type S = sig val x : int end
b.ml:
include A
c.ml:
module M : B.S = struct let x = 2 end

compiled with:
ocamlc -c a/a.ml
ocamlc -I a -c b.ml
ocamlc -c c.ml

This would not work anymore, and I do not even see a workaround (we are already using include here).

If we really see module types as having a nominal aspect, the correct thing to do would rather be to add a separate "manifest" field, just like for type definitions.
Another approach would be to make them "more" structural, i.e. to check equivalence of signatures, at least in simple cases.
This shouldn't be that hard in practice, but we delayed it until now.

@vicuna
Copy link
Author

vicuna commented Mar 3, 2014

Comment author: @alainfrisch

Do you think it is going to be a problem in practice? If the user deliberately wants to hide a.cmi when compiling c.ml, he could accept the burden of creating a proper b.mli which expands the definition for S. And one could also argue that keeping a symbolic reference to A.S reduces the size of b.cmi, which is nice.

Otherwise, would it be possible to expand module type aliases only while saving the signature?

And yes, a solution based on a more structural comparison of package types would probably be a nicer approach to fixing this.

@vicuna
Copy link
Author

vicuna commented Mar 4, 2014

Comment author: @garrigue

I just uploaded a patch that does the "right thing".
I.e., provide structural comparison and subtyping for first-class module signatures.
This should not be that costly.
The only thing we loose is that it becomes very hard to ensure that two signatures
are incompatible, so if you use them as type indices you won't be able to discard cases.
(Which I think doesn't matter at all)
Here are a few examples using it:

module type S = sig type u type t end;;
module type S' = sig type t = int type u = bool end;;

(* ok to convert between structurally equal signatures, and parameters
are inferred *)
let f (x : (module S with type t = 'a and type u = 'b)) = (x : (module S'));;
let g x = (x : (module S with type t = 'a and type u = 'b) :> (module S'));;

(* with subtyping it is also ok to forget some types )
module type S2 = sig type u type t type w end;;
let g2 x = (x : (module S2 with type t = 'a and type u = 'b) :> (module S'));;
let h x = (x : (module S2 with type t = 'a) :> (module S with type t = 'a));;
let f2 (x : (module S2 with type t = 'a and type u = 'b)) =
(x : (module S'));; (
fail )
let k (x : (module S2 with type t = 'a)) =
(x : (module S with type t = 'a));; (
fail *)

(* but you cannot forget values (no physical coercions) )
module type S3 = sig type u type t val x : int end;;
let g3 x =
(x : (module S3 with type t = 'a and type u = 'b) :> (module S'));; (
fail *)

@vicuna
Copy link
Author

vicuna commented Mar 4, 2014

Comment author: @garrigue

By the way, there remains another question: whether to allow using first class modules without defining a module type in advance.
Since comparison is now structural, there is no obstacle to do that.
On the other, you probably don't want to see such types printed, just like with objects...

@vicuna
Copy link
Author

vicuna commented Mar 10, 2014

Comment author: @garrigue

Structural comparison of first class module types merged into trunk at revision 14450.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants