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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 556B37EE9C for ; Thu, 1 Dec 2016 15:51:39 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f181.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.181 as permitted sender) identity=mailfrom; client-ip=209.85.223.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-io0-f181.google.com) identity=helo; client-ip=209.85.223.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f181.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3As8+ItxIGQ21p7uvDANmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgUKfTxwZ3uMQTl6Ol3ixeRBMOAuqkC17Od6P2oGTRZp83e4DZaKN0EfiRGoP?= =?us-ascii?q?tVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blIt?= =?us-ascii?q?dazdU7TfhMWv1u2054abI0AR3GL8MoVJMQ6uoA7Nms4TiIpkYuZtm1qa6kdPLs?= =?us-ascii?q?hTxH9yNBq5khLtrpO8+Z9/6TUWsf8l5uZPVKz7e+IzSrkOXxo8NGVgy8ThrxjO?= =?us-ascii?q?SUO07XsRSGgM2k5HCgLf7Rz+GIz6sibgu/BV1yyTPMmwRrcxD2fxp5x3QQPl3X?= =?us-ascii?q?9UfwUy93va34kt1a8=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B9AAC+N0BYhrXfVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgw0BAQEBAXd2EAeFSJ8BgjeQM4QTKYQfgVoCggEHQhEBAQEBAQE?= =?us-ascii?q?BAQEBARIBAQEICwsJHTCCMwQBFQWCFgEBAQMBEhEEGQEbEgsBAwELBgULDQ0dA?= =?us-ascii?q?gIhAQERAQUBChIGExIQiDABAw8IDp06gTI/MotQgWwYBQEfgw0Fg2AKGScDClS?= =?us-ascii?q?DNAEBAQEBAQEDAQEBAQEBARgCBhKGLIRbgkiCLoIfOIJdBYcNDIhcijQ1gXiEU?= =?us-ascii?q?4Zog12CQo10iUaENIJIEx6BEw8lgRlEEYJtLCCCBiA0AQGHcoFPAQEB?= X-IPAS-Result: =?us-ascii?q?A0B9AAC+N0BYhrXfVdFdHAEBBAEBCgEBFwEBBAEBCgEBgw0?= =?us-ascii?q?BAQEBAXd2EAeFSJ8BgjeQM4QTKYQfgVoCggEHQhEBAQEBAQEBAQEBARIBAQEIC?= =?us-ascii?q?wsJHTCCMwQBFQWCFgEBAQMBEhEEGQEbEgsBAwELBgULDQ0dAgIhAQERAQUBChI?= =?us-ascii?q?GExIQiDABAw8IDp06gTI/MotQgWwYBQEfgw0Fg2AKGScDClSDNAEBAQEBAQEDA?= =?us-ascii?q?QEBAQEBARgCBhKGLIRbgkiCLoIfOIJdBYcNDIhcijQ1gXiEU4Zog12CQo10iUa?= =?us-ascii?q?ENIJIEx6BEw8lgRlEEYJtLCCCBiA0AQGHcoFPAQEB?= X-IronPort-AV: E=Sophos;i="5.33,282,1477954800"; d="scan'208,217";a="247666155" Received: from mail-io0-f181.google.com ([209.85.223.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 01 Dec 2016 15:51:38 +0100 Received: by mail-io0-f181.google.com with SMTP id m5so289181087ioe.3 for ; Thu, 01 Dec 2016 06:51:38 -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; bh=q/I4ZmLlyo9F+uMXNOxKJfaNLKdJ0uwILLjoTNjwy2A=; b=yd+ofLOprFH2HLI/CZGjrcPmOFspUKpO9+OknPIls84EMV5bQ+phYcmqjIUA7Wt3sW jpjuwGeoPl5bmlXdp1URBtQ7z4efQvcWXRc3qoHa0o9rU021GVW12TbMHeOz1Rqn0QDn aHKkoqAaCX9sO7ajiCRbERVvN9TyHn+/vW1TzxkVh06V8HDTjCsznA3YAgalMTmxSJU3 jnJZFBK7t4cetLVFjCD7HogIcVH6czriz22Xupxq/si6K1NWggF9eian2vPKBOmgYWuY KQKiBAjEcNk+xdywJxiX3fhxR5/+08QvDvWAOiuQEFQxEA3uMSNt+TR8O7XQz0IqtGx3 CyUA== 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:to:cc; bh=q/I4ZmLlyo9F+uMXNOxKJfaNLKdJ0uwILLjoTNjwy2A=; b=iYJIChR5LqYwZbMOg2PecC69MtAHs6PLLl3RdyIqdrIjD7mnJXqhwkA/fRR8civQSh oR9d3KVh4SXgxEg+sCX0DefWddjVDzMOrynrq27n6xr+YridplRWi80GaEOz2+O+O6RH eYZi1U1lerNCQ2n1cMgrgr6RIMoSGC76tIeI4bRF1udRueoqEJGZ21Vd5W0SJTSwFgvo c7LhU198UopeV1f6bUGcHBsLuLx6c/LaVeb1qgHpyC38qONZaw3ZZITAORkss344DPsm t/0svb728OmPGpmT9MqGdw3MlhSgeZesJzBLewCssXie94J84bhii1zun57M/1NbyY1H kAfQ== X-Gm-Message-State: AKaTC02WuntlHPkbhW4mxGDEvuZPH4cmfHdwjtKFYy3UzJc0PFneVMbhrrsucHbJ8r3nE3RbYSrMRZNbVqtmdg== X-Received: by 10.36.14.84 with SMTP id 81mr33733787ite.54.1480603896995; Thu, 01 Dec 2016 06:51:36 -0800 (PST) MIME-Version: 1.0 Received: by 10.79.140.146 with HTTP; Thu, 1 Dec 2016 06:50:56 -0800 (PST) In-Reply-To: References: <3f89d13a-14f0-090b-be96-d3f67fcb95f3@lexifi.com> From: Gabriel Scherer Date: Thu, 1 Dec 2016 09:50:56 -0500 Message-ID: To: Dmitry Bely Cc: Caml List Content-Type: multipart/alternative; boundary=001a1143e56a5565b7054299f577 Subject: Re: [Caml-list] GADT memory representation --001a1143e56a5565b7054299f577 Content-Type: text/plain; charset=UTF-8 The type you want to give to this `get` function is problematic as it says that for any 'a it can produce a value of type ('a gadt). In particular I can create a (char gadt), and then use the fact that the type-checker knows that no such value exist to break the type soundness of OCaml -- cast any type to any other type. I think you should try to get more familiar with how to manipulate GADT values from the OCaml side (in particular the need for "existential packing") before defining potentially unsafe and unsound FFI primitives, as the OCaml type-checker is really helpful in knowing what should not be done. The question of how to express this kind of things safely (create GADT values whose GADT type parameter depends on a value determined only at runtime) is, justifiably, asked by anyone playing with GADTs for the first time. I think it would be very nice if we addressed it explicitly in the part of the manual discussing GADT: http://caml.inria.fr/pub/docs/manual-ocaml-4.04/extn.html#sec238 (We could then reuse the examples of existential packing in the part on existential types and error messages.) On Thu, Dec 1, 2016 at 9:32 AM, Dmitry Bely wrote: > On Thu, Dec 1, 2016 at 2:51 PM, 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. > > So if I need to return a GADT value for C code, what would be the best > (working) option? Oversimplifying the problem, is it possible to > implement the following safely w.r.t future runtime changes? > > type _ gadt = > | Int : int -> int gadt > | Float : float -> float gadt > > external get : unit -> 'a gadt = "get" > > - Dmitry Bely > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --001a1143e56a5565b7054299f577 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
The type you want to give to this `get` function= is problematic as it says that for any 'a it can produce a value of ty= pe ('a gadt). In particular I can create a (char gadt), and then use th= e fact that the type-checker knows that no such value exist to break the ty= pe soundness of OCaml -- cast any type to any other type.

