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 sympa.inria.fr (Postfix) with ESMTPS id 67A9C7FD1D for ; Thu, 5 Nov 2015 04:22:30 +0100 (CET) IronPort-PHdr: 9a23:iIIxRRNgx1exwD9d9l0l6mtUPXoX/o7sNwtQ0KIMzox0KPX6rarrMEGX3/hxlliBBdydsKIZzbGP+P27EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35nxjLn5psabSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzhRACW+3YHGkofiABJDBXIpEX1V43rsyTnu8J40TWae8v/QrclUHG/qa5gDh3w3nQpLTk8pUjMis1rjOpyrxu7uBV7i9rdb4iPK/N6J/KCIPsVQGNAWoBaUCkXUdD0VJcGE+dUZbUQlIL6vVZb6ELmXQQ= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=agarwal1975@gmail.com; spf=Pass smtp.mailfrom=agarwal1975@gmail.com; spf=None smtp.helo=postmaster@mail-wi0-f175.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of agarwal1975@gmail.com) identity=pra; client-ip=209.85.212.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of agarwal1975@gmail.com designates 209.85.212.175 as permitted sender) identity=mailfrom; client-ip=209.85.212.175; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f175.google.com) identity=helo; client-ip=209.85.212.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="postmaster@mail-wi0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C6AQB8yjpWm6/UVdFeDoNMNG8Gs2GMAhmFeQKBOgc7EQEBAQEBAQEBEAEBAQEBBgsLCSEugi6CCAEBBBIRBBkBGx0BAwwGBQQHNwICIgERAQUBHAYTIod2AQMSoxyBMT4xi0iBaoJ5hnwKGScNVoNmAQEBAQEFAQEBAQEBARYBBQ6LRId1gUMFjhGIMAeFHYgGmnQSJIEXESaCMCOBH1wgNIUfAQEB X-IPAS-Result: A0C6AQB8yjpWm6/UVdFeDoNMNG8Gs2GMAhmFeQKBOgc7EQEBAQEBAQEBEAEBAQEBBgsLCSEugi6CCAEBBBIRBBkBGx0BAwwGBQQHNwICIgERAQUBHAYTIod2AQMSoxyBMT4xi0iBaoJ5hnwKGScNVoNmAQEBAQEFAQEBAQEBARYBBQ6LRId1gUMFjhGIMAeFHYgGmnQSJIEXESaCMCOBH1wgNIUfAQEB X-IronPort-AV: E=Sophos;i="5.20,246,1444687200"; d="scan'208";a="186124324" Received: from mail-wi0-f175.google.com ([209.85.212.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 05 Nov 2015 04:22:29 +0100 Received: by wicll6 with SMTP id ll6so1582752wic.0 for ; Wed, 04 Nov 2015 19:22:29 -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=0uAwbipB70pUv+JV4qs0CUT3auL+B95PHOTgDQJJdT0=; b=GsJ5Fs/HZzZ65ypMYP2tnTucl0oN9xx7WkB/vrm02RwRqmMuBGzI/+31Bcmaa52jFT RwVQdVwUkf4XBZ26YdldKhg/gGjFv9BN7KKyZ5DxzVPD3FwO2zYvJuC+nDwhMHRQrD8I wshtkUofpTTAwNbSHrHwzKVl4zTiGCJ7mYw8Q/XwDhamPMAdJGUJZDGgLwsXAbSVSa3W 6MQWa7BBX+K2qhuh8JBeYG7KCQFBPAKlTiyQD49JHx/5fHH0UdJr0YwJYStE0YGUzFrL kD/pS2fShep7Qrq64Usov4JpDuVA4QoVKBXqwz4wqiWvJpljYbeNsJVQuILr+ndiU7wr pxgg== X-Received: by 10.194.114.70 with SMTP id je6mr5397308wjb.7.1446693749336; Wed, 04 Nov 2015 19:22:29 -0800 (PST) MIME-Version: 1.0 Received: by 10.27.82.65 with HTTP; Wed, 4 Nov 2015 19:22:09 -0800 (PST) In-Reply-To: References: From: Ashish Agarwal Date: Wed, 4 Nov 2015 22:22:09 -0500 Message-ID: To: Jacques Garrigue Cc: OCaml Mailing List Content-Type: multipart/alternative; boundary=001a1130d288072fe90523c2a34b Subject: Re: [Caml-list] substituting recursive types inside a signature --001a1130d288072fe90523c2a34b Content-Type: text/plain; charset=UTF-8 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 --001a1130d288072fe90523c2a34b Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On W= ed, Nov 4, 2015 at 9:10 PM, Jacques Garrigue <garrigue@math.na= goya-u.ac.jp> wrote:

the c= ode you wrote is exactly equivalent to:

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

And the parentheses here don&#= 39;t matter right, so this is the same as:

in= clude 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 around this, at the expense of some = manual typing. Here's what works:

$ cat <= a href=3D"http://foo.ml">foo.ml
module M =3D struct
=C2=A0 type t =3D A | B of u
=C2=A0 and u =3D C of t
e= nd

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

--001a1130d288072fe90523c2a34b--