[Caml-list] GADT memory representation

[Caml-list] GADT memory representation

[Dmitry Bely]

I need to access/modify GADT data from C glue code. What is their
memory representation? Is there any difference from ordinary sum
types? Unfortunately OCaml manual doesn't even mention GADTs in
section "Interfacing C with OCaml".

- Dmitry Bely

RE: [Caml-list] GADT memory representation

[David Allsopp]

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.


David 

Re: [Caml-list] GADT memory representation

[Dmitry Bely]

On Thu, Dec 1, 2016 at 12:52 PM, David Allsopp <dra-news@metastack.com> 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

Re: [Caml-list] GADT memory representation

[Alain Frisch]

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

Re: [Caml-list] GADT memory representation

[octachron]

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
>

Re: [Caml-list] GADT memory representation

[Dmitry Bely]

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

Re: [Caml-list] GADT memory representation

[Gabriel Scherer]

[-- 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 --]

Re: [Caml-list] GADT memory representation

[Josh Berdine]

On Thu, Dec 01 2016, 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.

FWIW, I would rather polymorphic comparison were removed than GADT's made heavier.

RE: [Caml-list] GADT memory representation

[David Allsopp]

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