From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 0B1AA5D6 for ; Fri, 21 Sep 2018 01:25:50 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.54,282,1534802400"; d="scan'208,217";a="347377134" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 Sep 2018 03:25:50 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 0F2B3824E4; Fri, 21 Sep 2018 03:25:50 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 8802D824CF for ; Fri, 21 Sep 2018 03:25:43 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arlencox@gmail.com; spf=Pass smtp.mailfrom=arlencox@gmail.com; spf=None smtp.helo=postmaster@mail-yb1-f182.google.com IronPort-PHdr: =?us-ascii?q?9a23=3A4EmyyxPwZThQjAKF0bMl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0LPX4rarrMEGX3/hxlliBBdydt6obzbKO+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1?= =?us-ascii?q?Ov71GonPhMiryuy+4ZLebxlKiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPde?= =?us-ascii?q?RWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbY?= =?us-ascii?q?UwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhS?= =?us-ascii?q?gIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoak?= =?us-ascii?q?YoYTFeoBOfhXr4/grFYQqhu/ChSnCeT1xT9Sgn/5w6s63PgmEQDJxwEgENcOv2?= =?us-ascii?q?7VrNXxLqsdTee1zKzRwDjFcvhY2i/95ZDWfhw9pfyAR7F9fMrLxUUxCg/Iik+c?= =?us-ascii?q?pZHmMj+L0OkGrnKV4PB6Ve21jm4qswFxrSarxscrkoTJg5gaylHA9SlgwIc6Ps?= =?us-ascii?q?C0RFd1YdK5E5ZcqTuWN4RxQsMlTGFovDg1xqcatp68eSgG0JUnxxjBZPyba4WE?= =?us-ascii?q?/A7vWeKLLTp7hH9pYqyziwu2/ES61+HxVde43E5PriVfk9nMsn4N1wbU6siCUv?= =?us-ascii?q?Zy5F2h2TKR2ADV9u5EJk81mLHUK54k2LEwl54TvV7fES/xnUX6lLWWeVk8+ui0?= =?us-ascii?q?9+TnZa3rqYOGOI9xjgHyK6Aums2kAeQkKQUORGia+eGk1LL550H5QbNKjuc3kq?= =?us-ascii?q?bDqpzaK94b9eaFBFpa25w56hmiAh+j2cgY238OI1VUcVeayYHifVPWc97iCvLq?= =?us-ascii?q?qk6onTEj7PfWdunoGJHAKHPEgJ/ueL987whXzw9lnoMX3I5dFrxUeKG7YUT2rt?= =?us-ascii?q?GNVkZoYTzx+P7uDZBG7q1bXGuOBqGDN6aL6A2H4+suJ6+HY4pH4W+hechg3Obn?= =?us-ascii?q?iDoCoXFYZbOghMJFZ3WxH/AgKEKcMyK134UxVFwStw97d9TEzV2PVTkJOSS3Vq?= =?us-ascii?q?M4oyAxUceoVNeZAI+qh7OF0WGwGZgEPm0=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AjAgAUSKRbhrbbVdFbDg4BAQEEAQEHB?= =?us-ascii?q?AEBhT0og3OBHYJckE+CDYhsao5yC4RsAoNCGQcBBDQUAQMBAQIBAQEBARMBAQE?= =?us-ascii?q?ICwsIKSMMgjUigmEBAQEBAgEjHQEbHQEDAQsGAwILDSoCAiIBEQEFARw0gwaBa?= =?us-ascii?q?QEDDQiHP5AGPIsLgREFAReCdgWDbgoZJg1YgW8CBhKKXReBQT+EJId/glcCk1K?= =?us-ascii?q?JHQmCDI4ZF48hlGYPIYE4gXYzGggbFTsxgjuCGRqDT4oYViMwjg8BAQ?= X-IPAS-Result: =?us-ascii?q?A0AjAgAUSKRbhrbbVdFbDg4BAQEEAQEHBAEBhT0og3OBHYJ?= =?us-ascii?q?ckE+CDYhsao5yC4RsAoNCGQcBBDQUAQMBAQIBAQEBARMBAQEICwsIKSMMgjUig?= =?us-ascii?q?mEBAQEBAgEjHQEbHQEDAQsGAwILDSoCAiIBEQEFARw0gwaBaQEDDQiHP5AGPIs?= =?us-ascii?q?LgREFAReCdgWDbgoZJg1YgW8CBhKKXReBQT+EJId/glcCk1KJHQmCDI4ZF48hl?= =?us-ascii?q?GYPIYE4gXYzGggbFTsxgjuCGRqDT4oYViMwjg8BAQ?= X-IronPort-AV: E=Sophos;i="5.54,282,1534802400"; d="scan'208,217";a="347377122" Received: from mail-yb1-f182.google.com ([209.85.219.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Sep 2018 03:25:42 +0200 Received: by mail-yb1-f182.google.com with SMTP id p74-v6so4196708ybc.9 for ; Thu, 20 Sep 2018 18:25:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=+21pmASKgEorU3VPIBsf77Li6Sqw8hg50tmWvbPxrro=; b=g1IOrrvfhaoGi2iGXRqSz+ietqrtl4ccVYeZ2TkcRlh924U283lpBkzcd8//OEgfRs khM9P2BD5D2AaETfc7gcTG0o/stR1G6ACOvHv2VuFp+LM3slMjjV7YE36XAaAvp9nCge GDT3Ky1QsBDux+WBQvN4cThFWLrbY7Gp5MEF5tDdlAq3PNgU5dW173s6DzTKO05nO6Qi eVM1eOFC/eKPIoFtAWmX10uMLKoL7reOkXbueSxYHydn0ipoKqJpB8KEA0cNeXMJ6QKk GU7FHFntA3Xb3dSKzE1Wg+0yUeLpevHsjllw1yxF+pw+ey+mNAJzh8W7FrfBc5ffmBPW O2AA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=+21pmASKgEorU3VPIBsf77Li6Sqw8hg50tmWvbPxrro=; b=kwsfwpfJgsDbnnGwkV1ta2nWAM9/95FJ3NcZUltj5QrWzxIcH7+ilUOls/xebloDdy 5mCpolJpCt5NwbpwiTHfQVoLFLf5GEwcYUVW0i3CXS7BT85p7mVjoYhWk5z6GHLRiJJ3 kQa2PKQR3Qeoc7+JRBOZ+0BNSWvluqmUuUQkMKuXcECKcYNLgd9o5JAOCzvrttE7DeOD oj9xr7d/cRs1lp55LXI+x3lccj0kDp6F+GcWxa6QS0I17i2N/g1PEl4bPpCOWKzcqclz xejl2NT5dRQerQaX5gW7IAMXmCBLH4bp1e9hDjKJcSviqS/mMGYuUxauF+1ubjL52pzW Pn/g== X-Gm-Message-State: APzg51DmvQq21w7Y6IwWAy+YD87Pkyn2BTm2deqRuElOGShPT/HT5FU+ ujifbNuXveGO55tofSPSAu1Ohw7IgC6zuRDRiBz+KEQN X-Google-Smtp-Source: ANB0Vda2DQXJnGeH+4orHZMgTV3nQ2I05q55Ai9b6hqKWmNU3UxstTlaF3EPUdXpF8Gc7e89nU08NSpYW9vukGGHc0k= X-Received: by 2002:a25:734a:: with SMTP id o71-v6mr930935ybc.329.1537493140886; Thu, 20 Sep 2018 18:25:40 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Arlen Cox Date: Thu, 20 Sep 2018 21:25:29 -0400 Message-ID: To: garrigue@math.nagoya-u.ac.jp Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary="00000000000081f21705765784da" Subject: Re: [Caml-list] Applicative Functor Madness Reply-To: Arlen Cox X-Loop: caml-list@inria.fr X-Sequence: 17079 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --00000000000081f21705765784da Content-Type: text/plain; charset="UTF-8" Hi Jacques, Thank you for your reply. I have some further questions inlined: > A first remark: this use of module type of is probably not a good idea in > the long term, as module type of is brittle, and its semantics could change. > Duly noted. > Do you see a problem with this version? > Not immediately. I'll have to think about what limitations that imposes on my design. It is good to know more of the rules. Are the actual rules of module equality documented somewhere in the OCaml manual? It seems like Section 8.12 documents this (at least partially): There are several restrictions on module-path: > 1. it should be of the form M0.M1...Mn (i.e. without functor > applications); > 2. inside the body of a functor, M0 should not be one of the functor > parameters; > 3. inside a recursive module definition, M0 should not be one of the > recursively defined modules. Obviously in doing this inside a functor, I violated rule #2. What I don't understand is if there are clear syntactic rules, should there not be at least a warning when the rules are violated? Second, how does your solution not still violate rule #1? Thank you very much for your help, Arlen On 2018/09/20 23:29, Arlen Cox wrote: > > > > Hi everyone, > > > > I'm having some trouble getting some code that relies heavily on > applicative functors to type check. Does anyone know what I'm doing wrong > with this? > > > > module type S = sig > > module T : Set.OrderedType > > module ST : module type of Set.Make(T) > > end > > > > module Make(T_in : Set.OrderedType) : S (* <- ERROR *) > > with module T = T_in > > and module ST = Set.Make(T_in) > > = struct > > module T = T_in > > module ST = Set.Make(T_in) > > end > > > > I get the following error message referencing the above point in the > program. > > > > Error: In this `with' constraint, the new definition of ST > > does not match its original definition in the constrained > signature: > > ... > > Type declarations do not match: > > type t = Set.Make(T_in).t > > is not included in > > type t = Set.Make(T).t > > File "set.mli", line 68, characters 4-10: Expected declaration > > File "set.mli", line 68, characters 4-10: Actual declaration > > > > It seems to me that since T = T_in, but applicative functors should make > the type of Set.Make(T) = Set.Make(T_in). Does this not work this way? > > > > Note that if I change the definition of S slightly, the same definition > of Make now type checks: > > > > module type S = sig > > module T : Set.OrderedType > > module ST : Set.S with type elt = T.t > > end > > > > This solution is undesirable because I have a number of modules whose > types would require an excessive number of "with module ... = ..." > constraints to constrain in this way. Is there a better way of getting > this to type check? > > > > Thank you, > > Arlen > > > > > > > -- Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs --00000000000081f21705765784da Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Hi Ja= cques,
Thank you for your reply.=C2=A0 I have some further questi= ons inlined:
=C2=A0
A first remark: this u= se of module type of is probably not a good idea in the long term, as modul= e type of is brittle, and its semantics could change.
= =C2=A0
Duly noted.
=C2=A0
Do you see a problem with this version?

