|Anonymous | Login | Signup for a new account||2018-09-25 01:11 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006637||OCaml||typing||public||2014-10-29 14:09||2018-09-08 02:59|
|Target Version||Fixed in Version|
|Summary||0006637: Type alias or module type alias should not be taken into account for signature inclusion|
|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 =
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
|Tags||No tags attached.|
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
See also 0006356.
Why do you restrict the proposal to type aliases, and not arbitrary type definitions?
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.
((struct type t = int end : sig end) : sig type t = float end)
(struct type t = int end : sig type t = float end)
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"
|The idea in 0006356 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.|
edited on: 2014-10-29 16:56
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:
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)
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
|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.|
Boris Yakobowski (reporter)
Another possibility would be to use a new toplevel declaration :
"module type S : inherit sig" (or something similar), which would be more explicit.
edited on: 2014-10-31 02:34
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.)
|The PR https://github.com/ocaml/ocaml/pull/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.|
I am an agent of one of the products of PT NASA that is domiciled in Indonesia and ready to send products in various countries thanks
More info - http://www.agenherbalnasa.com/ [^]
|2014-10-29 14:09||bobot||New Issue|
|2014-10-29 14:17||bobot||Note Added: 0012457|
|2014-10-29 15:02||frisch||Note Added: 0012458|
|2014-10-29 15:02||frisch||Relationship added||duplicate of 0006356|
|2014-10-29 15:40||lpw25||Note Added: 0012459|
|2014-10-29 16:09||bobot||Note Added: 0012460|
|2014-10-29 16:23||frisch||Note Added: 0012461|
|2014-10-29 16:29||bobot||Note Added: 0012462|
|2014-10-29 16:56||bobot||Note Edited: 0012462||View Revisions|
|2014-10-29 17:30||bobot||Note Added: 0012464|
|2014-10-29 17:31||Boris Yakobowski||Note Added: 0012465|
|2014-10-30 02:52||garrigue||Note Added: 0012470|
|2014-10-31 02:34||garrigue||Note Edited: 0012470||View Revisions|
|2014-11-17 23:46||doligez||Status||new => acknowledged|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|2018-09-05 10:48||bobot||Note Added: 0019341|
|2018-09-08 02:59||user11163||Note Added: 0019344|
|Copyright © 2000 - 2011 MantisBT Group|