Re: [Caml-list] Why should I use .mli files?

[Gabriel Scherer <gabriel.scherer@gmail.com>]

Independently of this discussion, I have been discussed related issues
with a friend for the last two weeks. I think there would be a feature
proposal to make in this area that would be *relatively* natural and
help solve the following different problems in this area:
1. Repeating types, module types and class types declarations in the
.mli and the .ml is redundant and increases the maintenance burden
2. The semantics of type-checking the .ml as a whole, and then
checking that it matches the .mli signature is sometimes inconvenient:
checking values against their .mli counterpart could help detect
typing mistakes sooner, which is helpful to get error messages that
are easier to understand
3. Some users want to have annotations on values (at least at
toplevel) for readability and the expression language is not optimal
for this (in particular the fact that type variables do not enforce
polymorphism)

## Proposal

My suggestion would be to allow two features (the second depending on
the first):
1. allow to insert signature items anywhere in a module structure or
.ml file, giving a reasonable semantics to it
    (in particular allow inclusion of signature as a structure item,
with the derived semantics)
2. have a syntax to designate the mli signature from the ml file
(possible suggestion: "module type", used a signature expression)

By combining the two features you could have something like

a.mli
  type t = A | B of u
  type u
  val f : 'a -> 'a

a.ml
  include (module type with type u = int)
  let f x = x

But you could also write only a.ml:
  type t = A | B of u
  type u = int
  val f : 'a -> 'a
  let f x = x

## Corner cases and rejected extensions

Regarding feature 1., there is indeed something to be decided about
shadowing of values:
  val x : int
  let x = 0.
  let x = int_of_float x
or:
  val x : float
  let x = 0.
  val x : int
  let x = 0

My suggestion would be, as a conservative measure, to reject all
shadowing of an identifier that has been prototype with "val" -- as
Edgar suggested. This can always be extended with time (eg. to accept
the second example).

It is also natural, in particular if you come from the world of C
prototypes and predeclared types, to wish to accept something like
  type u
  type u = int (* refining semantics *)
I think we should reject those because they have a muddier semantic
(you could define what the least abstract "unifier" of two definitions
would be, but let's net get down that road). The "S with type u = ..."
(in particular when S is "module type") allows to refine type in a
principle way without shadowing/redeclaration.

Finally, the presence of these "val f : ..." ahead of the actual
definition made me think of the well-known regret that OCaml
compilation units are not very good at top-down programming: you have
to define everything before use which enforces a bottom-up style which
is sometimes not how you would like your code to be read. C prototypes
allow top-down programming, but picking a right semantics without
implicit mutual recursion is tricky. My feature idea willingly rejects
this ambitious direction to stay simple and true. I would still be
interested in thinking about this in the future.


## Known issues and competing proposals

The main problem with this proposal is that the presence of the
"module type" construction can only be explained in terms of the
"superficial" semantics of OCaml compilation units, rather than as a
"pure" feature of a typed lambda calculus. More precisely, I see no
way to explain this semantics but saying "we include the signature of
the .mli", which is admittedly an presentation detail of the OCaml
compiler rather than a deep aspect of the OCaml language.

"module type" could be explained in terms of the module sublanguage:
module M : sig
   type t = int
end = struct
    include (module type)
    let x : t = 1
end

But as you see the context-dependent semantics is not very nice and it
feels ad-hoc -- it is. I think this is the most serious problem with
the proposal and the reason why I'm unsure it could ever be accepted
by the language designers.

Another criticism is that most of the benefits of this proposal can
already be obtained with existing features:
1. one can define the relevant signatures in a "interfaces.ml" files
reused in both the current .ml and the .mli, to avoid duplication
2. there is a rich annotation¹ language for OCaml expressions patterns
or modules that can express what would be independently expressed as a
signature item

¹: while we're at it, I'm considering pushing for the syntax "fun pat
pat ... pat : ty -> expr" as a synonym for "fun pat pat ... pat ->
(expr : ty)", but the potential confusion between "fun x : int ->" and
"fun (x : int) ->" is disheartening.

There is another related proposal: Alain Frisch's suggestion to make
compilation units *recursive* modules implicitly, rather than
non-recursive modules.
  http://caml.inria.fr/mantis/print_bug_page.php?bug_id=5480
Using recursive modules induces a definitive amount of complexity, but
is also more expressive in terms of allowing forward references (the
top-to-bottom style aspect I mentioned earlier). I think a simpler,
non-recursive proposition is a more reasonable choice. Alain described
a compromise in use at Lexifi, where compilation units are
*type-checked* are recursive modules but *compiled* as non-recursive
modules. That's probably close in expressivity to this proposal (but
harder, I think, to explain to the newcomer).

On another level, the signature module of OCaml is not arbitrarily
expressive, and there are some things that cannot be presently handled
by signature manipulations and inclusion alone. For example, you
cannot easily hide/remove values or types from a signature
(destructive substitution "with t := ..." partly does that for type).
Heavy use of the proposed feature could run into these limitations. I
think we should be ready to enrich the signature language in this
case.


On Tue, Oct 30, 2012 at 5:46 PM, Edgar Friendly <thelema314@gmail.com> wrote:
> On 10/30/2012 12:21 PM, Romain Bardou wrote:
>>
>> Le 30/10/2012 17:06, Edgar Friendly a écrit :
>>>
>>> On 10/30/2012 10:47 AM, Romain Bardou wrote:
>>>>
>>>> Maybe ocaml should provide something like:
>>>>
>>>> include type t in sig
>>>>
>>> Is there any case where type declarations in the .mli file should not be
>>> included as part of the .ml file?
>>
>>
>> No, as it does not compile otherwise. However, maybe the user wants the
>> declarations to be put in some specific order.
>>
>>>> Which would mean "copy-paste the definition of t from the .mli".
>>>>
>>> Why not have this be the default? i.e. when compiling a .ml file, if the
>>> corresponding .mli file exists, its type declarations are in scope for
>>> the .ml file, and its value declarations are applied to the
>>> corresponding values in the .ml file. The only edge case I can think of
>>> is when an identifier is bound multiple times in the .ml file, the type
>>> from the .mli file currently only applies to the last binding, whereas
>>> with this strategy, the type would most easily be implemented as
>>> applying to all bindings of that identifier.
>>>
>>> E.
>>>
>>
>> I'm not sure I understand what you mean, but here are some examples I
>> worry about.
>>
>> 1) You have the following .mli:
>>         type t = A
>>         type u = A
>> with the following implementation:
>>         let x = A
>> Where should type t and type u be copied? In other words, should x be of
>> type t or of type u?
>>
> They could be copied to the top of the .ml file in the order specified in
> .mli file.
>
>> It may also happen that the user wants the order of t and u to be reversed
>> in the implementation.
>>
>> 2) You have a declaration like this in the .mli:
>>         type t = private something
>> Should it be copied as:
>>         type t = something
>> or as:
>>         type t = private something
>> I don't think the latter makes much sense most of the time, but it is a
>> valid declaration.
>>
> Or the user could specify "type t = something" in the .ml file and override
> the .mli file's type.  To do this, we'd need the concept of these "copied"
> types being overrideable in the .ml file, but I think doing this would be
> necessary for backwards compatibility, as all existing code would break
> under the new .mli semantics.
>
> E.
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs