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