From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA09115; Fri, 23 Mar 2001 13:03:59 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 NAA08840 for ; Fri, 23 Mar 2001 13:03:57 +0100 (MET) Received: from mrwall.kal.com (mrwall.kal.com [194.193.14.236]) by concorde.inria.fr (8.11.1/8.10.0) with SMTP id f2NC3uX01717; Fri, 23 Mar 2001 13:03:56 +0100 (MET) Received: from mrwall.kal.com [194.193.14.236] (HELO localhost) by mrwall.kal.com (AltaVista Mail V2.0J/2.0J BL25J listener) id 0000_0045_3abb_3c26_165a; Fri, 23 Mar 2001 12:05:58 +0000 Subject: RE: [Caml-list] Caml 3.01 : pb with include MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Date: Fri, 23 Mar 2001 12:02:48 -0000 content-class: urn:content-classes:message X-MimeOLE: Produced By Microsoft Exchange V6.0.4417.0 Message-ID: Thread-Topic: [Caml-list] Caml 3.01 : pb with include Thread-Index: AcCyIquraKj5If3gQ+Wx0VcFBzq3BABbUScg From: "Dave Berry" To: "Judicael Courant" , Cc: "Xavier Leroy" , "Andreas Rossberg" , "Christophe Raffalli" Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Do you have a real-life example where you need module equality of the sort you suggest? One of the reasons that SML'97 dropped this notion of module equality was that it wasn't used in practice. Also, you can simulate it if necessary by adding an abstract type to the module. Removing this in SML'97 hugely simplified the semantics of modules, and made them easier to implement. (I think MLWorks was the only SML compiler that implemented all the nooks and crannies of the SML'90 modules language, although I may be wrong about that. From an engineering point of view, that was a mis-use of resources, IMO). Clearly there is potential for a better way of specifying this equality, if you need it. I hope your calculus is a good step down that road. Dave. -----Original Message----- From: Judicael Courant [mailto:Judicael.Courant@lri.fr] Sent: Wednesday, March 21, 2001 16:16 To: caml-list@inria.fr Cc: Dave Berry; Xavier Leroy; Andreas Rossberg; Christophe Raffalli Subject: Re: [Caml-list] Caml 3.01 : pb with include Hi, I realized I missed an interesting discussion some time ago, so I am adding a small comment now. IMHO, the "with module" is a useful notion, but its current theoretical interpretation is the wrong one: for instance when I write module X =3D struct type t =3D int let compare x y =3D x-y end module Y =3D struct type t =3D int let compare x y =3D y-x end I would not like X and Y to be considered equal. The problem with this comes from the status of equality of type=20 expressions in a modular settings. The often cited paper of Harper, Mitchell and Moggi about the phase distinction has IMHO been misinterpreted as the fact that the equality should be extensionnal, that is F(X).t and F(Y).t should be equal as soon as the types defined in X and the types defined in Y are equal. The previous condition indeed ensures that at run time F(X).t and F(Y).t are equal but it is not restrictive enough: roughly, this is saying that equality over modules is extensionnal whereas what the developper need is an intentionnal equality (i.e. if I define two modules X and Y, my intention is that are different, even if they define the same types). Consider the previous example with F =3D Map.Make. You certainly do not want F(X).t and F(Y).t to be considered equal by the type-checker! And in fact, in O'Caml, they are incompatible as the comparison of types mixes intentionality and extentionality. That stamp-based generative semantics was also a way to ensure that F(X).t and F(Y).t are not considered equal by the type-checker. I proposed a module system (called MC for "module calculus") in my thesis in which equality is intentional. The semantics of module equality is precisely defined --- although the thesis itself has been said hard to read. BTW, Christophe Raffali's example seems to be correct in MC. The problem with MC is that, although useful on proof languages (in which you can strongly normalize expression), it is probably of little use on Turing-complete programming languages (as you can not decide the equality of arbitrary expressions). However, I plan to design another system, tailored for programming languages that would not have this limitation (maybe soon at a Cristal-LogiCal-Moscova seminar ?). Stay tuned... Judica=EBl. --=20 Judicael.Courant@lri.fr, http://www.lri.fr/~jcourant/ (+33) (0)1 69 15 64 85 "Montre moi des morceaux de ton monde, et je te montrerai le mien" Tim, matricule #929, condamn=E9 =E0 mort. http://rozenn.picard.free.fr/tim.html ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr