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 0ED787F0B9 for ; Fri, 26 Aug 2016 00:33:33 +0200 (CEST) IronPort-PHdr: 9a23:vNXz0B2Rfa9lANR3smDT+DRfVm0co7zxezQtwd8ZsegTI/ad9pjvdHbS+e9qxAeQG96KsrQf2qGP6OigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV4Zz2PmKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduYCgJ45jgvBzHCA+O/Wc0U2MMkxMODRKWwgv9W8LevzH2/tFh3y2COMTwS/hgWDKs6I9kRQXkzTwbMDoh9WjRjIp8gfQI81qauxVjztuMM8muP/1kc/aFcA== 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.135; 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.135; 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.135; 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: A0AIAgCKcb9Xbod+49RdKxiCfgEBAQEBHlZ8uCGBfyCHYDgUAQEBAQEBAQEBAQESCwsLCQsOL4IyGIJFLoF1CYgtAQmgVp9gDoU2ilGBfguDBwWILJEegT8ClzyFe5A6HoRFbgGGSwEBAQ X-IPAS-Result: A0AIAgCKcb9Xbod+49RdKxiCfgEBAQEBHlZ8uCGBfyCHYDgUAQEBAQEBAQEBAQESCwsLCQsOL4IyGIJFLoF1CYgtAQmgVp9gDoU2ilGBfguDBwWILJEegT8ClzyFe5A6HoRFbgGGSwEBAQ X-IronPort-AV: E=Sophos;i="5.28,578,1464645600"; d="asc'?scan'208";a="191116597" Received: from mout.kundenserver.de ([212.227.126.135]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 26 Aug 2016 00:33:32 +0200 Received: from office1.lan.sumadev.de ([89.12.41.209]) by mrelayeu.kundenserver.de (mreue004) with ESMTPSA (Nemesis) id 0LeyNP-1amcx21N9z-00qfUB for ; Fri, 26 Aug 2016 00:33:31 +0200 Received: from e130 (unknown [192.168.65.10]) by office1.lan.sumadev.de (Postfix) with ESMTPSA id AC4C4DC05D for ; Fri, 26 Aug 2016 00:33:30 +0200 (CEST) Message-ID: <1472164400.6898.12.camel@gerd-stolpmann.de> From: Gerd Stolpmann To: caml-list@inria.fr Date: Fri, 26 Aug 2016 00:33:20 +0200 Content-Type: multipart/signed; micalg="pgp-sha256"; protocol="application/pgp-signature"; boundary="=-MYDhUBD2xjSQOcJjNtff" X-Mailer: Evolution 3.18.5.2-0ubuntu3 Mime-Version: 1.0 X-Provags-ID: V03:K0:ZsVWGEt3GlSWNiMUGwrFYVDi2SVHKpr+QB9xy3w/ohphZOxPyRf 9O67aTDH668cwyl7f3PdD6EjcuBaZWQSd44jYwTKUwdqqP5ZBSprUoB85kFKgO3JDrhSRav nN02j2V+fr1Jq7nTklU650O86bGHuf/4CHiozm4IiTHa6vUarVhCOZ6zCR2CthyJVdyzpXC 3DSZN3VurcKvMEDK4+AEQ== X-UI-Out-Filterresults: notjunk:1;V01:K0:U4KH2l6pbxY=:wEyF/nkw/ir1IgFWAk7+CV Wf23bEyoz4ka1eneUKABA+ISBlZ0RAZloYzBVQ+2g2Ww8f8MmTXgEK7le2/Q7dnCdlDILeJBk 9M87tFY+b89f7y+D2BuQoNlMknec4hjkQhFPbv5AXQ0bVaNrdozmgdty+0KdlvhH7jZZXTBME 8yA0xN+3iCb3sBAmqnwdY7m5uWsHaQYf1GY2MQq82Ihg8sbiq5Ac5pu2z8NDx0HW6xc8jTNIZ pXjsu4TBLiDIsKet48bd4v87AFXu2qRKwFg78u79JtMZwG3i8Fq48VOZTupOI9PK+p4jO+joq n6Hms04fCckV6VlxZrP6ChIER0Y7+JfllKEsNjB9L/CAIUpVHg+nthNoA3RUFN+8rKxM9su+I mgUb+ToDBijHe/hYwV0V+k3HJuo7rprunGysxJ+++S6t1uWBGtiO/xZzx66v2njzp4IwOUSnx EgN6qfgP1sRwy/WGqgTxM33F7+UBfs/fyzovfejGsF76l7C8RbIS0yxgv2A8ZWVuScTn7krzY 5yJQ3z/6/DE9EIAgEpBwn2MrQXCZkdfithFLmiSeB8BvxJu6j+C9rGq9O41NvW6dPA02g0uFj 1uxZT1JKwvWVMD0QEmTe5ByXk/4VKCnwEoK8CNzKDEqChrziX8yTxKzWo2x1XUQ91MzWfSgYH A1jyUJBHu+7S7VlD/JwBWA4wN1PmTs4+PmXXY0nL/AFhocKVv6lvCBeX36gULahWRUBY= Subject: [Caml-list] isn't this cheating? --=-MYDhUBD2xjSQOcJjNtff Content-Type: text/plain; charset="ISO-8859-15" Content-Transfer-Encoding: quoted-printable Hi, just fixing up some GADT code. I came across this: I have a module M with module type T: module type T =3D sig =A0 type p =A0=A0val p_type : p Ztypes.ztype =A0=A0val output : float -> p end Now, Ztypes.ztype is a GADT like type _ ztype =3D =A0 | Zstring : string ztype =A0 | Zfloat : float ztype =A0 | ... In a function calling M.output I cannot assume that p=3Dfloat unless I check it explicitly. So I wrote 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... This doesn't type-check. Funnily, you can fix it by simply adding a newtype to the function: 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... 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 unexpect= ed. 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. 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 ------------------------------------------------------------ --=-MYDhUBD2xjSQOcJjNtff 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 iQEcBAABCAAGBQJXv3IwAAoJEAaM4b9ZLB5TjzkH/j+VUbUrk8YMCq8pUXRvX7RU bY75M3JfS0ptr31Ax9XDLgFPkgVeYudT6jyaQA9FaqwysJgrBe1tC5xJbvfYWVxY 2Qonv3fqauE2kbyvHVOKm4myTbXKD+hXfmpt5npKlHr5R1L1y7qm61bufF+UJu67 opNqIz8W5ewUeXjU15OsoTAjJLfgJ8oEgrp926Jz9fxuI28rg26y8yR5Yo1CIm79 GlO7CpvO0aEhMzTLBsFLgREMgWBd/2U+ScfXonkatsN/yhE/9y5bRngIFAjfLtQC LB/nvfeDdF19QsibeVoSJ0DTK0iBXdYgvQ0/5isICzDWY5XroEqmohNqKhILyG4= =e22T -----END PGP SIGNATURE----- --=-MYDhUBD2xjSQOcJjNtff--