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

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

[Dave Berry]

I can add a little background to Xavier's remark about SML'97.  One of
the main changes in SML'97 from SML'90 was the removal of the
"stamp-based" notion of structure sharing (where two structures were
shared only if they were exactly the same structure).  In an early draft
this change went so far as to remove the structure sharing syntax
entirely.  

After some discussion, the syntax was retained, and interpreted purely
as a shorthand for sharing all the (flexible) types in the structures.
This was partly for backwards compatibility, which is why the SML'97
standard didn't add a "where structure" form analogous to "where type".
(SML/NJ allows this as an extension to the language, and I think other
implementations may have picked this up).

I find the structure sharing syntax genuinely useful.  As an example, if
you have a module containing all the (recursive) datatypes of an
abstract syntax, and you use this file in many other modules, it's
useful to specify that the types are shared using a single line instead
of having to add a sharing constraint for each type.  The risk of
keeping the syntax is that people might interpret it in a way that is
subtly different from what is intended -- witness the confusion in this
case.  But I think the gain outweighs the cost, provided that the
intended definition is clearly explained.

Dave.

-----Original Message-----
From: Xavier Leroy [mailto:Xavier.Leroy@inria.fr]
Sent: Tuesday, March 13, 2001 10:32
To: Andreas Rossberg
Cc: caml-list@inria.fr; Christophe Raffalli
Subject: Re: [Caml-list] Caml 3.01 : pb with include

I agree with you that the most natural interpretation of the "with
module" constraint is to stand for a bunch of "with type" constraints
on the type components of the modules.  With this interpretation, the
current behavior is a bug.  SML'97 also interprets sharing constraints
between structures as the implied sharing constraints between the type
components of these modules.
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

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

[Judicael Courant]

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

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

[Dave Berry]

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

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

[Judicael Courant]

[-- Attachment #1: message body text --]
[-- Type: text/plain, Size: 3560 bytes --]

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.


[-- Attachment #2: Patch to Leroy's modular module system, adds module sharing --]
[-- Type: text/plain, Size: 22935 bytes --]

diff -c modular_modules.orig/miniC.ml modular_modules/miniC.ml
*** modular_modules.orig/miniC.ml	Fri Dec  3 14:35:22 1999
--- modular_modules/miniC.ml	Tue Mar 27 09:31:14 2001
***************
*** 78,84 ****
            List.for_all2 (valtype_match env) args1 args2 &&
            valtype_match env res1 res2
        | (Typename path1, Typename path2) ->
!           path_equal path1 path2 ||
            begin match (CEnv.find_type path1 env,
                         CEnv.find_type path2 env) with
              ({manifest = Some def}, _) -> valtype_match env def ty2
--- 78,84 ----
            List.for_all2 (valtype_match env) args1 args2 &&
            valtype_match env res1 res2
        | (Typename path1, Typename path2) ->
!           Env.path_equal env path1 path2 ||
            begin match (CEnv.find_type path1 env,
                         CEnv.find_type path2 env) with
              ({manifest = Some def}, _) -> valtype_match env def ty2
***************
*** 351,360 ****
            print_string "typedef "; print_name_type id ty
        | Type_sig(id, {manifest = None}) ->
            print_string "typedef "; print_string(Ident.name id)
!       | Module_sig(id, mty) ->
            open_hvbox 2;
            print_string "module "; print_string(Ident.name id);
!           print_string ":"; print_space(); print_modtype mty;
            close_box()
    end
      
--- 351,368 ----
            print_string "typedef "; print_name_type id ty
        | Type_sig(id, {manifest = None}) ->
            print_string "typedef "; print_string(Ident.name id)
!       | Module_sig(id, mdecl) ->
            open_hvbox 2;
            print_string "module "; print_string(Ident.name id);
!           print_string ":"; print_space(); print_moddecl mdecl;
            close_box()
+     and print_moddecl mdecl =
+       open_hvbox 2;
+       print_modtype mdecl.CMod.ty;
+       (match mdecl.CMod.eq with
+ 	 | None -> ()
+ 	 | Some p -> print_space (); print_string "="; print_space();
+ 	     print_path p);
+       close_box()
    end
      
diff -c modular_modules.orig/miniCparser.mly modular_modules/miniCparser.mly
*** modular_modules.orig/miniCparser.mly	Fri Dec  3 16:34:11 1999
--- modular_modules/miniCparser.mly	Tue Mar 27 09:32:49 2001
***************
*** 240,247 ****
          CMod.Type_sig(id, {CMod.kind = (); CMod.manifest = Some ty}) }
    | TYPEDEF UIDENT SEMI
        { CMod.Type_sig(Ident.create $2, {CMod.kind = (); CMod.manifest = None}) }
!   | MODULE UIDENT COLON moduletype SEMI
        { CMod.Module_sig(Ident.create $2, $4) }
  ;
  
  /* Toplevel entry point */
--- 240,253 ----
          CMod.Type_sig(id, {CMod.kind = (); CMod.manifest = Some ty}) }
    | TYPEDEF UIDENT SEMI
        { CMod.Type_sig(Ident.create $2, {CMod.kind = (); CMod.manifest = None}) }
