From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 9BB407FD1E for ; Thu, 5 Nov 2015 04:24:48 +0100 (CET) IronPort-PHdr: 9a23:BdGbYBQwF0aY2IxmMmwRvC/vCdpsv+yvbD5Q0YIujvd0So/mwa64bRWN2/xhgRfzUJnB7Loc0qyN4/2mAjVLvM3JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviptuIOk4V33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1kVWXwLnwEALAHf9hD1Q5q55iTzrPB81zSXFcj/UbByXz2t6LZiDQKugSxBNSZvo0/NjcklpblboQmh7zVwypTLaYXdYPNxd7nCdNdDFDUcdslUXi1FRIi7at1cXKI6Ie9Eotyl9BM1phykCFzpXbu3xw== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agarwal1975@gmail.com; spf=Pass smtp.mailfrom=agarwal1975@gmail.com; spf=None smtp.helo=postmaster@mail-wm0-f51.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of agarwal1975@gmail.com) identity=pra; client-ip=74.125.82.51; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of agarwal1975@gmail.com designates 74.125.82.51 as permitted sender) identity=mailfrom; client-ip=74.125.82.51; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wm0-f51.google.com) identity=helo; client-ip=74.125.82.51; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="postmaster@mail-wm0-f51.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CgAQCjyzpWlDNSfUpeDoNMNG8GrGSRIYFeGYV5AoE6BzoSAQEBAQEBAQEQAQEBAQcLCwkfMIIugggBAQQSEQQZARsdAQMBCwYFBAcNKgICIQEBEQEFARwGEyKHdgEDEqMegTE+MYtIgWqCeYZ8ChknDVaDZgEBAQEBBQEBAQEBAQEWAQUOi0SCU4UigUMFjhGIMAeFHYYSgXSUb4YFEiSBFxEXAoI9I4EfXCA0hR8BAQE X-IPAS-Result: A0CgAQCjyzpWlDNSfUpeDoNMNG8GrGSRIYFeGYV5AoE6BzoSAQEBAQEBAQEQAQEBAQcLCwkfMIIugggBAQQSEQQZARsdAQMBCwYFBAcNKgICIQEBEQEFARwGEyKHdgEDEqMegTE+MYtIgWqCeYZ8ChknDVaDZgEBAQEBBQEBAQEBAQEWAQUOi0SCU4UigUMFjhGIMAeFHYYSgXSUb4YFEiSBFxEXAoI9I4EfXCA0hR8BAQE X-IronPort-AV: E=Sophos;i="5.20,246,1444687200"; d="scan'208";a="152693361" Received: from mail-wm0-f51.google.com ([74.125.82.51]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 05 Nov 2015 04:24:22 +0100 Received: by wmeg8 with SMTP id g8so2881007wme.0 for ; Wed, 04 Nov 2015 19:24:21 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=qLtTY0YWD63B+yvqAZfKf4XUw1alRTWCZ8C2m64RxrA=; b=H3L4g1ouw5mxo3E6BRHZkb68qWdrYgirlLN6JDKdoxtn1Iz4UcuGMAGUTcw8onkQVc Mw8FbfLToW5Ns3agsb3iodiRLv9vSC72iweO1MSyn43SoE1glbpNKfe/3fwfUN61EUJd HfUk5tK38HwC/1GoipbuzwgNM/1mrVU3l/ItmR/nkwRCYPJpKVQ/Pwewdg1L/wSEQBE0 IBWzf2tsNc80pPonEswyX/q+lqDJ6R4jKhxZr055cTqVjrM4HyLKa70QPIAGsnCgWSSc El7nD07wAqr97dGR2XugYO6E7uD4rF5y4VsGxRXbr4V/80YCUJzS5Z/y9lWnfVtrwgI5 WKwA== X-Received: by 10.28.15.136 with SMTP id 130mr655495wmp.36.1446693861842; Wed, 04 Nov 2015 19:24:21 -0800 (PST) MIME-Version: 1.0 Received: by 10.27.82.65 with HTTP; Wed, 4 Nov 2015 19:24:02 -0800 (PST) In-Reply-To: References: From: Ashish Agarwal Date: Wed, 4 Nov 2015 22:24:02 -0500 Message-ID: To: Jacques Garrigue Cc: OCaml Mailing List Content-Type: multipart/alternative; boundary=001a1145b006bc04df0523c2a9c5 Subject: Re: [Caml-list] substituting recursive types inside a signature --001a1145b006bc04df0523c2a9c5 Content-Type: text/plain; charset=UTF-8 I pasted the wrong code. Slightly less typing is possible by doing "include M" in N's implementation. On Wed, Nov 4, 2015 at 10:22 PM, Ashish Agarwal wrote: > On Wed, Nov 4, 2015 at 9:10 PM, Jacques Garrigue < > garrigue@math.nagoya-u.ac.jp> wrote: > > the code you wrote is exactly equivalent to: >> >> include (((module type of M) with type t = M.t) with type u = M.u) >> > > And the parentheses here don't matter right, so this is the same as: > > include module type of M > with type t = M.t > with type u = M.u > > So then why do we have the "and" syntax at all? > > Well, I can use manifest types to work around this, at the expense of some > manual typing. Here's what works: > > $ cat foo.ml > module M = struct > type t = A | B of u > and u = C of t > end > > module N : sig > type t = M.t = A | B of u > and u = M.u = C of t > val f : t -> t > end = struct > type t = M.t = A | B of u > and u = M.u = C of t > let f x = x > end > > let x : M.t = M.A > let _ = N.f x > > --001a1145b006bc04df0523c2a9c5 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I pasted the wrong code. Slightly less typing is possible = by doing "include M" in N's implementation.

On Wed, Nov 4, 2015 at 10:2= 2 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:
<= blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px= #ccc solid;padding-left:1ex">
<= div class=3D"gmail_quote">On Wed, Nov 4, 2015 at 9:10 PM, = Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> w= rote:

the code you wrote is exactly equi= valent to:

=C2=A0 =C2=A0include (((module type of M) with type t =3D M.t) with type u = =3D M.u)

And the parentheses her= e don't matter right, so this is the same as:

=
include module type of M
=C2=A0 =C2=A0 with= type t =3D M.t
=C2=A0 =C2=A0 with type u =3D M.u

So then why do we have the "and" syntax at= all?

Well, I can use manifest types to work aroun= d this, at the expense of some manual typing. Here's what works:
<= div>
$ cat foo.ml
module M =3D struct
=C2=A0 t= ype t =3D A | B of u
=C2=A0 and u =3D C of t
end
<= div>
module N : sig
=C2=A0 type t =3D M.t = =3D A | B of u
=C2=A0 and u =3D M.u =3D C of t
=C2=A0 v= al f : t -> t
end =3D struct
=C2=A0 type t =3D M.t = =3D A | B of u
=C2=A0 and u =3D M.u =3D C of t
=C2=A0 l= et f x =3D x
end

let x : M.t =3D M.A
let _ =3D N.f x


--001a1145b006bc04df0523c2a9c5--