Content-Type: text/plain; charset=iso-8859-1
Content-Description: message body text
Content-Transfer-Encoding: 8bit



Dave Berry a écrit :
> 
> Do you have a real-life example where you need module equality of the
> sort you suggest?

I recognize the choice of an intentional notion of module equality was
not driven by immediate practical considerations. However, if you have
a look at Xavier's modular module system, it is used several times. Of
course, you can do without it (and in the background, Caml does without).

When I tried to define a module calculus for Pure Type Systems with
good metatheroetical properties, it happens that I needed module
equality: if you are familiar with O'Caml typing system for modules,
you probably know that it has a rule telling

E |- m : M
------------
E |- m : M/m

where "M/m" is M strengthened by m. Roughly this rule says if X is a
module defining an abstract type t then we at least know that this
type t is equal to X.T (the result of strengthening sig type t end by
X is sig type t = X.t end).

Now, a metatheoretical result you want is that if m has type M and M
is a correct module type then M/m is a correct module type.  It turns
out that if you want this property in presence of dependent types, you
need a notion of equality over modules that ensures that if X=Y then
F(X).t = F(Y).t (although this seems to be a truism, it is false in
O'Caml with the current definition of module equality). The
extentionnal definition is IMHO the wrong one since this lead to
accept that F(X).t = F(Y).t when F is Map.Make with

X = struct type t = int let compare x y = x-y end
and
Y = struct type t = int let compare x y = y-x end

as I said in my previous post. So I was left with the intentionnal
one. module equality is therefore part of the semantic of modules in
MC, so you have it for free. I did not try to add it to the modular
module system of Xavier until friday, when I began to write this
reply.

In a few hours, I could patch Xavier's code so that it accepts module
equality constraints (about 6h of total work time, including writing
this message and a very basic web page). I enclose the patch below,
you can download the fully modified code at
http://www.lri.fr/~jcourant/01/03/modular_modules

Here is an example that can be checked by miniML (look at the
signature of W)
----------------------------------------------------------------------
struct

module IntOrder =
 struct
   type t = int
   val equal x y = x == y
   val less x y = x < y
 end

module IntOrder' =
  struct
    type t = int
    val equal x y = x == y
    val less x y = x > y
  end

module Z =
 struct
  module X = IntOrder

  module Y = IntOrder
 end

module F =
  functor(W:sig
             module X : sig type t = int end
             module Y : sig type t = int end = X
	    end
	)
   struct
   end

module G = F(Z)

end
----------------------------------------------------------------------

The previous example typechecks but if you replace "module Y = IntOrder" by
"module Y = IntOrder'", it does not typechecks as X and Y are now
different.

If you have a look at the code, you will notice that any module
defined as "module X = m" is transparent as long as "m" is a path. It
is difficult to make more module transparent unless you extend the
definition of a path. However, you might wish some definition "module
X = p" (where p is a path) be opaque. It would be quite easy to change
the code so that the standard module definition is opaque and
introduce a "transparent module" definition.


Sincerly yours,

Judicaël.