!   | MODULE UIDENT COLON moduledecl SEMI
        { CMod.Module_sig(Ident.create $2, $4) }
+ ;
+ 
+ 
+ moduledecl:
+     moduletype EQUAL upath { { CMod.ty = $1 ; CMod.eq = Some $3 } }
+   | moduletype            { { CMod.ty = $1 ; CMod.eq = None } }
  ;
  
  /* Toplevel entry point */
diff -c modular_modules.orig/miniML.ml modular_modules/miniML.ml
*** modular_modules.orig/miniML.ml	Fri Dec  3 14:34:45 1999
--- modular_modules/miniML.ml	Tue Mar 27 09:23:51 2001
***************
*** 86,92 ****
        let repr1 = typerepr ty1 and repr2 = typerepr ty2 in
        match (repr1, repr2) with
          (Typeconstr(path1, args1), Typeconstr(path2, args2)) ->
!           if path_equal path1 path2 then
              (repr1, repr2)
            else begin
              try
--- 86,92 ----
        let repr1 = typerepr ty1 and repr2 = typerepr ty2 in
        match (repr1, repr2) with
          (Typeconstr(path1, args1), Typeconstr(path2, args2)) ->
!           if Env.path_equal env path1 path2 then
              (repr1, repr2)
            else begin
              try
***************
*** 394,402 ****
            open_hvbox 2;
            print_string "type "; print_typedecl id decl;
            close_box()
!       | Module_sig(id, mty) ->
            open_hvbox 2;
            print_string "module "; print_string(Ident.name id);
!           print_string ":"; print_space(); print_modtype mty;
            close_box()
    end
--- 394,410 ----
            open_hvbox 2;
            print_string "type "; print_typedecl id decl;
            close_box()
!       | Module_sig(id, mdecl) ->
            open_hvbox 2;
            print_string "module "; print_string(Ident.name id);
!           print_string ":"; print_space(); print_moddecl mdecl;
            close_box()
+     and print_moddecl mdecl =
+       open_hvbox 2;
+       print_modtype mdecl.MLMod.ty;
+       (match mdecl.MLMod.eq with
+ 	 | None -> ()
+ 	 | Some p -> print_space (); print_string "="; print_space();
+ 	     print_path p);
+       close_box()
    end
diff -c modular_modules.orig/miniMLparser.mly modular_modules/miniMLparser.mly
*** modular_modules.orig/miniMLparser.mly	Fri Dec  3 12:03:55 1999
--- modular_modules/miniMLparser.mly	Tue Mar 27 09:33:03 2001
***************
*** 217,223 ****
  signature_item:
      VALUE IDENT valuedecl             { MLMod.Value_sig(Ident.create $2, $3) }
    | TYPE typeinfo    { let (id, def) = $2 in MLMod.Type_sig(Ident.create id, def) }
!   | MODULE IDENT COLON moduletype     { MLMod.Module_sig(Ident.create $2, $4) }
  ;
  
  /* Toplevel entry point */
--- 217,228 ----
  signature_item:
      VALUE IDENT valuedecl             { MLMod.Value_sig(Ident.create $2, $3) }
    | TYPE typeinfo    { let (id, def) = $2 in MLMod.Type_sig(Ident.create id, def) }
!   | MODULE IDENT COLON moduledecl     { MLMod.Module_sig(Ident.create $2, $4) }
! ;
! 
! moduledecl:
!     moduletype EQUAL path { { MLMod.ty = $1 ; MLMod.eq = Some $3 } }
!   | moduletype            { { MLMod.ty = $1 ; MLMod.eq = None } }
  ;
  
  /* Toplevel entry point */
Only in modular_modules: modeq.miniML
diff -c modular_modules.orig/modules.ml modular_modules/modules.ml
*** modular_modules.orig/modules.ml	Fri Dec  3 12:00:09 1999
--- modular_modules/modules.ml	Tue Mar 27 09:20:15 2001
***************
*** 44,56 ****
      Pident of Ident.t             (* identifier *)
    | Pdot of path * string         (* access to a module component *)
  
