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
Type alias or module type alias should not be taken into account for signature inclusion #6637
Comments
Comment author: bobot Some makes the criticism that this proposition breaks the property that one can remove all the interfaces and keep the same program at the end, but this property is already not true: a.ml : "let id y x = x" If one remove a.mli, b.ml doesn't compile anymore: |
Comment author: @alainfrisch See also #6356. Why do you restrict the proposal to type aliases, and not arbitrary type definitions? |
Comment author: @lpw25 One thing this breaks is transitivity of signature inclusion. You can remove a type alias and then add a different type alias with the same name, but you cannot just change a type alias. E.g ((struct type t = int end : sig end) : sig type t = float end) works but (struct type t = int end : sig type t = float end) doesn't. |
Comment author: bobot Thank you Alain for the pointer, I though the patch would be more complicated! I limit to aliases because it is already useful and it is clear that doesn't create unsoundness by definition of an alias. Moreover some definitions do have a content at runtime, like exceptions, open types, no? So it becomes more complicated to compile: a.ml : "" |
Comment author: @alainfrisch The idea in #6356 was to allow adding any pure type-level (i.e. types, class types, module types) components. Exceptions, extension constructors, values, classes, modules would still be rejected. |
Comment author: bobot Leo, the transitivity breaking is very interesting. I'm not sure it is worse the trouble but one way to solve the problem is to define the signature inclusion with aliases by:
With this definition However this definition doesn't allow to type first-class module since they don't type modulo substitution: a.ml: a.mli: Error: The implementation test.ml does not match the interface test.cmi: |
Comment author: bobot Perhaps we should discuss in 0006356, since it is the original bug and close this one. But I prefer to stick only with aliases because it is clear what is a type alias and what is not, whereas it is less clear (and implementation dependent I think) which are the pure types and not pure types. |
Comment author: @yakobowski Another possibility would be to use a new toplevel declaration : |
Comment author: @garrigue I agree with Leo: breaking the transitivity of module subtyping looks like a no-no from a theoretical point of view. |
Comment author: bobot The PR #2016 is a way to help for the case of arg.mli where the type alias is added for readability, but I think it is not applicable to the case of set.mli because we want Set.S to be defined and able to be referenced by the users of the library. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
There is now a type t := ... notation in signatures, with the behaviour described here. So I suppose we can close this. (One might want this for module types to, but then we would also need |
Remaining part subsumed by #6356. |
Original bug ID: 6637
Reporter: bobot
Status: acknowledged (set by @damiendoligez on 2014-11-17T22:46:28Z)
Resolution: open
Priority: normal
Severity: feature
Platform: all
OS: all
OS Version: all
Version: 4.02.1
Category: typing
Duplicate of: #6356
Monitored by: @hcarty @yakobowski
Bug description
Often in a .mli one want to add type alias or module type alias for improving the readability of the signature.
For example in arg.mli:
Or for simplifying the writing of other signature:
For example in set.mli:
allows the user to write
module S = Set.S with type elt = usertype
Although these alias do not add any information, the test of signature inclusion compels the user to add them in the implementation
.ml
. In the case ofset.mli
, if one want to add a function in functionSet.Make
, it need to add the implementation in the.ml
the signature and documentation in.mli
, but also the signature in the module type of the.ml
. For avoiding this problem people define these module type alias in a separate file (.ml or .mli only) but it is not satisfactory.The proposition is to accept that a signature declare more aliases than the implementation.
The text was updated successfully, but these errors were encountered: