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 p8KADVVW021842 for ; Tue, 20 Sep 2011 12:13:31 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AloCANpmeE7RVdQ2kGdsb2JhbAAoGqA/AYcSCBQBAQEBCQkNBxQEIoFTAQEBAQIBCwcCFxUBGx0BAwELBgULOyEBAQwBBAEFAQMBGAYTCBqHVQYklwQKi0EKglKFWDuIbQIDBoZ3BIdui12GC4QIgnE9OYNC X-IronPort-AV: E=Sophos;i="4.68,410,1312149600"; d="scan'208";a="120538444" 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:13:29 +0200 Received: by vws11 with SMTP id 11so1055889vws.27 for ; Tue, 20 Sep 2011 03:13:28 -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=jI+ecJqOD6pes+PRb65+5aWNq4rUdJnPbaD7JXy5ey0=; b=pTkPPMU8C7oD+qSJYZ8+4WHIGUF3G4CANgOvlCoArRFFj2fZFBqgYjCIdjgA8a1ZeL l+I7uRbn+0qc6LtIhD+KmGTpv9GQpKWbEWdwIfQKIDhrzwbA2vtPreKEImQX+8+G2JzO gSxpPhuhKPh2kHX3ozs5Xt6hXqrs/5mhqA+j0= MIME-Version: 1.0 Received: by 10.52.175.135 with SMTP id ca7mr520840vdc.171.1316513608824; Tue, 20 Sep 2011 03:13:28 -0700 (PDT) Received: by 10.220.152.84 with HTTP; Tue, 20 Sep 2011 03:13:28 -0700 (PDT) Reply-To: yminsky@gmail.com In-Reply-To: References: <4E7856EE.3050903@lexifi.com> Date: Tue, 20 Sep 2011 18:13:28 +0800 Message-ID: From: Yaron Minsky To: Alain Frisch Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=bcaec5101c71fef60504ad5cb5a3 Subject: Re: [Caml-list] A limitation of "with type" declarations for first-class modules --bcaec5101c71fef60504ad5cb5a3 Content-Type: text/plain; charset=ISO-8859-1 For anyone who is interested, here is the bug report: http://caml.inria.fr/mantis/view.php?id=5358 y On Tue, Sep 20, 2011 at 6:07 PM, Yaron Minsky wrote: > 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 > > --bcaec5101c71fef60504ad5cb5a3 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable For anyone who is interested, here is the bug report:

=A0=A0 http://caml.inria.fr/ma= ntis/view.php?id=3D5358

y

On T= ue, Sep 20, 2011 at 6:07 PM, Yaron Minsky <yminsky@gmail.com> wrote:
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" constraints in addition to "with type t =3D". = =A0Is there a need for that?

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

Would that replace the dependence on pat= hs that you describe above?=A0 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


--bcaec5101c71fef60504ad5cb5a3--