- let rec path_equal p1 p2 =
-   match (p1, p2) with
-     (Pident id1, Pident id2) -> Ident.equal id1 id2
-   | (Pdot(r1, field1), Pdot(r2, field2)) ->
-       path_equal r1 r2 && field1 = field2
-   | (_, _) -> false
- 
  (* Section 2.3: Substitutions *)
  
  module type SUBST =
--- 44,49 ----
***************
*** 101,107 ****
      and specification =
          Value_sig of Ident.t * Core.val_type      (* val x: ty *)
        | Type_sig of Ident.t * type_decl           (* type t :: k [= ty] *)
!       | Module_sig of Ident.t * mod_type          (* module X: mty *)
      type mod_term =
          Longident of path                         (* X or X.Y.Z *)
        | Structure of structure                    (* struct ... end *)
--- 94,101 ----
      and specification =
          Value_sig of Ident.t * Core.val_type      (* val x: ty *)
        | Type_sig of Ident.t * type_decl           (* type t :: k [= ty] *)
!       | Module_sig of Ident.t * mod_decl          (* module X: mty [=p]*)
!     and mod_decl = { ty : mod_type; eq : path option }
      type mod_term =
          Longident of path                         (* X or X.Y.Z *)
        | Structure of structure                    (* struct ... end *)
***************
*** 116,121 ****
--- 110,116 ----
                                                    (* type t :: k = ty *)
        | Module_str of Ident.t * mod_term          (* module X = mod *)
      val subst_typedecl: type_decl -> Subst.t -> type_decl
+     val subst_moddecl: mod_decl -> Subst.t -> mod_decl
      val subst_modtype: mod_type -> Subst.t -> mod_type
    end
  
***************
*** 134,140 ****
      and specification =
          Value_sig of Ident.t * Core.val_type      (* val x: ty *)
        | Type_sig of Ident.t * type_decl           (* type t :: k [= ty] *)
!       | Module_sig of Ident.t * mod_type          (* module X: mty *)
      type mod_term =
          Longident of path                         (* X or X.Y.Z *)
        | Structure of structure                    (* struct ... end *)
--- 129,136 ----
      and specification =
          Value_sig of Ident.t * Core.val_type      (* val x: ty *)
        | Type_sig of Ident.t * type_decl           (* type t :: k [= ty] *)
!       | Module_sig of Ident.t * mod_decl          (* module X: mty [ = p]*)
!     and mod_decl = { ty : mod_type; eq : path option }
      type mod_term =
          Longident of path                         (* X or X.Y.Z *)
        | Structure of structure                    (* struct ... end *)
***************
*** 162,168 ****
      and subst_sig_item sub = function
          Value_sig(id, vty) -> Value_sig(id, Core.subst_valtype vty sub)
        | Type_sig(id, decl) -> Type_sig(id, subst_typedecl decl sub)
!       | Module_sig(id, mty) -> Module_sig(id, subst_modtype mty sub)
    end
  
  (* Section 2.6: The environment structure *)
--- 158,169 ----
      and subst_sig_item sub = function
          Value_sig(id, vty) -> Value_sig(id, Core.subst_valtype vty sub)
        | Type_sig(id, decl) -> Type_sig(id, subst_typedecl decl sub)
!       | Module_sig(id, mdecl) -> Module_sig(id, subst_moddecl mdecl sub)
!     and subst_moddecl mdecl sub = 
!       { ty = subst_modtype mdecl.ty sub;
!         eq = match mdecl.eq with
! 	  | None -> None
! 	  | Some p -> Some(Subst.path p sub) }
    end
  
  (* Section 2.6: The environment structure *)
***************
*** 172,185 ****
      module Mod: MOD_SYNTAX
      type t
      val empty: t
      val add_value: Ident.t -> Mod.Core.val_type -> t -> t
      val add_type: Ident.t -> Mod.type_decl -> t -> t    
!     val add_module: Ident.t -> Mod.mod_type -> t -> t    
      val add_spec: Mod.specification -> t -> t
      val add_signature: Mod.signature -> t -> t
      val find_value: path -> t -> Mod.Core.val_type
      val find_type: path -> t -> Mod.type_decl
      val find_module: path -> t -> Mod.mod_type
    end
  
  module Env(Mod_syntax: MOD_SYNTAX) =
--- 173,189 ----
      module Mod: MOD_SYNTAX
      type t
      val empty: t
+     val path_equal : t -> path -> path -> bool
      val add_value: Ident.t -> Mod.Core.val_type -> t -> t
      val add_type: Ident.t -> Mod.type_decl -> t -> t    
!     val add_module: Ident.t -> Mod.mod_decl -> t -> t    
!     val add_absmodule: Ident.t -> Mod.mod_type -> t -> t    
      val add_spec: Mod.specification -> t -> t
      val add_signature: Mod.signature -> t -> t
      val find_value: path -> t -> Mod.Core.val_type
      val find_type: path -> t -> Mod.type_decl
      val find_module: path -> t -> Mod.mod_type
