From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 CDF2C7EE9C for ; Thu, 1 Dec 2016 15:12:23 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=octa@polychoron.fr; spf=None smtp.mailfrom=octa@polychoron.fr; spf=None smtp.helo=postmaster@relay3-d.mail.gandi.net Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=pra; client-ip=217.70.183.195; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of octa@polychoron.fr) identity=mailfrom; client-ip=217.70.183.195; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="octa@polychoron.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@relay3-d.mail.gandi.net) identity=helo; client-ip=217.70.183.195; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="octa@polychoron.fr"; x-sender="postmaster@relay3-d.mail.gandi.net"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Az6ZIjx/4wYWUcv9uRHKM819IXTAuvvDOBiVQ1KB4?= =?us-ascii?q?0eocTK2v8tzYMVDF4r011RmSDN6dt6sP0LCempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgpp?= =?us-ascii?q?POT1HZPZg9iq2+yo9ZDeZwtFiCCybL9vIxm7oxvdvdQKjIV/Lao81gHHqWZSde?= =?us-ascii?q?RMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZ?= =?us-ascii?q?TQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhz?= =?us-ascii?q?odNzMh7W/ZlMJwgqJYrhyvqRNwzIzbb52aOvdlYqPQfskXSXZdUstfVSFMBJ63?= =?us-ascii?q?YYsVD+oGOOZVt479qEcSrRSkGQasBPnvyjhOhnTr2qA61PguER3c0wE7B9IOt3?= =?us-ascii?q?DUrdXpO6cSVuC11q7IzTPZY/NYwzfw8Y7FeQ0ir/GURb98b9fdxEs1Gw7Hklmc?= =?us-ascii?q?s5HpMjCb2+gXrmSW6+ptWfqyh2MjpAx9uDiiy8U2hoXXiY8YyErI+Ct/zY0oP9?= =?us-ascii?q?O3UlR7bsShEJZItyGVKY92QsQ6TmFypik6zqcJuJ61cSQT1Zsr3RvfZOaGc4iM?= =?us-ascii?q?+B7jW/yeITFli3JkYr6/gQi98VS4xu39UMm7zkpKozJbntXRtH0BzR7e5tSdRv?= =?us-ascii?q?dg/Uqs1yyD2x3X5+xEOUw0kLDUK58lwr4+jJoTtkHDEzfxmErqkK+ZbF4p+vCv?= =?us-ascii?q?6+TjYrTpup+cN4huigH5NKQigMK/Af4gPggUQ2eb4fi81KHk/UDhXLpFlPg2kq?= =?us-ascii?q?3AvJDeJMQbvbK5DhRO0ocj7ha/Fy2p3M4ZnXkBNlJFeQiIg5LnO1HUc7jECqK0?= =?us-ascii?q?ilGo1TNq3OzuP7v7A5yLIGKQvq3meON64FJVwwopytYXs5VfFrgpOPX3S0Txs8?= =?us-ascii?q?bfCFk3KVrnkK7cFNxh29ZGCiq0CaiDPfaKvA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B1AADhLkBYh8O3RtldHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAYElXwGkSJJqhBOGIgKCB0MQAQEBAQEBAQEBAQESAQE?= =?us-ascii?q?BCgsJCR0wgjMYgh4BAQQjBAsBBVELGAICJgICVxMIAQGIbas6gWw9jAKBC4Uyg?= =?us-ascii?q?X6CXoUVgjiCXQWaXmWBZZhRhiuNeoQKAjWBOSODSoFpiScBgQwBAQE?= X-IPAS-Result: =?us-ascii?q?A0B1AADhLkBYh8O3RtldHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAYElXwGkSJJqhBOGIgKCB0MQAQEBAQEBAQEBAQESAQEBCgsJCR0wgjMYg?= =?us-ascii?q?h4BAQQjBAsBBVELGAICJgICVxMIAQGIbas6gWw9jAKBC4UygX6CXoUVgjiCXQW?= =?us-ascii?q?aXmWBZZhRhiuNeoQKAjWBOSODSoFpiScBgQwBAQE?= X-IronPort-AV: E=Sophos;i="5.33,282,1477954800"; d="scan'208";a="202480444" Received: from relay3-d.mail.gandi.net ([217.70.183.195]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 01 Dec 2016 15:12:23 +0100 Received: from mfilter11-d.gandi.net (mfilter11-d.gandi.net [217.70.178.131]) by relay3-d.mail.gandi.net (Postfix) with ESMTP id 7535BA8141 for ; Thu, 1 Dec 2016 15:12:22 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at mfilter11-d.gandi.net Received: from relay3-d.mail.gandi.net ([IPv6:::ffff:217.70.183.195]) by mfilter11-d.gandi.net (mfilter11-d.gandi.net [::ffff:10.0.15.180]) (amavisd-new, port 10024) with ESMTP id huB9JitcfLXs for ; Thu, 1 Dec 2016 15:12:21 +0100 (CET) X-Originating-IP: 194.57.247.3 Received: from [172.22.8.14] (fw.enpc.fr [194.57.247.3]) (Authenticated sender: octa@polychoron.fr) by relay3-d.mail.gandi.net (Postfix) with ESMTPSA id 06CA4A8135 for ; Thu, 1 Dec 2016 15:12:20 +0100 (CET) To: caml-list@inria.fr References: <3f89d13a-14f0-090b-be96-d3f67fcb95f3@lexifi.com> From: octachron Message-ID: Date: Thu, 1 Dec 2016 15:12:19 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.5.0 MIME-Version: 1.0 In-Reply-To: <3f89d13a-14f0-090b-be96-d3f67fcb95f3@lexifi.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] GADT memory representation I would tend to think that it would be nicer to document this memory layout − with all necessary caveats embedded in the documentation itself − rather than hide away the documentation due to the potentiality of a change in an unknown future. − octachron. On 01/12/16 à 12:51, Alain Frisch wrote: > On 01/12/2016 10:52, David Allsopp wrote: >> Dmitry Bely wrote: >>> I need to access/modify GADT data from C glue code. What is their >>> memory >>> representation? Is there any difference from ordinary sum types? >> >> It's the same - GADTs are "just" add a lot of clever typing stuff on >> top of a normal sum type - they don't affect the runtime operation of >> the code. >> >>> Unfortunately OCaml manual doesn't even mention GADTs in section >>> "Interfacing C with OCaml". >> >> That's worth a GPR/Mantis issue. > > I'm not sure we want to document the memory layout of GADTs. I don't > think there are concrete plans to do so, but it might be considered to > change the representation of GADTs so that they cannot be used to > compare values of different types with the polymorphic comparison > function. Today you can write: > > type t = E: 'a -> t > > let () = assert(E 1 = E true) > > A similar "bad" behavior used to be available for exceptions and this > was "fixed" by changing their representation (their "slot" now has > object_tag and a (per process) unique id). We might want to do the > same for GADTs (not an easy decision since it would add a lot of > overhead) and for first-class modules as well. > > > Alain >