Re: [Caml-list] Covariant GADTs

[Markus Mottl <markus.mottl@gmail.com>]

Ah, thanks a lot, I totally missed following the link.  Yes, this
OCaml feature would solve this problem efficiently, too.  I guess an
existentially quantified record field would look neater, but I'd be
happy enough with GPR#606 getting into the next release.

Regards,
Markus

On Mon, Sep 19, 2016 at 10:53 AM, Mikhail Mandrykin <mandrykin@ispras.ru> wrote:
> On понедельник, 19 сентября 2016 г. 10:46:22 MSK Markus Mottl wrote:
>
>> Thanks, Mikhail, that's the correct way to solve this problem from a
>
>> typing perspective. Sadly, this encoding using a separate GADT
>
>> containing a "Link" tag defeats the purpose of the idea, which was to
>
>> save indirections and the associated memory overhead. I wish it was
>
>> possible to introduce existentially quantified variables within
>
>> records without having to go through another GADT.
>
>
>
> In fact the purpose of GPR#606 (https://github.com/ocaml/ocaml/pull/606) is
> to avoid the indirection e.g.
>
> type t = A of string [@@unboxed]
>
> let x = A "toto"
>
> assert (Obj.repr x == Obj.repr (match x with A s -> s))
>
> It is also said in the comment that:
>
>
>
> This is useful (for example):
>
>
>
> --...
>
> -- when using a single-constructor, single-field GADT to introduce an
> existential type
>
>
>
> This is merged into trunk and should appear in 4.04.0: (from CHANGES)
>
> - GPR#606: optimized representation for immutable records with a single
>
> field, and concrete types with a single constructor with a single argument.
>
> This is triggered with a [@@unboxed] attribute on the type definition.
>
> (Damien Doligez)
>
>
>
> Regards, Mikhail
>
>
>
>>
>
>> Regards,
>
>> Markus
>
>>
>
>> On Mon, Sep 19, 2016 at 6:18 AM, Mikhail Mandrykin <mandrykin@ispras.ru>
>> wrote:
>
>> > Hello,
>
>> >
>
>> > On понедельник, 19 сентября 2016 г. 10:58:29 MSK you wrote:
>
>> >> Hi Markus,
>
>> >>
>
>> >>
>
>> >>
>
>> >> Therefore, these fields are neither readable nor writable directly. A
>
>> >>
>
>> >> direct manifestation of the problem is that, as you observed, you
>> >> cannot
>
>> >>
>
>> >> assign new values to either prev or next without use of `Obj.magic`.
>> >> For
>
>> >>
>
>> >> instance,
>
>> >
>
>> > As far as I know quite common approach in this case is introduction of
>
>> > one-constructor wrapper types to hide the existential variable and allow
>
>> > mutability e.g.
>
>> >
>
>> >
>
>> >
>
>> > type ('el, _) t =
>
>> >
>
>> > | Empty : ('el, [ `empty ]) t
>
>> > |
>
>> > | Elt : {
>
>> >
>
>> > mutable prev : 'el link;
>
>> >
>
>> > el : 'el;
>
>> >
>
>> > mutable next : 'el link;
>
>> >
>
>> > } -> ('el, [ `elt ]) t
>
>> >
>
>> > and 'el link = Link : ('el, _) t -> 'el link;;
>
>> >
>
>> >
>
>> >
>
>> > So the link type wraps the type parameter of the next element and thus
>
>> > allows safe mutation, otherwise it's only possible to update the field
>
>> > with
>
>> > the element of exactly same type that doesn't allow e.g. deleting an
>
>> > element at the end of the list without reallocating the corresponding
>
>> > record of the previous element (and if one decides to keep more precise
>
>> > information e.g. about the number of elements, the whole list needs to
>> > be
>
>> > re-allocated). With the link wrapper as above it's possible to define
>
>> > add, remove and also a get operation without and extra pattern matching:
>
>> >
>
>> >
>
>> >
>
>> > let add : type a. _ -> (_, a) t -> (_, [`elt]) t = fun el ->
>
>> >
>
>> > function
>
>> >
>
>> > | Empty -> Elt { el; prev = Link Empty; next = Link Empty }
>
>> > |
>
>> > | Elt _ as n -> Elt { el; prev = Link Empty; next = Link n };;
>
>> >
>
>> > let remove : type a. ('el, a) t -> 'el link =
>
>> >
>
>> > function
>
>> >
>
>> > | Empty -> Link Empty
>
>> > |
>
>> > | Elt { prev = Link p as prev; next = Link n as next} ->
>
>> >
>
>> > (match p with Empty -> () | Elt p -> p.next <- next);
>
>> >
>
>> > (match n with Empty -> () | Elt n -> n.prev <- prev);
>
>> >
>
>> > next;;
>
>> >
>
>> >
>
>> >
>
>> > let get : (_, [`elt]) t -> _ = function Elt { el; _ } -> el
>
>> >
>
>> >
>
>> >
>
>> > Also note the GPR#606(https://github.com/ocaml/ocaml/pull/606 ) that
>
>> > should
>
>> > allow constructing and deconstructing links (Link l) without overhead.
>
>> >
>
>> >
>
>> >
>
>> > Regards, Mikhail
>
>> >
>
>> >
>
>> >
>
>> >
>
>> >
>
>> >
>
>> >
>
>> > --
>
>> >
>
>> > Mikhail Mandrykin
>
>> >
>
>> > Linux Verification Center, ISPRAS
>
>> >
>
>> > web: http://linuxtesting.org
>
>> >
>
>> > e-mail: mandrykin@ispras.ru
>
>
>
>
>
> --
>
> Mikhail Mandrykin
>
> Linux Verification Center, ISPRAS
>
> web: http://linuxtesting.org
>
> e-mail: mandrykin@ispras.ru



-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com