Re: [Caml-list] Covariant GADTs

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

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.

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



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