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 RAA26671; Wed, 21 Mar 2001 17:19:51 +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 RAA26563 for ; Wed, 21 Mar 2001 17:19:50 +0100 (MET) Received: from ext.lri.fr (ext.lri.fr [129.175.15.4]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f2LGJnL17994; Wed, 21 Mar 2001 17:19:49 +0100 (MET) Received: from pc87.lri.fr (IDENT:root@pc87 [129.175.8.106]) by ext.lri.fr (8.11.1/jtpda-5.3.2) with ESMTP id f2LGFvu16148 ; Wed, 21 Mar 2001 17:15:58 +0100 (MET) Received: from lri.fr (IDENT:jcourant@localhost.localdomain [127.0.0.1]) by pc87.lri.fr (8.9.3/jtpda-5.3.2) with ESMTP id RAA15567 ; Wed, 21 Mar 2001 17:15:56 +0100 Message-ID: <3AB8D3BC.7C386F88@lri.fr> Date: Wed, 21 Mar 2001 17:15:56 +0100 From: Judicael Courant X-Mailer: Mozilla 4.72 [fr] (X11; U; Linux 2.2.14-5.0 i686) X-Accept-Language: en MIME-Version: 1.0 To: caml-list@inria.fr CC: Dave Berry , Xavier Leroy , Andreas Rossberg , Christophe Raffalli Subject: Re: [Caml-list] Caml 3.01 : pb with include References: Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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 = struct type t = int let compare x y = x-y end module Y = struct type t = int let compare x y = 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 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 = 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ël. -- 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é ŕ mort. http://rozenn.picard.free.fr/tim.html ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr