Re: [Caml-list] Covariant GADTs

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

Has the OCaml team ever considered implementing existentially
quantified type variables for record fields?  Having given it some
superficial thought, I didn't see any obvious reason why it would be
impossible, though it would be admittedly more difficult than the
usual (universally quantified) polymorphic record fields.

Existentially quantified type variables need a well-defined scope.
It's easy to define this scope with GADTs and first class modules: it
starts with a pattern match or when unpacking the module.  But
accessing a record field as such doesn't create a binding.  This would
require some care when establishing the scope.  Maybe one could define
the start as the topmost binding whose type depends on a given
existential type as obtained through field accesses.

Another issue: when accessing an immutable field twice, one could
assign the same existential type to bindings of their values.  But
accessing a mutable field twice would require two distinct existential
types, because intermittent changes to the field could substitute
values of incompatible types.  Maybe there are even more awkward
things that I haven't thought about.

Any thoughts?

Regards,
Markus

On Mon, Sep 19, 2016 at 11:03 AM, Markus Mottl <markus.mottl@gmail.com> wrote:
> Ah, thanks a lot, I totally missed following the link.  Yes, this
> OCaml feature would solve this problem efficiently, too.  I guess an
> existentially quantified record field would look neater, but I'd be
> happy enough with GPR#606 getting into the next release.
>
> Regards,
> Markus
>
> On Mon, Sep 19, 2016 at 10:53 AM, Mikhail Mandrykin <mandrykin@ispras.ru> wrote:
>> 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
>
>
>
> --
> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com



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