* RE: [Caml-list] Caml 3.01 : pb with include @ 2001-03-21 13:25 Dave Berry 2001-03-21 16:15 ` Judicael Courant 0 siblings, 1 reply; 9+ messages in thread From: Dave Berry @ 2001-03-21 13:25 UTC (permalink / raw) To: Xavier Leroy, Andreas Rossberg; +Cc: caml-list, Christophe Raffalli 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [Caml-list] Caml 3.01 : pb with include 2001-03-21 13:25 [Caml-list] Caml 3.01 : pb with include Dave Berry @ 2001-03-21 16:15 ` Judicael Courant 0 siblings, 0 replies; 9+ messages in thread From: Judicael Courant @ 2001-03-21 16:15 UTC (permalink / raw) To: caml-list; +Cc: Dave Berry, Xavier Leroy, Andreas Rossberg, Christophe Raffalli 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* RE: [Caml-list] Caml 3.01 : pb with include @ 2001-03-23 12:02 Dave Berry 2001-03-27 9:19 ` Judicael Courant 0 siblings, 1 reply; 9+ messages in thread From: Dave Berry @ 2001-03-23 12:02 UTC (permalink / raw) To: Judicael Courant, caml-list Cc: Xavier Leroy, Andreas Rossberg, Christophe Raffalli 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* RE: [Caml-list] Caml 3.01 : pb with include 2001-03-23 12:02 Dave Berry @ 2001-03-27 9:19 ` Judicael Courant 0 siblings, 0 replies; 9+ messages in thread From: Judicael Courant @ 2001-03-27 9:19 UTC (permalink / raw) To: Dave Berry; +Cc: caml-list, Xavier Leroy, Andreas Rossberg, Christophe Raffalli [-- 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* [Caml-list] Camlp4 3.01 released @ 2001-03-11 5:04 Daniel de Rauglaudre 2001-03-12 11:52 ` [Caml-list] Caml 3.01 : pb with include Christophe Raffalli 0 siblings, 1 reply; 9+ messages in thread From: Daniel de Rauglaudre @ 2001-03-11 5:04 UTC (permalink / raw) To: caml-list 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* [Caml-list] Caml 3.01 : pb with include 2001-03-11 5:04 [Caml-list] Camlp4 3.01 released Daniel de Rauglaudre @ 2001-03-12 11:52 ` Christophe Raffalli 2001-03-12 17:13 ` Andreas Rossberg 0 siblings, 1 reply; 9+ messages in thread From: Christophe Raffalli @ 2001-03-12 11:52 UTC (permalink / raw) To: caml-list 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [Caml-list] Caml 3.01 : pb with include 2001-03-12 11:52 ` [Caml-list] Caml 3.01 : pb with include Christophe Raffalli @ 2001-03-12 17:13 ` Andreas Rossberg 2001-03-13 10:32 ` Xavier Leroy 0 siblings, 1 reply; 9+ messages in thread From: Andreas Rossberg @ 2001-03-12 17:13 UTC (permalink / raw) To: caml-list; +Cc: Christophe Raffalli 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [Caml-list] Caml 3.01 : pb with include 2001-03-12 17:13 ` Andreas Rossberg @ 2001-03-13 10:32 ` Xavier Leroy 2001-03-13 11:18 ` Andreas Rossberg 2001-03-13 11:23 ` Christophe Raffalli 0 siblings, 2 replies; 9+ messages in thread From: Xavier Leroy @ 2001-03-13 10:32 UTC (permalink / raw) To: Andreas Rossberg; +Cc: caml-list, Christophe Raffalli > 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [Caml-list] Caml 3.01 : pb with include 2001-03-13 10:32 ` Xavier Leroy @ 2001-03-13 11:18 ` Andreas Rossberg 2001-03-13 11:23 ` Christophe Raffalli 1 sibling, 0 replies; 9+ messages in thread From: Andreas Rossberg @ 2001-03-13 11:18 UTC (permalink / raw) To: Xavier Leroy; +Cc: caml-list, Christophe Raffalli 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [Caml-list] Caml 3.01 : pb with include 2001-03-13 10:32 ` Xavier Leroy 2001-03-13 11:18 ` Andreas Rossberg @ 2001-03-13 11:23 ` Christophe Raffalli 1 sibling, 0 replies; 9+ messages in thread From: Christophe Raffalli @ 2001-03-13 11:23 UTC (permalink / raw) To: Xavier Leroy; +Cc: Andreas Rossberg, caml-list 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2001-03-27 9:19 UTC | newest] Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2001-03-21 13:25 [Caml-list] Caml 3.01 : pb with include Dave Berry 2001-03-21 16:15 ` Judicael Courant -- strict thread matches above, loose matches on Subject: below -- 2001-03-23 12:02 Dave Berry 2001-03-27 9:19 ` Judicael Courant 2001-03-11 5:04 [Caml-list] Camlp4 3.01 released Daniel de Rauglaudre 2001-03-12 11:52 ` [Caml-list] Caml 3.01 : pb with include Christophe Raffalli 2001-03-12 17:13 ` Andreas Rossberg 2001-03-13 10:32 ` Xavier Leroy 2001-03-13 11:18 ` Andreas Rossberg 2001-03-13 11:23 ` Christophe Raffalli
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).