Re: [Caml-list] Covariant GADTs

[Mikhail Mandrykin <mandrykin@ispras.ru>]

On понедельник, 19 сентября 2016 г. 13:18:19 MSK Mikhail Mandrykin 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;;
This is actually buggy (although typesafe), more like this:

let add : type a. _ -> (_, a) t -> (_, [`elt]) t = fun el ->
  function
  | Empty -> Elt { el; prev = Link Empty; next = Link Empty }
  | Elt ({ prev = Link p as prev; _ } as n) as next ->
    let r = Elt { el; prev; next = Link next } in
    (match p with Empty -> () | Elt p -> p.next <- Link r);
    n.prev <- Link r;
    r;;

let remove : type a. (_, a) t -> (_, a) t * _ =
  function
  | Empty -> Empty, Link Empty
  | Elt ({ prev = Link p as prev; next = Link n as next} as e) as elt ->
    (match p with Empty -> () | Elt p -> p.next <- next);
    (match n with Empty -> () | Elt n -> n.prev <- prev);
    e.next <- Link Empty;
    e.prev <- Link Empty;
    elt, next;;

Regards, Mikhail


-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru