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 211E57EE9C for ; Thu, 1 Dec 2016 11:26:33 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dmitry.bely@gmail.com; spf=Pass smtp.mailfrom=dmitry.bely@gmail.com; spf=None smtp.helo=postmaster@mail-qt0-f170.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of dmitry.bely@gmail.com) identity=pra; client-ip=209.85.216.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dmitry.bely@gmail.com"; x-sender="dmitry.bely@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of dmitry.bely@gmail.com designates 209.85.216.170 as permitted sender) identity=mailfrom; client-ip=209.85.216.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dmitry.bely@gmail.com"; x-sender="dmitry.bely@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-qt0-f170.google.com) identity=helo; client-ip=209.85.216.170; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="dmitry.bely@gmail.com"; x-sender="postmaster@mail-qt0-f170.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ARC3PQRSp4ST4K+mnV0Hm1YHsCtpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa69YxWN2/xhgRfzUJnB7Loc0qyN4vumBTVLuczJmUtBWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6?= =?us-ascii?q?OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBu7oR/eu8ULjoduNrg9wQbVr3VVfO?= =?us-ascii?q?hb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnY?= =?us-ascii?q?UAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhS?= =?us-ascii?q?waLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUSlBAoKn?= =?us-ascii?q?b4sUDuoBO+lYpJTjqVUXsBC+CwisC/3ryjBVm3T62aM33/gkHQzAwQcuHc8BsG?= =?us-ascii?q?7Modr3OqccUe67wqrVwzrfdP5WxSvx5ZLUfhw9vf2BX7R9etfRx0k1EAPFi02d?= =?us-ascii?q?p4LgPzOUyuQNqWia5Pd9WO2xj24mqxx6rz+yyccpi4nJmpgVy1De+Spi3ok1Id?= =?us-ascii?q?25RVV0Yd6hCpRQtiWaO5FqTcMlRmFloSA3waAFt56jZCUG1ogryhrFZ/GEc4WE?= =?us-ascii?q?+AzvWPuQLDtimX5oeq6zihCv+ka60OL8TNO70FNSoypFjNbMsncN2gTW6sedS/?= =?us-ascii?q?t9+l6t2S+T1wzP8+1EL104mKjHJ5I7zb4wkZ0TsUvHHiDogkn5kKiWdkA89uip?= =?us-ascii?q?7eTofKnmq4eCO4NojgzyKKcjl8ylDegmLwQDXnKX9fm+2bH/5UH5Ra9Fjvwykq?= =?us-ascii?q?nXqpDaIsEbq7akDA9Q04Yj9wy/Dje83NsDg3YHKFJEdQmIj4jsIV7OIfT4Ae2j?= =?us-ascii?q?jFSrlTdn3+rGMaH5ApXRMnjDl6/scqpn5E5ZzAo/1NRf55NPCrEdO//zQU/wtN?= =?us-ascii?q?nADhAjKQC0wuDnCM981owEQ26PDLWZY+v8q1iNs84qIvWWdcc/tTLsY6wp4v/y?= =?us-ascii?q?l25/k1IZbIGm2JIWbDazGfEwcBbRWmblntpUSTRChQE5VuG/zQLaXA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DjAgDc+T9YhqrYVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAYFuDAeINZtoLIhiigiCDoIFhiICJoFOB0ESAQEBAQE?= =?us-ascii?q?BAQEBAQESAQEBCAsLCR0wgjMaghMIAQEBAwESEQQZARsdAQMMBgULDQICJgICI?= =?us-ascii?q?gERAQUBHBkIEgiFUIJgAQMPCJ17gTI/MotQgWwYBQEfgw0Fg18KGScNVIM0AQE?= =?us-ascii?q?BAQYBAQEBGwIGEnmFM4Rbh00RgkwBBI9vim2BeI8YkDWNeIJIEx6BEyUFgSNEE?= =?us-ascii?q?S+CaiCBazs0iUIBAQU?= X-IPAS-Result: =?us-ascii?q?A0DjAgDc+T9YhqrYVdFdHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAYFuDAeINZtoLIhiigiCDoIFhiICJoFOB0ESAQEBAQEBAQEBAQESAQEBC?= =?us-ascii?q?AsLCR0wgjMaghMIAQEBAwESEQQZARsdAQMMBgULDQICJgICIgERAQUBHBkIEgi?= =?us-ascii?q?FUIJgAQMPCJ17gTI/MotQgWwYBQEfgw0Fg18KGScNVIM0AQEBAQYBAQEBGwIGE?= =?us-ascii?q?nmFM4Rbh00RgkwBBI9vim2BeI8YkDWNeIJIEx6BEyUFgSNEES+CaiCBazs0iUI?= =?us-ascii?q?BAQU?= X-IronPort-AV: E=Sophos;i="5.33,724,1477954800"; d="scan'208";a="202444323" Received: from mail-qt0-f170.google.com ([209.85.216.170]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 01 Dec 2016 11:26:32 +0100 Received: by mail-qt0-f170.google.com with SMTP id p16so215245453qta.0 for ; Thu, 01 Dec 2016 02:26:32 -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:cc; bh=RLPoVa91x9GgGh1HSF3JbPJyZhJGMcPtvMW4aUWd/YI=; b=pGd9vlxVwCy+tfHfEHAAVmI8yOYXV9HfbVQRAN3n1aBkcfTHNJegzqHh1R/+6gd9BD Lyi2a5viw1xUburtbtLzR6EY0eGzbbQt1e89I4fqjzAdr1ErQCdJLQKrO+Yrnl1i+20K 6Zt5dHo+UBC6JH2E9PGcceDWCGWT4zevO+5BcbMPNrX+8q646mnJOWsNU7GIhtzYPSBx Qt99m0XIIprykvB3mc2LHzGoYKTzeUHJ/9EcSwRUJPNbJouZNjrEnU8/61cY26GaNjNd MQwBwblUVO3kma3UfRfX/P2Wym+b7vvH9XH5379crIbx/UYcY0jp98T6sGRnOyyV0PUG 5IVA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:cc; bh=RLPoVa91x9GgGh1HSF3JbPJyZhJGMcPtvMW4aUWd/YI=; b=QGFy6uqe1MUp3DHJhbSlqAfGEIGXoksvjugDGpSSl+CCbd/iieeGhxTPr91hsEn+75 BjoJTqRv5R2HBha1WsCYYsFmBU3nGUmOP/qXxGm0pI+qiaX44lbhdsyZjGH86RoJlFLW VnJm3bS7xMcLB/QR7d/qcylqor3MbFlkXZbvTcbT56DV6VC8zuPxwczjLleHtAGnbS9X EIIv7TW4losikKDzH5e4sjV5Bf/AudK1m5cJY144jA5VEEnLcUqwXJIxuDee1ESvT/33 Wn/VGxDibGX3j3q1irbso0Mk2BOa36PaETzcnYHDmqSA+9MU5cEtvF80QSz6nXjwBWQ2 naYQ== X-Gm-Message-State: AKaTC03bhJCRBtwWFggyswpPxGZHZe7ZTJiQNSuSBgDwWmVmeFBHhWLsmQyUkK8JZM+FNyqS/z4ctovsg8VLDw== X-Received: by 10.237.42.65 with SMTP id k1mr32545857qtf.210.1480587990689; Thu, 01 Dec 2016 02:26:30 -0800 (PST) MIME-Version: 1.0 Received: by 10.12.173.164 with HTTP; Thu, 1 Dec 2016 02:26:30 -0800 (PST) In-Reply-To: References: From: Dmitry Bely Date: Thu, 1 Dec 2016 13:26:30 +0300 Message-ID: Cc: Caml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] GADT memory representation On Thu, Dec 1, 2016 at 12:52 PM, 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. Thanks a lot for your explanation. Let me ask another dumb question regarding GADTs. What should I do to make the following code typecheck? type sum = Int_ of int | Float_ of float;; type _ gadt = Int : int -> int gadt | Float : float -> float gadt;; let convert (type el) v : el gadt = match v with Int_ i -> Int i | Float_ f -> Float f;; Characters 61-66: let convert (type el) v : el gadt = match v with Int_ i -> Int i | Float_ f -> Float f;; ^^^^^ Error: This expression has type int gadt but an expression was expected of type el gadt Type int is not compatible with type el >> Unfortunately OCaml manual doesn't even mention GADTs in section >> "Interfacing C with OCaml". > > That's worth a GPR/Mantis issue. Yes, I'll submit one. - Dmitry Bely