From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8KA7WcW021419 for ; Tue, 20 Sep 2011 12:07:32 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkECAKBkeE7RVdQ2kGdsb2JhbABCp1IIFAEBAQEJCQ0HFAQigVMBAQEBAgELBwIXFQEbHQEDAQsGBQs7IgEMAQQBBQEDARgGEwgah1WXPgqLQQqCUoVUO4htAgMGhncEh26LXYYLhnk9OYNC X-IronPort-AV: E=Sophos;i="4.68,410,1312149600"; d="scan'208";a="120537054" Received: from mail-vw0-f54.google.com ([209.85.212.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 20 Sep 2011 12:07:24 +0200 Received: by vws11 with SMTP id 11so1046118vws.27 for ; Tue, 20 Sep 2011 03:07:23 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:reply-to:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; bh=ikYKNuASi2XtrCCQw5cTcGy/eQePby8uZ25H8MppeuU=; b=DYUrUhhrQdvmB4fcorghARyzw69bzv5nEjovfzkPFiu5hn/4LBA7EPshCuyVev6Zp8 cVoKCr6HQvcsbielCplwpflI8rqNMubXiKzWRSmwjWRLHjoJQHQjUOHz0mLKQkHyeRnk 27lx1J/Nlfd+rWOPZ/AlCMk3cO+yHWFGgQCQw= MIME-Version: 1.0 Received: by 10.220.107.5 with SMTP id z5mr135802vco.176.1316513243587; Tue, 20 Sep 2011 03:07:23 -0700 (PDT) Received: by 10.220.152.84 with HTTP; Tue, 20 Sep 2011 03:07:23 -0700 (PDT) Reply-To: yminsky@gmail.com In-Reply-To: <4E7856EE.3050903@lexifi.com> References: <4E7856EE.3050903@lexifi.com> Date: Tue, 20 Sep 2011 18:07:23 +0800 Message-ID: From: Yaron Minsky To: Alain Frisch Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=f46d043c7bd439e3fa04ad5ca0b4 Subject: Re: [Caml-list] A limitation of "with type" declarations for first-class modules --f46d043c7bd439e3fa04ad5ca0b4 Content-Type: text/plain; charset=ISO-8859-1 On Tue, Sep 20, 2011 at 5:03 PM, Alain Frisch wrote: > > The important point is that package types (the ... in a type expression > (module ...) or in an expression (module M : ...)) are not module types. > Syntactically, they are indeed a subset of module types, but it is a strict > subset, and they obey different rules than module types. > > Package types live at the boundary between types and module types. In a > packing expression (module M : ...), the package type must produce a > well-typed module type. This is why you cannot write (module M : S with type > t = 'a), because "S with type t = 'a" is not a proper module type. But > (module S with type t = 'a) is a correct type. > > Package types must also support all operations on types, including > equality, unification, etc. For instance, unifying (module S1 with type t = > 'a) and (module S2 with type t = 'b) is defined as checking than S1 and S2 > are equivalent paths and unifying 'a and 'b. The fact that a package type > can also be seen as a module type is nowhere used in this definition. (Of > course, one must be careful when defining equality of package types that it > does not allow to cast a module from one module type to an incompatible > one.) > > There is some flexibility in both the definition of admissible package > types and the definition of equality between package types. > > For instance, I don't see any problem or difficulty in your proposal of > allowing constraints on types nested in sub-modules (but this should be > checked carefully). Feel free to open a feature request for this! Will do. > Similarly, one could allow "with type t :=" constraints in addition to > "with type t =". Is there a need for that? I haven't seen one yet, but I'll keep my eyes out. > One could also relax equality of package types (module S1 with ...) and > (module S2 with ...) by checking that S1 and S2 expand to structurally > equivalent module types (with the exact same ordering between value > components!). > Would that replace the dependence on paths that you describe above? The use of paths has turned out to be pretty fragile in my experience, with module types that should have been the same showing up as different in the presence of rebinding of module signatures, which we would normally do as a way of improving concision and readability. y --f46d043c7bd439e3fa04ad5ca0b4 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable On Tue, Sep 20, 2011 at 5:03 PM, Alain Frisch <alain.frisch@lexifi.com> = wrote:

The important point is that package types (the ... in a type expression (mo= dule ...) or in an expression (module M : ...)) are not module types. Synta= ctically, they are indeed a subset of module types, but it is a strict subs= et, and they obey different rules than module types.

Package types live at the boundary between types and module types. In a pac= king expression (module M : ...), the package type must produce a well-type= d module type. This is why you cannot write (module M : S with type t =3D &= #39;a), because "S with type t =3D 'a" is not a proper module= type. But (module S with type t =3D 'a) is a correct type.

Package types must also support all operations on types, including equality= , unification, etc. =A0For instance, unifying (module S1 with type t =3D &#= 39;a) and (module S2 with type t =3D 'b) is defined as checking than S1= and S2 are equivalent paths and unifying 'a and 'b. The fact that = a package type can also be seen as a module type is nowhere used in this de= finition. (Of course, one must be careful when defining equality of package= types that it does not allow to cast a module from one module type to an i= ncompatible one.)

There is some flexibility in both the definition of admissible package type= s and the definition of equality between package types.

For instance, I don't see any problem or difficulty in your proposal of= allowing constraints on types nested in sub-modules (but this should be ch= ecked carefully). Feel free to open a feature request for this!

Will do.
=A0
Similarly, one could allow "with type t :=3D" constr= aints in addition to "with type t =3D". =A0Is there a need for th= at?

I haven't seen one yet, but I'll keep my eyes out.
=A0<= /div>
=A0One could= also relax equality of package types (module S1 with ...) and (module S2 w= ith ...) by checking that S1 and S2 expand to structurally equivalent modul= e types (with the exact same ordering between value components!).

Would that replace the dependence on paths tha= t you describe above?=A0 The use of paths has turned out to be pretty fragi= le in my experience, with module types that should have been the same showi= ng up as different in the presence of rebinding of module signatures, which= we would normally do as a way of improving concision and readability.

y

--f46d043c7bd439e3fa04ad5ca0b4--