|Anonymous | Login | Signup for a new account||2015-01-28 23:15 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006356||OCaml||OCaml typing||public||2014-03-28 10:37||2014-10-30 02:42|
|Priority||low||Severity||feature||Reproducibility||have not tried|
|Target Version||Fixed in Version|
|Summary||0006356: Allowing extra 'type' fields in signature inclusion check|
|Description||It is slightly annoying having to maintain the same definition of a type (resp. class type / module type) in both the interface and the implementation of a module, especially when the definition is not required within the implementation itself.|
For instance, for a structure such as:
module type S = sig ... end module Make(X : S) = struct ... end
one might want to give a signature which gives a name to the result type:
module type S = sig ... end module type T = sig ... end module Make(X : S) : T with ...
But this doesn't work: one needs to copy the definition of T within the implementation.
What about extending the inclusion check to allow more type items in the supertype? I don't know if I really want to push for it, but I'm wondering if there is any deeper implication in allowing that. The patch would be rather trivial:
Index: typing/includemod.ml =================================================================== --- typing/includemod.ml (revision 14492) +++ typing/includemod.ml (working copy) @@ -297,6 +297,8 @@ (* Do not report in case of failure, as the main type will generate an error *) Field_type (String.sub s 0 (String.length s - 4)), false + | (Sig_type _ | Sig_modtype _ | Sig_class_type _), name2 -> + name2, false | _ -> name2, true in begin try
|Tags||No tags attached.|
FWIW, this change enables two cases currently failing in testsuite/tests/typing-module/firstclass.ml:
module type S = sig type u type t end;; module type S' = sig type t = int type u = bool end;; module type S2 = sig type u type t type w end;; let f2 (x : (module S2 with type t = 'a and type u = 'b)) = (x : (module S'));; (* no longer fails *) let k (x : (module S2 with type t = 'a)) = (x : (module S with type t = 'a));; (* no longer fails *)
I would be very careful with this kind of change, because basically you enter uncharted territory.
Some properties, like the substitution property for modules, would not work anymore
(it already doesn't work stricto sensu due to open and include, but we go to another level).
A proof of soundness would be a first step :-)
By the way, the implementation could not be that simple.
I tried your patch, and the following program fails:
module M : sig module type T = sig val x : int end module F() : T end =
struct module F() = struct let x = 3 end end;;
The reason is that, when comparing component types, we work in the environment of the internal module, which does not contain any definition for T.
At least one would need to add such definitions to the environment; clearly we would need a semantics first.
|2014-03-28 10:37||frisch||New Issue|
|2014-04-02 23:09||frisch||Note Added: 0011186|
|2014-04-04 04:49||garrigue||Note Added: 0011216|
|2014-07-16 15:49||doligez||Status||new => feedback|
|2014-10-29 15:02||frisch||Relationship added||has duplicate 0006637|
|2014-10-30 02:42||garrigue||Note Added: 0012469|
|Copyright © 2000 - 2011 MantisBT Group|