Re: [Caml-list] Caml 3.01 : pb with include

[Judicael Courant <Judicael.Courant@lri.fr>]

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