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 EA53C7F0B9 for ; Fri, 26 Aug 2016 00:36:06 +0200 (CEST) IronPort-PHdr: 9a23:zvlSwByc9SXw06jXCy+O+j09IxM/srCxBDY+r6Qd0e8fIJqq85mqBkHD//Il1AaPBtSCrakVwLON++C4ACpbsM7H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpqsSVOFQD3WH1Iesrak7n9UOJ7oheqLAhA5558gHOrHpMdrYe7kJTDnXXoSzB4Nyt9oVo6SVatqFp3cdBVaLnY/ZwFuQAX3x1e1wyscbisB2GSQqU+lMdVH8Xm1xGGVvr9hb/C7j8qCeyjfZ63DGfNMvwBeQ1Xzqlx6hmUhOtkzsAMyY8+WfRzMB92vEI6Cm9rgByltaHKLqeM+BzK/vQ Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=info@gerd-stolpmann.de; spf=None smtp.mailfrom=info@gerd-stolpmann.de; spf=None smtp.helo=postmaster@mout.kundenserver.de Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=pra; client-ip=212.227.126.130; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=mailfrom; client-ip=212.227.126.130; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.kundenserver.de) identity=helo; client-ip=212.227.126.130; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="postmaster@mout.kundenserver.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A5AQCKcb9Xh4J+49RdSYJ4AQEBAQF0fLghgX8ghX0CgWE4FAEBAQEBAQEBAQEBEgEBAQgNCQkZL4IyGIIYAQEEJy40C0ZXGQmILQEJwBMBAQEHAhcOhTaFRYRMQIUQBYgsi1eFR4E/Apc8hXuMQYN5HoJsgVluAYZLAQEB X-IPAS-Result: A0A5AQCKcb9Xh4J+49RdSYJ4AQEBAQF0fLghgX8ghX0CgWE4FAEBAQEBAQEBAQEBEgEBAQgNCQkZL4IyGIIYAQEEJy40C0ZXGQmILQEJwBMBAQEHAhcOhTaFRYRMQIUQBYgsi1eFR4E/Apc8hXuMQYN5HoJsgVluAYZLAQEB X-IronPort-AV: E=Sophos;i="5.28,578,1464645600"; d="asc'?scan'208";a="191116766" Received: from mout.kundenserver.de ([212.227.126.130]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 26 Aug 2016 00:36:06 +0200 Received: from office1.lan.sumadev.de ([89.12.41.209]) by mrelayeu.kundenserver.de (mreue003) with ESMTPSA (Nemesis) id 0MK5c9-1bbgLA1Rht-001S0p for ; Fri, 26 Aug 2016 00:36:05 +0200 Received: from e130 (unknown [192.168.65.10]) by office1.lan.sumadev.de (Postfix) with ESMTPSA id B3433DC05D for ; Fri, 26 Aug 2016 00:36:04 +0200 (CEST) Message-ID: <1472164554.6898.13.camel@gerd-stolpmann.de> From: Gerd Stolpmann To: caml-list@inria.fr Date: Fri, 26 Aug 2016 00:35:54 +0200 In-Reply-To: <1472164400.6898.12.camel@gerd-stolpmann.de> References: <1472164400.6898.12.camel@gerd-stolpmann.de> Content-Type: multipart/signed; micalg="pgp-sha256"; protocol="application/pgp-signature"; boundary="=-BF8VfizqXPMAUWzDUBKw" X-Mailer: Evolution 3.18.5.2-0ubuntu3 Mime-Version: 1.0 X-Provags-ID: V03:K0:w6avkQifj9we8p/S/2Wh9NSNntvj/L0juMZeW5aJeMh3fNUuS0w EfK8+4YYL/NKH9CrkXD1s8er+0jCOE6vkg9CuNipU5pVo9sMvSKBbsOOvdmixpIhNbAw27f F1DgY2ypI8SfodniZcdHuJZCZcr4kKIbvt6e7KeKya2r6H5VGWEIQar53XZeynygpB8D9/N AhJFAvwFDr345sitWlvsg== X-UI-Out-Filterresults: notjunk:1;V01:K0:LN5p0QaRwFA=:g3fdG3yqsT2ui+z6UtPpAz BANwMC/VRb4qMEKmhCd9NPSGWiwpffBrZJbg9rhxpB/8LGN9MWf58Ys0Wr4ktTSmN8DCd/VPT 08CNSAEFRzENndDzFFcrRFOAseyNnW9+9K8FbBzOzMBoV8MZ55FAUHP12R3mkwNrxeGyJWv+R ph3PQ7/7mteb3d3HULk3WFZqpWERwxod1DLjZgfzGGaI//lm8+n8mnXk5abPGhqNT3scMzJtR 76ev6OjloSITRTdEKLvaRFpyptCoohmd7AuKiX3UUxddS2gbgiV16xn7Ee5yMw3XAvv7qyhDT qmt/azg6H4XxHjCGtfS0RXfqUV7mFofypauYqv2iE3xAPB4NGc27aX8JSD2rLkCjTrioSrWYo nQ/kNbUm+hzml7HJUZiKY4Lg+Bnohtxq3XD6GHOZ4sLtH+zBBrYThoVEHeJNpL/YwT8rwlDqN Qo0iP9KDonmE7oraSW4aS6GKwiiLd3i1VJXSm+vOMLT7F4I4xllENnmrDyKnFxEXemaNKYDDn ZgqH3Vkf5oM08bDS/EpckjRTXoHApFI76UC9CXWxWBPBmmjNV/CVDsf/WaPUk9gICNtQizxlq 0qN9cNcmNByb+6nqueSyfQsGpxdCtkVvFiPUkBdKGP7PGeg3W1qkpZBhhyWFBMGR13QlbJAPD LXDj3iPPa4tFPVC7JvQSgGhN/+eGc6clFV+kw2L6Q3fuNc0phikKgU8lUxG88adFjciQ= Subject: Re: [Caml-list] isn't this cheating? --=-BF8VfizqXPMAUWzDUBKw Content-Type: text/plain; charset="ISO-8859-15" Content-Transfer-Encoding: quoted-printable Forget this message. Gerd Am Freitag, den 26.08.2016, 00:33 +0200 schrieb Gerd Stolpmann: > Hi, >=20 > just fixing up some GADT code. I came across this: >=20 > I have a module M with module type T: >=20 > module type T =3D sig > =A0 type p > =A0=A0val p_type : p Ztypes.ztype > =A0=A0val output : float -> p > end >=20 > Now, Ztypes.ztype is a GADT like >=20 > type _ ztype =3D > =A0 | Zstring : string ztype > =A0 | Zfloat : float ztype > =A0 | ... >=20 > In a function calling M.output I cannot assume that p=3Dfloat unless I > check it explicitly. So I wrote >=20 > let f() =3D > =A0 let m_output =3D > =A0=A0=A0=A0match M.p_type with > =A0=A0=A0=A0=A0=A0| Ztypes.Zfloat -> (M.output : float -> float) > =A0=A0=A0=A0=A0=A0| _ -> assert false in > =A0... >=20 > This doesn't type-check. Funnily, you can fix it by simply adding a > newtype to the function: >=20 > let f : type t =3D fun() -> > =A0 let m_output =3D > =A0=A0=A0=A0match M.p_type with > =A0=A0=A0=A0=A0=A0| > Ztypes.Zfloat -> (M.output : float -> float) > =A0=A0=A0=A0=A0=A0| _ -> assert false > in > =A0... >=20 > It is just the presence of t that makes it type-check. This type is > not in any way bound to the type parameter of ztype, and this is > somewhat unexpected. From a user's perspective it is very comfy that > the newtype works like a configuration switch for the type checker. > Nevertheless, I wonder why it is like that. >=20 > Gerd --=20 ------------------------------------------------------------ Gerd Stolpmann, Darmstadt, Germany gerd@gerd-stolpmann.de My OCaml site: http://www.camlcity.org Contact details: http://www.camlcity.org/contact.html Company homepage: http://www.gerd-stolpmann.de ------------------------------------------------------------ --=-BF8VfizqXPMAUWzDUBKw Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQEcBAABCAAGBQJXv3LKAAoJEAaM4b9ZLB5TyQIIAIlAdH8wvut8Fhe7XKijyjS2 cUSBvBFuSSreFEenXQokSPXT5+kpo6GqVxpBFyeHEsA4MAr47WrQVXMv8d7qD7Rd OIUyIHSXqnFR36ZWfDM5U1v/vVozdwZLX4pwsE39EBqIQQ6cTgRQ9UQnPuIbeqgJ /lmogax7Gg2IERN6Qydrtzz+aZ+5nWX28sVo7ZIpi2uz6F0i22vch9QI5Oz6RKET 5YdgljhyfxNs+/eVLFQxCb19iJ62eEp+neGaXpAW9CIPsDWLpLG3Zwl4RGbemj4b 5a8gw+I3T/TZAMEPLwlEwv/zYhvOmFZZdLSjE5ZW17R6nSlIW9P6rduWYxoQhVk= =DFmh -----END PGP SIGNATURE----- --=-BF8VfizqXPMAUWzDUBKw--