RE: [Caml-list] GADT memory representation

[David Allsopp <dra-news@metastack.com>]

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.

Surely we never want the situation where any kind of OCaml value is at least officially inaccessible from the C side? Does that officially exist elsewhere in the runtime?

There are various cases where the GADT soundness can allow the C bindings to rely on type safety, for example:

type hive = _

type 'a value =  
| REG_SZ : string value
| REG_DWORD : int32 value

external writeWindowsRegistry : hive -> key:string -> value:string -> 'a value -> 'a -> unit

is much easier to implement both on the C and OCaml sides with a GADT than the undecorated:

external writeWindowsRegistry : hive -> key:string -> value:string -> value -> 'a -> unit

where either the C or OCaml side must ensure that the data parameter has a type corresponding to the constructor.

> 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.

Indeed it will be nice to get rid of it - though I think that losing the equivalence between GADT and regular sum type would be a shame.


David