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

Type alias or module type alias should not be taken into account for signature inclusion #6637

Closed
vicuna opened this issue Oct 29, 2014 · 13 comments

Comments

@vicuna
Copy link

vicuna commented Oct 29, 2014

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:

type key = string
type doc = string
type usage_msg = string
type anon_fun = (string -> unit)

Or for simplifying the writing of other signature:

For example in set.mli:

module type S =
  sig
    [...]
  end

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 of set.mli, if one want to add a function in function Set.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.

module M : sig
   type t = int
   module type S =  sig val f: t -> t end
 end = struct end
@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

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"
a.mli: "val id: unit -> int -> int"
b.ml : "let f = A.id ()"

If one remove a.mli, b.ml doesn't compile anymore:
File "b.ml", line 1, characters 8-15:
Error: The type of this expression, '_a -> '_a,
contains type variables that cannot be generalized

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

Comment author: @alainfrisch

See also #6356.

Why do you restrict the proposal to type aliases, and not arbitrary type definitions?

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

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.

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

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 : ""
a.mli: "exception A"

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

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.

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

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:

  1. Apply the substitution given by the aliases in the two signatures
  2. Check the inclusion without taking into account the alias fields.

With this definition (struct type t = int end : sig type t = float end) is accepted.

However this definition doesn't allow to type first-class module since they don't type modulo substitution:

a.ml:
module type S = sig val x : int end
module type T = sig val x : int end
let f x = (module (struct let x = x end) : T)

a.mli:
module type S = sig val x : int end
val f : int -> (module S)

Error: The implementation test.ml does not match the interface test.cmi:
Values do not match:
val f : int -> (module T)
is not included in
val f : int -> (module S)
File "test.ml", line 6, characters 4-5: Actual declaration

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

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.

@vicuna
Copy link
Author

vicuna commented Oct 29, 2014

Comment author: @yakobowski

Another possibility would be to use a new toplevel declaration :
"module type S : inherit sig" (or something similar), which would be more explicit.

@vicuna
Copy link
Author

vicuna commented Oct 30, 2014

Comment author: @garrigue

I agree with Leo: breaking the transitivity of module subtyping looks like a no-no from a theoretical point of view.
Handling aliases in a special way may avoid the theoretical problem, but it could be rather confusing : the interface could bear little relation to the module...
Note that module types and class types can be seen as aliases too (they are both purely structural), so the difference with 6356 is very small.
(For the record, bobot's example with first-class modules does type in trunk.)

@vicuna
Copy link
Author

vicuna commented Sep 5, 2018

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.

@github-actions
Copy link

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.

@github-actions github-actions bot added the Stale label May 11, 2020
@ocaml ocaml deleted a comment from vicuna May 11, 2020
@garrigue
Copy link
Contributor

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 with module type T = ... and `with module type T := ...P).

@garrigue
Copy link
Contributor

Remaining part subsumed by #6356.

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