Not immediately.=C2=A0 I'll have to think about what limitations that = imposes on my design.=C2=A0 It is good to know more of the rules.=C2=A0 Are= the actual rules of module equality documented somewhere in the OCaml manu= al?

It seems like Section 8.12 documents this (at = least partially):

There are several restrictions on module-path:
=C2=A0 1. it should be = of the form M0.M1...Mn (i.e. without functor applications);
=C2=A0 2. in= side the body of a functor, M0 should not be one of the functor parameters;=
=C2=A0 3. inside a recursive module definition, M0 should not be one of= the recursively defined modules.

Obviously in doing this inside a f= unctor, I violated rule #2.=C2=A0 What I don't understand is if there a= re clear syntactic rules, should there not be at least a warning when the r= ules are violated?=C2=A0 Second, how does your solution not still violate r= ule #1?

Thank you very much for your help,
Arlen<= /div>


On 2018/09/20 23:29, Arlen Cox wrote:
>
> Hi everyone,
>
> I'm having some trouble getting some code that relies heavily on a= pplicative functors to type check.=C2=A0 Does anyone know what I'm doin= g wrong with this?
>
> module type S =3D sig
>=C2=A0 =C2=A0module T : Set.OrderedType
>=C2=A0 =C2=A0module ST : module type of Set.Make(T)
> end
>
> module Make(T_in : Set.OrderedType) : S (* <- ERROR *)
>=C2=A0 =C2=A0with module T =3D T_in
>=C2=A0 =C2=A0 and module ST =3D Set.Make(T_in)
> =3D struct
>=C2=A0 =C2=A0module T =3D T_in
>=C2=A0 =C2=A0module ST =3D Set.Make(T_in)
> end
>
> I get the following error message referencing the above point in the p= rogram.
>
> Error: In this `with' constraint, the new definition of ST
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 does not match its original definition in t= he constrained signature:
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 ...
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Type declarations do not match:
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 type t =3D Set.Make(T_in).t
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 is not included in
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 type t =3D Set.Make(T).t
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 File "set.mli", line 68, characte= rs 4-10: Expected declaration
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 File "set.mli", line 68, characte= rs 4-10: Actual declaration
>
> It seems to me that since T =3D T_in, but applicative functors should = make the type of Set.Make(T) =3D Set.Make(T_in).=C2=A0 Does this not work t= his way?
>
> Note that if I change the definition of S slightly, the same definitio= n of Make now type checks:
>
> module type S =3D sig
>=C2=A0 =C2=A0module T : Set.OrderedType
>=C2=A0 =C2=A0module ST : Set.S with type elt =3D T.t
> end
>
> This solution is undesirable because I have a number of modules whose = types would require an excessive number of "with module ... =3D ...&qu= ot; constraints to constrain in this way.=C2=A0 Is there a better way of ge= tting this to type check?
>
> Thank you,
> Arlen
>
>


--00000000000081f21705765784da--