+ (*    val find_module_type: path -> t -> Mod.mod_type *)
    end
  
  module Env(Mod_syntax: MOD_SYNTAX) =
***************
*** 188,204 ****
      type binding =
          Value of Mod.Core.val_type
        | Type of Mod.type_decl
!       | Module of Mod.mod_type
      type t = binding Ident.tbl
      let empty = Ident.emptytbl
      let add_value id vty env = Ident.add id (Value vty) env
      let add_type id decl env = Ident.add id (Type decl) env
!     let add_module id mty env = Ident.add id (Module mty) env
      let add_spec item env =
        match item with
          Mod.Value_sig(id, vty) -> add_value id vty env
        | Mod.Type_sig(id, decl) -> add_type id decl env
!       | Mod.Module_sig(id, mty) -> add_module id mty env
      let add_signature = List.fold_right add_spec
      let rec find path env =
        match path with
--- 192,210 ----
      type binding =
          Value of Mod.Core.val_type
        | Type of Mod.type_decl
!       | Module of Mod.mod_decl
      type t = binding Ident.tbl
      let empty = Ident.emptytbl
      let add_value id vty env = Ident.add id (Value vty) env
      let add_type id decl env = Ident.add id (Type decl) env
!     let add_module id mdecl env = Ident.add id (Module mdecl) env
!     let add_absmodule id mty env =
!       Ident.add id (Module { Mod.ty = mty; Mod.eq = None }) env
      let add_spec item env =
        match item with
          Mod.Value_sig(id, vty) -> add_value id vty env
        | Mod.Type_sig(id, decl) -> add_type id decl env
!       | Mod.Module_sig(id, mdecl) ->  add_module id mdecl env
      let add_signature = List.fold_right add_spec
      let rec find path env =
        match path with
***************
*** 219,227 ****
            then Type(Mod.subst_typedecl decl subst)
            else find_field p field
                   (Subst.add id (Pdot(p, Ident.name id)) subst) rem
!       | Mod.Module_sig(id, mty) :: rem ->
            if Ident.name id = field
!           then Module(Mod.subst_modtype mty subst)
            else find_field p field
                   (Subst.add id (Pdot(p, Ident.name id)) subst) rem
      and find_value path env =
--- 225,233 ----
            then Type(Mod.subst_typedecl decl subst)
            else find_field p field
                   (Subst.add id (Pdot(p, Ident.name id)) subst) rem
!       | Mod.Module_sig(id, mdecl) :: rem ->
            if Ident.name id = field
!           then Module(Mod.subst_moddecl mdecl subst)
            else find_field p field
                   (Subst.add id (Pdot(p, Ident.name id)) subst) rem
      and find_value path env =
***************
*** 232,238 ****
          Type decl -> decl | _ -> error "type field expected"   
      and find_module path env =
        match find path env with
!         Module mty -> mty | _ -> error "module field expected"   
    end
  
  (* Section 2.7: Type-checking the base language *)
--- 238,277 ----
          Type decl -> decl | _ -> error "type field expected"   
      and find_module path env =
        match find path env with
