Re: [Caml-list] Covariant GADTs

[Mikhail Mandrykin <mandrykin@ispras.ru>]

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

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

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