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

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

> If I missed your pointm then you need to explain in more depth, what you mean.

My point of view is that you write .mli files, but then you don't want
to repeat in the .ml the concrete type definitions that have been
written in the .mli already. One problem with writing those concrete
(non-abstract) type definitions (and exceptions, class types and
module types) is that you have two places to edit instead of one when
you make a change, which 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

The current semantics is nice from a conceptual point of view (you
just need to explain how a .ml/.mli pair are understood as a module
with its interface, and then let the usual type-checking rule do the
work), but sometimes you would wish to have values type-checked
against their specification directly, rather than after the whole
module is type-checked. If the value has an unexpected type (compared
to the .mli signature), being warned at the value declaration site is
often better than at a (possibly remote) use site in the rest of the
module. The proposed semantics for having signature items in
structures allows to do this: every "let foo = ..." that comes after a
"val foo : bar" is type-checked under the expected type "bar".

>> 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)

The following code is valid:
  let f : 'a -> 'a = fun x -> x + 1

Beginners are often surprised by this. The language of type
annotations of OCaml is not simple, with three different ways to
enforce polymorphism, none of them obvious to the beginner. Value
signatures have a simple and non-surprising semantics that would
reject the following
  val f : 'a -> 'a
  let f x = x + 1

> I just suspect, that something important has been forgotten...

It's my turn to not understand what you say.

> If you don't use mli files, then the exported signiture
> is available and is like what you find inside the ml-file.
> So what is new here?

Allowing signatures items in structures and .ml files alone does not
increase the expressivity of the language. It is just a different way
to annotate names with expected types, that has the advantage of being
simple and predictable, and coincide with a syntax that users
sometimes wish they could use.
The new aspect of the proposal is the way it can be combined with the
(more debatable in itself) "module type" feature to avoid repeating
type definitions in the .ml. I believe the combination of these two
features is conceptually simpler than other approaches to this problem
(but not the recursive proposal of Alain which is very simple), and
has desirable other effects regarding the principled use of
annotations as signatures.

That said, I'm not clung to this proposal. I have been thinking about
it infrequently for a few weeks, and I'm still not satisfied with the
rather ad-hoc semantics of the "module type" feature. I was exposing
it as a contribution to the discussion, but I don't expect it to turn
into a submitted type-system patch right away.

On Tue, Oct 30, 2012 at 11:18 PM, Oliver Bandel
<oliver@first.in-berlin.de> wrote:
>
>
> Am 30.10.2012 um 22:25 schrieb 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
>
>
> Hmhh, not sure if Innserstand whatbyou mean.
> But as a mli-file narrows the default signature,
> repeating types mustbe done.
> An empty mli-file would create an empty signature,
> and IMHO thats good.
> Otherwise it would be necessary to have another mechanism to
> narrow the automatic copying of types.
>
> If I missed your pointm then you need to explain in more depth, what you mean.
>
>
>
>> 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
>
> What is your argument? pro or contra?
> It looks weird to me.
>
>
>> 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)
>
>
> This is something that possibly would create a big mess,
> and also seems to mix up interface and implementation
> for the module language.
> At least thats my fear. Mybe if its well done, it would work.
>
> I just suspect, that something important has been forgotten...
>
>
>
>
>
>
>> 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
>
> ??
>
>
> If you don't use mli files, then the exported signiture
> is available and is like what you find inside the ml-file.
> So what is new here?
>
> I,may missed the point, but you can omit mli-files today also....
>
> Ciao,
>    Oliver
>