!         Module mdecl -> mdecl.Mod.ty | _ -> error "module field expected"
! 
!     (* norm_path : -> path * signature option *)
!     let rec norm_path env path =
!       let norm_binding path b =
! 	match b with
! 	  | Module { Mod.eq = Some p } -> norm_path env p
! 	  | Module { Mod.ty = Mod.Signature sg } -> path, Some sg
! 	  | _ -> path, None
!       in
!       match path with
! 	| Pident id -> norm_binding path (Ident.find id env)
! 	| Pdot(root, field) ->
! 	    let p', sgopt = norm_path env root in
! 	    (match sgopt with
! 	      | None -> error "structure expected in dot access"
! 	      | Some sg ->
! 		  let b = find_field p' field Subst.identity sg in
! 		  norm_binding (Pdot(p', field)) b
! 	    )
!     
!     (* syntactic equality *)
!     let rec path_syn_equal p1 p2 =
!       match (p1, p2) with
! 	  (Pident id1, Pident id2) -> Ident.equal id1 id2
! 	| (Pdot(r1, field1), Pdot(r2, field2)) ->
! 	    path_syn_equal r1 r2 && field1 = field2
! 	| (_, _) -> false
! 
!     (* semantic equality *)	      
!     let path_equal env p1 p2 =
!       let p1', _ = norm_path env p1
!       and p2', _ = norm_path env p2 in
!       path_syn_equal p1' p2'
    end
  
  (* Section 2.7: Type-checking the base language *)
***************
*** 286,292 ****
            let subst = Subst.add param1 (Pident param2) Subst.identity in
            let res1' = Mod.subst_modtype res1 subst in
            modtype_match env arg2 arg1;
!           modtype_match (Env.add_module param2 arg2 env) res1' res2
        | (_, _) ->
            error "module type mismatch"
      and pair_signature_components sig1 sig2 =
--- 325,331 ----
            let subst = Subst.add param1 (Pident param2) Subst.identity in
            let res1' = Mod.subst_modtype res1 subst in
            modtype_match env arg2 arg1;
!           modtype_match (Env.add_absmodule param2 arg2 env) res1' res2
        | (_, _) ->
            error "module type mismatch"
      and pair_signature_components sig1 sig2 =
***************
*** 318,325 ****
            if not (typedecl_match env id decl1
                                   (Mod.subst_typedecl decl2 subst))
            then error "type components do not match"
!       | (Module_sig(_, mty1), Module_sig(_, mty2)) ->
!           modtype_match env mty1 (Mod.subst_modtype mty2 subst)
      and typedecl_match env id decl1 decl2 =
        CT.kind_match env decl1.kind decl2.kind &&
        (match (decl1.manifest, decl2.manifest) with
--- 357,375 ----
            if not (typedecl_match env id decl1
                                   (Mod.subst_typedecl decl2 subst))
            then error "type components do not match"
!       | (Module_sig(id, mdecl1), Module_sig(_, mdecl2)) ->
! 	  moddecl_match env id mdecl1 (Mod.subst_moddecl mdecl2 subst)
!     and moddecl_match env id mdecl1 mdecl2 =
!       let mty1, mty2 = mdecl1.Mod.ty, mdecl2.Mod.ty in
!       modtype_match env mty1 mty2;
!       match (mdecl1.Mod.eq, mdecl2.Mod.eq) with
! 	| (_, None) -> ()
! 	| Some p1, Some p2 ->
! 	    if not (Env.path_equal env p1 p2)
! 	    then error "module components do not match"
! 	| None, Some p ->
! 	    if not (Env.path_equal env (Pident id) p)
! 	    then error "module components do not match"
      and typedecl_match env id decl1 decl2 =
        CT.kind_match env decl1.kind decl2.kind &&
        (match (decl1.manifest, decl2.manifest) with
***************
*** 345,352 ****
                                   (Pdot(path, Ident.name id)) decl.kind)
              | Some ty -> Some ty in
            Type_sig(id, {kind = decl.kind; manifest = m})
!       | Module_sig(id, mty) ->
!           Module_sig(id, strengthen_modtype (Pdot(path, Ident.name id)) mty)
  
      (* Continuation of section 2.8: Type-checking the module language *)
  
--- 395,406 ----
                                   (Pdot(path, Ident.name id)) decl.kind)
              | Some ty -> Some ty in
            Type_sig(id, {kind = decl.kind; manifest = m})
!       | Module_sig(id, mdecl) ->
!           Module_sig(id, strengthen_moddecl (Pdot(path, Ident.name id)) mdecl)
!     and strengthen_moddecl path mdecl =
!       let mty = strengthen_modtype path mdecl.Mod.ty
!       and path' = match mdecl.Mod.eq with None -> path | Some p -> p
!       in { Mod.ty = mty ; Mod.eq = Some path' }
  
      (* Continuation of section 2.8: Type-checking the module language *)
  
***************
*** 354,360 ****
          Signature sg -> check_signature env [] sg
        | Functor_type(param, arg, res) ->
            check_modtype env arg;
!           check_modtype (Env.add_module param arg env) res
      and check_signature env seen = function
          [] -> ()
        | Value_sig(id, vty) :: rem ->
--- 408,414 ----
          Signature sg -> check_signature env [] sg
        | Functor_type(param, arg, res) ->
            check_modtype env arg;
!           check_modtype (Env.add_absmodule param arg env) res
      and check_signature env seen = function
          [] -> ()
        | Value_sig(id, vty) :: rem ->
***************
*** 375,386 ****
            end;
            check_signature (Env.add_type id decl env)
                            (Ident.name id :: seen) rem
!       | Module_sig(id, mty) :: rem ->
            if List.mem (Ident.name id) seen 
            then error "repeated module name";
!           check_modtype env mty;
!           check_signature (Env.add_module id mty env) 
                            (Ident.name id :: seen) rem
  
      let rec type_module env = function
          Longident path ->
--- 429,448 ----
            end;
            check_signature (Env.add_type id decl env)
                            (Ident.name id :: seen) rem
!       | Module_sig(id, mdecl) :: rem ->
            if List.mem (Ident.name id) seen 
            then error "repeated module name";
! 	  check_moddecl env mdecl;
!           check_signature (Env.add_module id mdecl env) 
                            (Ident.name id :: seen) rem
+     and check_moddecl env mdecl =
+       let mty = mdecl.ty in
+       check_modtype env mdecl.Mod.ty;
+       match mdecl.Mod.eq with
+ 	| None -> ()
+ 	| Some path ->
+ 	    let mty' = strengthen_modtype path (Env.find_module path env) in
+ 	    modtype_match env mty' mty
  
      let rec type_module env = function
          Longident path ->
***************
*** 390,396 ****
        | Functor(param, mty, body) ->
            check_modtype env mty;
            Functor_type(param, mty,
!               type_module (Env.add_module param mty env) body)
        | Apply(funct, (Longident path as arg)) ->
            (match type_module env funct with
              Functor_type(param, mty_param, mty_res) ->
--- 452,458 ----
        | Functor(param, mty, body) ->
            check_modtype env mty;
            Functor_type(param, mty,
!               type_module (Env.add_absmodule param mty env) body)
        | Apply(funct, (Longident path as arg)) ->
            (match type_module env funct with
              Functor_type(param, mty_param, mty_res) ->
***************
*** 417,423 ****
        | Module_str(id, modl) ->
            if List.mem (Ident.name id) seen
            then error "repeated module name";
!           (Module_sig(id, type_module env modl), Ident.name id :: seen)
        | Type_str(id, kind, typ) ->
            if List.mem (Ident.name id) seen
            then error "repeated type name";
--- 479,487 ----
        | Module_str(id, modl) ->
            if List.mem (Ident.name id) seen
            then error "repeated module name";
! 	  let eq = match modl with Longident p -> Some p | _ -> None in
! 	  let mdecl = { Mod.ty = type_module env modl ; Mod.eq = eq } in
!           (Module_sig(id, mdecl), Ident.name id :: seen)
        | Type_str(id, kind, typ) ->
            if List.mem (Ident.name id) seen
            then error "repeated type name";
***************
*** 525,533 ****
        | Type_sig(id, decl) :: rem ->
            Type_sig(id, scope_typedecl sc decl) ::
            scope_signature (Scope.enter_type id sc) rem
!       | Module_sig(id, mty) :: rem ->
!           Module_sig(id, scope_modtype sc mty) ::
            scope_signature (Scope.enter_module id sc) rem
      let rec scope_module sc = function
          Longident path -> Longident(Scope.module_path path sc)
        | Structure str -> Structure(scope_structure sc str)
--- 589,604 ----
        | Type_sig(id, decl) :: rem ->
            Type_sig(id, scope_typedecl sc decl) ::
            scope_signature (Scope.enter_type id sc) rem
!       | Module_sig(id, mdecl) :: rem ->
!           Module_sig(id, scope_moddecl sc mdecl) ::
            scope_signature (Scope.enter_module id sc) rem
+     and scope_moddecl sc mdecl =
+       let mty = scope_modtype sc mdecl.Mod.ty in
+       let meq = match mdecl.eq with
+ 	| None -> None
+ 	| Some path -> Some (Scope.module_path path sc)
+       in
+       { Mod.ty = mty; Mod.eq = meq }
      let rec scope_module sc = function
          Longident path -> Longident(Scope.module_path path sc)
        | Structure str -> Structure(scope_structure sc str)

[-- Attachment #3: .signature --]
[-- Type: text/plain, Size: 226 bytes --]


-- 
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

[Caml-list] Camlp4 3.01 released

[Daniel de Rauglaudre]

Hi evribody,

Camlp4 3.01 compatible with OCaml 3.01 has been released
      http://caml.inria.fr/camlp4/

-- 
Daniel de RAUGLAUDRE
daniel.de_rauglaudre@inria.fr
http://cristal.inria.fr/~ddr/
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

[Caml-list] Caml 3.01 : pb with include

[Christophe Raffalli]

I tried to use the new include feature for my algebra library. I failed
!
Am I missing something ?

Here is a small example I created just to show the problem:

module type Semi_Group =
sig
  type t
  val e : t
  val ( ** ) : t -> t -> t
end

module type Group =
sig
  include Semi_Group
  val inv : t -> t
end

module type Semi_Group_Morphism =
sig
  module SG1 : Semi_Group
  module SG2 : Semi_Group
  val f : SG1.t -> SG2.t
end

module type Group_Morphism =
sig
  module G1 : Group
  module G2 : Group
  include Semi_Group_Morphism with module SG1 = G1 and module SG2 = G2
end

(*
Nice : SG1 et SG2 are groups : Here isCaml answer 

module type Group_Morphism =
  sig
    module G1 : Group
    module G2 : Group
    module SG1 :
      sig
        type t = G1.t
        val e : t
        val ( ** ) : t -> t -> t
        val inv : t -> t
      end
    module SG2 :
      sig
        type t = G2.t
        val e : t
        val ( ** ) : t -> t -> t
        val inv : t -> t
      end
    val f : SG1.t -> SG2.t
 
end                                                                           
*)

module Idt_Semi_Group_Morphism(SG : Semi_Group) = (
struct
  module SG1 = SG
  module SG2 = SG
  let f = fun x -> x
end : Semi_Group_Morphism with module SG1 = SG and module SG2 = SG)

module Idt_Group_Morphism(G : Group) = (
struct
  module G1 = G
  module G2 = G
  include (Idt_Semi_Group_Morphism(G) : Semi_Group_Morphism with module
SG1 = G and module SG2 = G)
end : Group_Morphism with module SG1 = G and module SG2 = G and module
G1 = G and module G2 = G)

(* 
Heavy and does not work ! 

Signature mismatch:
Modules do not match:
  sig
    module SG1 : sig type t = G.t val e : t val ( ** ) : t -> t -> t end
    module SG2 : sig type t = G.t val e : t val ( ** ) : t -> t -> t end
    val f : SG1.t -> SG2.t
  end
is not included in
  sig
    module SG1 :
      sig
        type t = G.t
        val e : t
        val ( ** ) : t -> t -> t
        val inv : t -> t
      end
    module SG2 :
      sig
        type t = G.t
        val e : t
        val ( ** ) : t -> t -> t
        val inv : t -> t
      end
    val f : SG1.t -> SG2.t
  end
Modules do not match:
  sig type t = G.t val e : t val ( ** ) : t -> t -> t end
is not included in
  sig type t = G.t val e : t val ( ** ) : t -> t -> t val inv : t -> t
end
The field `inv' is required but not
provided                                    
*)

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

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

[Andreas Rossberg]

Christophe Raffalli wrote:
> 
> I tried to use the new include feature for my algebra library. I failed
> !
> Am I missing something ?

Actually it is not the include feature causing the trouble, but rather
your use of with module constraints.

> Here is a small example I created just to show the problem:
> 
> module type Semi_Group =
> sig
>   type t
>   val e : t
>   val ( ** ) : t -> t -> t
> end
> 
> module type Group =
> sig
>   include Semi_Group
>   val inv : t -> t
> end
> 
> module type Semi_Group_Morphism =
> sig
>   module SG1 : Semi_Group
>   module SG2 : Semi_Group
>   val f : SG1.t -> SG2.t
> end
> 
> module type Group_Morphism =
> sig
>   module G1 : Group
>   module G2 : Group
>   include Semi_Group_Morphism with module SG1 = G1 and module SG2 = G2
> end
> 
> (*
> Nice : SG1 et SG2 are groups : Here isCaml answer

Well, not so nice really, because this treatment exactly is what causes
the later error. See below.

> module type Group_Morphism =
>   sig
>     module G1 : Group
>     module G2 : Group
>     module SG1 :
>       sig
>         type t = G1.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     module SG2 :
>       sig
>         type t = G2.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     val f : SG1.t -> SG2.t
> 
> end
> *)
> 
> module Idt_Semi_Group_Morphism(SG : Semi_Group) = (
> struct
>   module SG1 = SG
>   module SG2 = SG
>   let f = fun x -> x
> end : Semi_Group_Morphism with module SG1 = SG and module SG2 = SG)
> 
> module Idt_Group_Morphism(G : Group) = (
> struct
>   module G1 = G
>   module G2 = G
>   include (Idt_Semi_Group_Morphism(G) : Semi_Group_Morphism with module
> SG1 = G and module SG2 = G)
> end : Group_Morphism with module SG1 = G and module SG2 = G and module
> G1 = G and module G2 = G)

Just an aside: some of the outer module constraints here are redundant,
because they are already specified in the signature Group_Morphism. It
should suffice to say:

 ... : Group_Morphism with module G1 = G and module G2 = G

The signature annotation (at the include) also is a bit unnecessary, but
is the one that seems to be causing the error.

> (*
> Heavy and does not work !
> 
> Signature mismatch:
> Modules do not match:
>   sig
>     module SG1 : sig type t = G.t val e : t val ( ** ) : t -> t -> t end
>     module SG2 : sig type t = G.t val e : t val ( ** ) : t -> t -> t end
>     val f : SG1.t -> SG2.t
>   end

That is the result signature of the functor application
Idt_Semi_Group_Morphism(G).

> is not included in
>   sig
>     module SG1 :
>       sig
>         type t = G.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     module SG2 :
>       sig
>         type t = G.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     val f : SG1.t -> SG2.t
>   end

And that is the signature the compiler seems to calculate for

  Semi_Group_Morphism with module SG1 = G and module SG2 = G

Like in the case of Group_morphism above, SG1 and SG2 contain an inv
member in this signature. I think this semantics of module constraints
is not right - it should not extend subsignatures, only propagate type
identities. This not exactly is a bug, but IMHO not what you want in
most situations - at least not in this particular situation. Was there a
particular motivation to design the language this way?

> Modules do not match:
>   sig type t = G.t val e : t val ( ** ) : t -> t -> t end
> is not included in
>   sig type t = G.t val e : t val ( ** ) : t -> t -> t val inv : t -> t
> end
> The field `inv' is required but not
> provided
> *)

And this is correct, given the semantics of module constraints.

The simplest workaround is to remove the signature annotation at the
include spec (did not try it, though). Alternatively, you could avoid
using module constraints and restrict yourself to type constraints, ie.

  include (Idt_Semi_Group_Morphism(G) : Semi_Group_Morphism
           with type SG1.t = G.t and type SG2.t = G.t)

And similar in signature Group_Morphism.

Best regards,

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids.
 If Pac Man affected us as kids, we would all be running around in
 darkened rooms, munching pills, and listening to repetitive music."
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

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

[Xavier Leroy]

> Like in the case of Group_morphism above, SG1 and SG2 contain an inv
> member in this signature. I think this semantics of module constraints
> is not right - it should not extend subsignatures, only propagate type
> identities. This not exactly is a bug, but IMHO not what you want in
> most situations - at least not in this particular situation. Was there a
> particular motivation to design the language this way?

I can't remember, but the design and implementation of "with module"
dates back to 1996, so my memory is a bit hazy :-)

I agree with you that the most natural interpretation of the "with
module" constraint is to stand for a bunch of "with type" constraints
on the type components of the modules.  With this interpretation, the
current behavior is a bug.  SML'97 also interprets sharing constraints
between structures as the implied sharing constraints between the type
components of these modules.

There might be examples of signature surgery where the current
behavior is useful (I need to go back to my examples to check),
but I agree it's confusing.

- Xavier Leroy
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

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

[Andreas Rossberg]

Xavier Leroy wrote:
> 
> I can't remember, but the design and implementation of "with module"
> dates back to 1996, so my memory is a bit hazy :-)

BTW, to challenge your memory a bit more :-), was there a reason not to
integrate manifest module specifications along with "with module"? It
seems a bit odd that I can write

  sig
    module X : S
  end
  with module X = Y

and now even

  sig
    module X : S
    include sig module Y : T end with module Y = X
  end

but not simply

  sig
    module X : S = Y
  end

and

  sig
    module X : S
    module Y : T = X
  end

as for types.

> There might be examples of signature surgery where the current
> behavior is useful (I need to go back to my examples to check),

I believe so as well, but up to now I was not able to come up with any.
If you have an interesting example, I would like to learn about it.

Cheers,
	- Andreas


PS: The docs seem to be somewhat `conservative' on include for
signatures: they say the syntax is

	include modtype-path

but obviously it is the more general

	include module-type

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids.
 If Pac Man affected us as kids, we would all be running around in
 darkened rooms, munching pills, and listening to repetitive music."
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr

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

[Christophe Raffalli]

What I realy would like are more flexible include and constaints to make the
following work:

module type Semi_Group =
sig
  type t
  val e : t
  val ( ** ) : t -> t -> t
end

module type Group =
sig
  include Semi_Group
  val inv : t -> t
end

module type Semi_Group_Morphism =
sig
  module G1 : Semi_Group
  module G2 : Semi_Group
  val f : G1.t -> G2.t
end

(* I would like to be able to use include for the next definition:
something like:

module type Group_Morphism =
sig
  include Semi_Group_Morphism with module G1 : Group and module G2 : Group
end
*)

module type Group_Morphism =
sig
  module G1 : Group
  module G2 : Group
  val f : G1.t -> G2.t
end

module Idt_Semi_Group_Morphism(SG : Semi_Group) = (
struct
  module G1 = SG
  module G2 = SG
  let f = fun x -> x
end : Semi_Group_Morphism with module G1 = SG and module G2 = SG)

(* I can't make the next definition work using include at all *)
 
module Idt_Group_Morphism(G : Group) = (
struct
  include (Idt_Semi_Group_Morphism(G) : Semi_Group_Morphism with module G1 = G
and module G2 = G)
end : Group_Morphism with module G1 = G and module G2 = G)

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr