From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p8K93mwC017437 for ; Tue, 20 Sep 2011 11:03:48 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am0BALxVeE7B/BfSkWdsb2JhbABCmSmMQ4F3AQEBAQkLCwcUAyKBUwEBBThAARALGAkWDwkDAgECAUUTAQcBAYd1tGCGeQSTS4UejBI X-IronPort-AV: E=Sophos;i="4.68,410,1312149600"; d="scan'208";a="109696659" Received: from msa01.smtpout.orange.fr (HELO msa.smtpout.orange.fr) ([193.252.23.210]) by mail4-smtp-sop.national.inria.fr with ESMTP; 20 Sep 2011 11:03:43 +0200 Received: from [192.168.1.63] ([83.199.86.214]) by mwinf5d48 with ME id ax3h1h00l4dUC2T03x3idK; Tue, 20 Sep 2011 11:03:42 +0200 X-ME-engine: default Message-ID: <4E7856EE.3050903@lexifi.com> Date: Tue, 20 Sep 2011 11:03:42 +0200 From: Alain Frisch Organization: LexiFi User-Agent: Mozilla/5.0 (X11; U; Linux i686 (x86_64); en-US; rv:1.9.2.22) Gecko/20110902 Thunderbird/3.1.14 MIME-Version: 1.0 To: yminsky@gmail.com CC: caml-list@inria.fr References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Validation-by: alain@frisch.fr Subject: Re: [Caml-list] A limitation of "with type" declarations for first-class modules On 09/20/2011 03:36 AM, Yaron Minsky wrote: > For some reason, 1st-class modules have more restrictive "with" syntax, > which turns out to be a practical problem. > > The main constraint is that with constraints do not seem to be able to > refer to sub-modules. Consider the following code snippet: > >> module type Foo = sig type t end >> module type Bar = sig module Foo : Foo end >> >> (* compiles *) >> let g (type a) (m : (module Foo with type t = a)) = () >> >> (* fails to compile with a syntax error *) >> let f (type a) (m : (module Bar with type Foo.t = a)) = () > > Of course, ordinary modules have no such constraint. Any thoughts as to > what is going on here, and whether it can be fixed? 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! Similarly, one could allow "with type t :=" constraints in addition to "with type t =". Is there a need for that? 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!). -- Alain