Re: [Caml-list] GADT memory representation

[Gabriel Scherer <gabriel.scherer@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3183 bytes --]

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 <dmitry.bely@gmail.com> wrote:

> On Thu, Dec 1, 2016 at 2:51 PM, Alain Frisch <alain.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 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
>

[-- Attachment #2: Type: text/html, Size: 4582 bytes --]