From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p49GSG8K004108 for ; Mon, 9 May 2011 18:28:16 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao0CAP8UyE3RVaE2kGdsb2JhbACXYYZahz0IFAEBAQEJCQ0HFAQhiHGha4wZCoInhG02iF8BAQMGhgYEgimNPIUEgzyCMTsrgyI X-IronPort-AV: E=Sophos;i="4.64,341,1301868000"; d="scan'208";a="82691692" Received: from mail-fx0-f54.google.com ([209.85.161.54]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 09 May 2011 18:28:11 +0200 Received: by fxm11 with SMTP id 11so8001031fxm.27 for ; Mon, 09 May 2011 09:28:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:reply-to:in-reply-to:references :date:message-id:subject:from:to:cc:content-type; bh=xBYv+P2iB/LEx56RF6TCXVZePPqzz1oeH7gSFCrEM6A=; b=DInujmfamImXmxxBYu21JVHr+vgmNR+JOGItomyzV7VIRHeEXFp+wxkFX7YKQhZ+uC bxIlVq8l/+vywb17+fosCFrE+M2TKuMChp9o1LX9zqx5mf04SHkCP+IXRVTyMC5D1ZyE 59wd332sXyiZvVPJMhkYO6I5kZBiXS+pFqID8= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:reply-to:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; b=jD2WOL/+62hfVSuG2sDIoIjbzLgwyXzWqDyOYePyUl5TmTKjOJALtWyPMYn+y8WuUS 7o13CMSEWmRum5rIBFsEaNwLQyVIK3bcKmsSQ2W4J3NRB9dV8e20/9p/VKQVVZeK8LO3 EUSI9x4zstWo+8pWpTOkW8/KfOHg7odckk5rc= MIME-Version: 1.0 Received: by 10.223.24.153 with SMTP id v25mr177065fab.29.1304958396076; Mon, 09 May 2011 09:26:36 -0700 (PDT) Received: by 10.223.72.5 with HTTP; Mon, 9 May 2011 09:26:36 -0700 (PDT) Reply-To: yminsky@gmail.com In-Reply-To: References: <20110509142702.GZ28842@janestreet.com> Date: Mon, 9 May 2011 12:26:36 -0400 Message-ID: From: Yaron Minsky To: Markus Mottl Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=00151747342ca5153204a2da4d09 Subject: Re: [Caml-list] "with module" surprises --00151747342ca5153204a2da4d09 Content-Type: text/plain; charset=ISO-8859-1 I agree that specializing modules is a reasonable thing to do in general. But that's not what I think the "with" syntax is usually for. It's usually for adding sharing constraints, and this kind of modification of a module is not the same thing as adding a constraint. Note that the following code fails, as I think it should: module type S' = sig end with type t = int Do you by any chance have a use-case that you think benefits from these semantics? y On Mon, May 9, 2011 at 11:12 AM, Markus Mottl wrote: > The current semantics seems to make sense to me. E.g. > > module type M' = sig type t end > > specifies that M' needs a type t. It doesn't say that a module > matching this signature needs to keep t abstract. You can hence > specialize this signature using "with" to e.g. require that it be an > "int". > > Module constraints work similarly. If a signature is empty, this > doesn't mean that a module matching it must not contain anything, > rather the opposite: any module can match it. You can again > specialize the signature using "with" to require further entries. The > module passed to "with" only needs to match the first signature, which > is trivially true in this case. Its own (possibly inferred) signature > will then specialize the previous signature, potentially adding more > entries. > > A maybe more intuitive way to think about this is following: in OCaml > you can only make things more strict, never less strict. An empty > signature is less strict (can be matched by more modules) than a > non-empty one. Hence extending it is the right "direction". > > Markus > > On Mon, May 9, 2011 at 10:27, Yaron Minsky wrote: > > I've gotten bitten recently by the semantics of "with module", and after > > getting an explanation about how this seems to work in OCaml, I'm now > > deeply confused. Here's the example I was shown: > > > > module M = struct > > let x = 13 > > end > > > > module type S = sig > > module M' : sig end > > end > > with module M' = M > > > > The inferred types for this will be: > > > > module M : sig val x : int end > > module type S = sig module M' : sig val x : int end end > > > > Whereas I would have expected this: > > > > module M : sig val x : int end > > module type S = sig module M' : sig end end > > > > In other words, the "with module" constraint has added new structure to > > the signature S, rather than just adding constraints. This strikes me > > as deeply strange, and indeed, has caused a bunch of head-scratching > > here when using "with module". Is this a bug? Or is this really the > > desired semantics. My understanding is that in SML, "with module" > > simply adds in a bunch of type-level sharing constraints. From that > > point of view, this behavior is pretty surprising. > > > > Not only that, it's what the OCaml manual says. From section 6.10.4 > > > > The constraint [module module-path = extended-module-path] adds type > > equations to all type components of the sub-structure denoted by > > [module-path], making them equivalent to the corresponding type > > components of the structure denoted by [extended-module-path]. > > > > y > > > > -- > > Yaron Minsky > > > > -- > > Caml-list mailing list. Subscription management and archives: > > https://sympa-roc.inria.fr/wws/info/caml-list > > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > > Bug reports: http://caml.inria.fr/bin/caml-bugs > > > > > > > > -- > Markus Mottl http://www.ocaml.info markus.mottl@gmail.com > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --00151747342ca5153204a2da4d09 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable I agree that specializing modules is a reasonable thing to do in general.= =A0 But that's not what I think the "with" syntax is usually = for.=A0 It's usually for adding sharing constraints, and this kind of m= odification of a module is not the same thing as adding a constraint.=A0 No= te that the following code fails, as I think it should:

=A0 module type S' =3D sig end
=A0 with type t =3D int

Do= you by any chance have a use-case that you think benefits from these seman= tics?

y

On Mon, May 9, 2011 at 11:= 12 AM, Markus Mottl <markus.mottl@gmail.com> wrote:
The current seman= tics seems to make sense to me. =A0E.g.

=A0module type M' =3D sig type t end

specifies that M' needs a type t. =A0It doesn't say that a module matching this signature needs to keep t abstract. =A0You can hence
specialize this signature using "with" to e.g. require that it be= an
"int".

Module constraints work similarly. =A0If a signature is empty, this
doesn't mean that a module matching it must not contain anything,
rather the opposite: any module can match it. =A0You can again
specialize the signature using "with" to require further entries.= =A0The
module passed to "with" only needs to match the first signature, = which
is trivially true in this case. =A0Its own (possibly inferred) signature
will then specialize the previous signature, potentially adding more
entries.

A maybe more intuitive way to think about this is following: in OCaml
you can only make things more strict, never less strict. =A0An empty
signature is less strict (can be matched by more modules) than a
non-empty one. =A0Hence extending it is the right "direction".

Markus

On Mon, May 9, 2011 at 10:27, Yaron Minsky <yminsky@janestreet.com> wrote:
> I've gotten bitten recently by the semantics of "with module&= quot;, and after
> getting an explanation about how this seems to work in OCaml, I'm = now
> deeply confused. =A0Here's the example I was shown:
>
> =A0module M =3D struct
> =A0 =A0let x =3D 13
> =A0end
>
> =A0module type S =3D sig
> =A0 =A0module M' : sig end
> =A0end
> =A0with module M' =3D M
>
> The inferred types for this will be:
>
> =A0module M : sig val x : int end
> =A0module type S =3D sig module M' : sig val x : int end end
>
> Whereas I would have expected this:
>
> =A0module M : sig val x : int end
> =A0module type S =3D sig module M' : sig end end
>
> In other words, the "with module" constraint has added new s= tructure to
> the signature S, rather than just adding constraints. =A0This strikes = me
> as deeply strange, and indeed, has caused a bunch of head-scratching > here when using "with module". =A0Is this a bug? =A0Or is th= is really the
> desired semantics. =A0My understanding is that in SML, "with modu= le"
> simply adds in a bunch of type-level sharing constraints. =A0From that=
> point of view, this behavior is pretty surprising.
>
> Not only that, it's what the OCaml manual says. =A0From section 6.= 10.4
>
> =A0The constraint [module module-path =3D extended-module-path] adds t= ype
> =A0equations to all type components of the sub-structure denoted by
> =A0[module-path], making them equivalent to the corresponding type
> =A0components of the structure denoted by [extended-module-path].
>
> y
>
> --
> Yaron Minsky
>
> --
> Caml-list mailing list. =A0Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>



--
Markus Mottl=A0 =A0 =A0 =A0 http://www.ocaml.info=A0 =A0 =A0 =A0 markus.mottl@gmail.com


--
Caml-list mailing list. =A0Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


--00151747342ca5153204a2da4d09--