Re: [Caml-list] Covariant GADTs

[Mikhail Mandrykin <mandrykin@ispras.ru>]

[-- Attachment #1: Type: text/plain, Size: 2247 bytes --]

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

--------
[1] https://github.com/ocaml/ocaml/pull/606

[-- Attachment #2: Type: text/html, Size: 9761 bytes --]