This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

RE: [Caml-list] Caml 3.01 : pb with include
• Dave Berry
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2001-03-23 (12:03) From: Dave Berry Subject: RE: [Caml-list] Caml 3.01 : pb with include
```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 = 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

```