Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006637OCamltypingpublic2014-10-29 14:092018-09-08 02:59
Reporterbobot 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusacknowledgedResolutionopen 
PlatformallOSallOS Versionall
Product Version4.02.1 
Target VersionFixed in Version 
Summary0006637: Type alias or module type alias should not be taken into account for signature inclusion
DescriptionOften 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
```


TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0006356feedback Allowing extra 'type' fields in signature inclusion check 

-  Notes
(0012457)
bobot (reporter)
2014-10-29 14:17

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
(0012458)
frisch (developer)
2014-10-29 15:02

See also 0006356.

Why do you restrict the proposal to type aliases, and not arbitrary type definitions?
(0012459)
lpw25 (developer)
2014-10-29 15:40

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.
(0012460)
bobot (reporter)
2014-10-29 16:09

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"
(0012461)
frisch (developer)
2014-10-29 16:23

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.
(0012462)
bobot (reporter)
2014-10-29 16:29
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:

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

(0012464)
bobot (reporter)
2014-10-29 17:30

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.
(0012465)
Boris Yakobowski (reporter)
2014-10-29 17:31

Another possibility would be to use a new toplevel declaration :
"module type S : inherit sig" (or something similar), which would be more explicit.
(0012470)
garrigue (manager)
2014-10-30 02:52
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.)

(0019341)
bobot (reporter)
2018-09-05 10:48

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.
(0019344)
user11163
2018-09-08 02:59

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/ [^]

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker