From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA03471 for caml-red; Thu, 27 Jul 2000 19:35:38 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id MAA20155 for ; Wed, 26 Jul 2000 12:16:52 +0200 (MET DST) Received: from jurancon.inria.fr (jurancon.inria.fr [128.93.8.74]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e6QAGiD09278; Wed, 26 Jul 2000 12:16:44 +0200 (MET DST) Received: (from delahaye@localhost) by jurancon.inria.fr (8.7.6/8.7.3) id MAA12019; Wed, 26 Jul 2000 12:16:44 +0200 (MET DST) From: David Delahaye Message-Id: <200007261016.MAA12019@jurancon.inria.fr> Subject: Re: automatic construction of mli files In-Reply-To: from Julian Assange at "Jul 24, 100 03:34:22 pm" To: proff@iq.org (Julian Assange) Date: Wed, 26 Jul 2000 12:16:44 +0200 (MET DST) Cc: caml-list@inria.fr X-Mailer: ELM [version 2.4ME+ PL28 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: weis@pauillac.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 : David.Delahaye@inria.fr : The Coq Project : Proofs : INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex FRANCE : (33)-(0)1 39 63 57 53 : (33)-(0)1 39 63 56 84 : 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.]