I think yo= u should try to get more familiar with how to manipulate GADT values from t= he OCaml side (in particular the need for "existential packing") = before defining potentially unsafe and unsound FFI primitives, as the OCam= l type-checker is really helpful in knowing what should not be done.
The question of how to express this kind of things safely (create GA= DT values whose GADT type parameter depends on a value determined only at r= untime) is, justifiably, asked by anyone playing with GADTs for the first t= ime. I think it would be very nice if we addressed it explicitly in the par= t of the manual discussing GADT:

=C2=A0 http://caml.inria.fr/pub/d= ocs/manual-ocaml-4.04/extn.html#sec238

(We could then reus= e the examples of existential packing in the part on existential types and = error messages.)



On Thu, Dec 1,= 2016 at 9:32 AM, Dmitry Bely <dmitry.bely@gmail.com> wr= ote:
On Thu, Dec 1, 2016= at 2:51 PM, Alain Frisch <al= ain.frisch@lexifi.com> 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 th= eir memory
>>> representation? Is there any difference from ordinary sum type= s?
>>
>>
>> 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 s= ection
>>> "Interfacing C with OCaml".
>>
>>
>> That's worth a GPR/Mantis issue.
>
>
> I'm not sure we want to document the memory layout of GADTs.=C2=A0= I don't think
> there are concrete plans to do so, but it might be considered to chang= e the
> representation of GADTs so that they cannot be used to compare values = of
> different types with the polymorphic comparison function.=C2=A0 Today = you can
> write:
>
>=C2=A0 =C2=A0type t =3D E: 'a -> t
>
>=C2=A0 =C2=A0let () =3D assert(E 1 =3D E true)
>
> A similar "bad" behavior used to be available for exceptions= and this was
> "fixed" by changing their representation (their "slot&q= uot; now has object_tag
> and a (per process) unique id).=C2=A0 We might want to do the same for= GADTs (not
> an easy decision since it would add a lot of overhead) and for first-c= lass
> modules as well.

So if I need to return a GADT value for C code, what would be the be= st
(working) option? Oversimplifying the problem, is it possible to
implement the following safely w.r.t future runtime changes?

type _ gadt =3D
=C2=A0 =C2=A0 | Int : int -> int gadt
=C2=A0 =C2=A0 | Float : float -> float gadt

external get : unit -> 'a gadt =3D "get"

- Dmitry Bely

--
Caml-list mailing list.=C2=A0 Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

--001a1143e56a5565b7054299f577--