Re: automatic construction of mli files

[David Delahaye <delahaye@jurancon.inria.fr>]

> .mli files are highly redundant. Almost without exception all, or at
> the vast majority of .mli information can be generated from the
> underlying .ml implementation. We have programming languages to reduce
> redundancy, not increase it. Keeping mli and ml files in-sync is not
> only a waste of time, but error-prone and from my survey often not
> performed correctly, particularly where consistency is not enforced by
> the compiler (e.g comments describing functions and types). While
> exactly the same problem exists in a number of other
> separate-compilation language implementations, we, as camlers, should
> strive for something better.

    I don't think that .mli are redundant. They essentially contain type
information and, in a strongly typed system, it is quite relevant and
especially useful. Moreover, with .mli, you can build abstract data types,
which are, in general, greatly used. So, to keep .mli and .ml files in-sync is
not a waste of time but a way to ensure that your .ml file is an implementation
of your specification. If you have errors during this verification then it
could be explained by (semantical) errors in your code, you wouldn't have seen
without this check. Of course, it could also be due to the .mli file which must
be changed but, again, it is not a waste of time and it should be have been
done before changing the implementation. Personally, I don't like .ml files
without .mli because you don't have any type information and even if I want to
export everything in an .ml file, I generate the .mli automatically.

    Regards.

    David.

===============================================================================
David Delahaye                                 <Email>: David.Delahaye@inria.fr
<Laboratory>: The Coq Project                                  <Domain>: Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[If you have time to waste, you can have a look on my proof that 2 = 1. We know
 that, for -1 < x <= 1:

   ln(1 + x) = x - 1/2(x^2) + 1/3(x^3) - 1/4(x^4) + ...

 Let x = 1:

   ln(2) = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + 1/7 - 1/8 + 1/9 - ...

 Let multiply the two members by 2:

   2ln(2) = 2 - 2/2 + 2/3 - 2/4 + 2/5 - 2/6 + 2/7 - 2/8 + 2/9 - ...
   2ln(2) = 2 - 1 + 2/3 - 1/2 + 2/5 - 1/3 + 2/7 - 1/4 + 2/9 - ...

 Let sum the terms with the same denominator:

   2ln(2) = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + 1/7 - ...
   2ln(2) = ln(2)

 Finally, 2 = 1.]