Re: [Caml-list] Covariant GADTs

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

Hi Octachron,

yes, indeed, that was spot on.  I somehow got sidetracked by the lack
of covariance annotations for GADTs, not realizing that the implicitly
defined type variables 'prev and 'next are existential within the
scope of Elt only.  Anything outside can't be a witness so I can't
write, and anything inside can't get out without escaping scope.

I guess what I would need to solve my problem efficiently are record
fields that support existentially rather than only universally
quantified variables.  Something along the lines of:

  | Elt : { mutable prev : $'kind. ('el, 'kind) t }

Would that make sense?

Btw., the "option" type was only introduced so as not having to reveal
the type representation to users of the API.  The "Some" tag would
typically be dropped right after the user pattern matches on the
option type.  They would then still benefit from the efficient
representation of the link, and the GADT + inlined record would still
be able to save the memory overhead associated with the indirection to
a non-inlined record.

Regards,
Markus

On Mon, Sep 19, 2016 at 4:58 AM, octachron <octa@polychoron.fr> wrote:
> Hi Markus,
>
>> Taking an element link can be done without
>> having to introduce superfluous pattern matches, because the GADT
>> guarantees via the type system that a link is non-empty.
>
>
> I fear that you are misinterpreting the guarantees giving to you by the type
> ('el, 'kind) Link.t. This type can be rewritten as
>
>   type ('el, _) t =
>     | Empty : ('el, [ `empty ]) t
>     | Elt : {
>         mutable prev : ('el, [< kind ] as 'prev ) t;
>         el : 'el;
>         mutable next : ('el, [< kind ] as 'next ) t;
>       } -> ('el, [ `elt ]) t
>
> Notice the existential types 'prev and 'next within the Elt constructor:
> they mean that outside of the context of Elt, the type system simply does
> not know the subtype of the prev and next fields. Even within the context of
> the `Elt` constructor, the type system only knows that there exists two
> types p and n such that Elt r is typed Elt {prev:p;next:n;el:el}. But the
> information about which precise type was present when constructing the value
> is lost.
>
> 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,
>
> let set_next (Elt r) x = r.next <- x;;
>
> fails with
>
> Error: This expression has type 'a but an expression was expected of type
> ('b, [< kind ]) t. The type constructor $Elt_'next would escape its scope.
>
> because the type checker tries to unify the type 'a of x with the
> existential type $Elt_'next of `next`. Using a fantasy syntax, we have
>
> let set_next (type a) (Elt (type p n) {next:n; prev:p; _} ) (x:a) = r.next:p
> <- x:a;;
>
> and the types `a` and `p` cannot be unified because `p` should not escape
> the context of the constructor Elt.
>
> Consequently writing `set_next` requires to use Obj.magic:
>
> let set_next (Elt r) x = r.next <- Obj.magic x;;
>
> This use of Obj.magic should be fine, since it is impossible to access the
> field prev and next directly. Contrarily, your coerce function is unsafe:
>
> let current (Elt {el;_}) = el
> let crash () = current (coerce @@ Empty)
>
> On the other side of the problem, this is the reason why you need to wrap
> access with an option in `get_opt_next`. Note that I am not certain that
> this wrapping does not completely defeat your optimisation objective.
>
> Regards − octachron.
>
>
> Le 09/19/16 à 03:52, Markus Mottl a écrit :
>
>> Hi Petter,
>>
>> thanks, the above approach obviously works with my previous example,
>> which I had sadly oversimplified.  In my case I was actually dealing
>> with inlined, mutable records where the above won't work, because then
>> I can't overwrite fields.  The somewhat more complete example also
>> contains strange type system behavior I don't understand that may even
>> be a bug.
>>
>> The example below shows how GADTs + inline records + (if available)
>> covariance could help implement doubly linked lists much more
>> efficiently.  The memory representation using mutable inline records
>> is essentially optimal.  Taking an element link can be done without
>> having to introduce superfluous pattern matches, because the GADT
>> guarantees via the type system that a link is non-empty.
>>
>> I had to use "Obj.magic" due to the lack of covariance support with
>> GADTs in the "coerce" function, which I believe to be sound.
>>
>> The strange behavior is in the "insert_first" function and also the
>> "create" function: "Empty" is not of covariant type, but nevertheless
>> can be used for allocation in that way (e.g. in the "let res = ..."
>> part).  But the commented out lines show that I cannot overwrite the
>> exact same field in the just allocated value with the exact same
>> value.  I can understand the reason why the latter is not possible,
>> but why is allocation allowed that way?  Maybe a type system guru can
>> explain what's going on.
>>
>> ----------
>> module Link = struct
>>    type kind = [ `empty | `elt ]
>>
>>    type ('el, _) t =
>>      | Empty : ('el, [ `empty ]) t
>>      | Elt : {
>>          mutable prev : ('el, [< kind ]) t;
>>          el : 'el;
>>          mutable next : ('el, [< kind ]) t;
>>        } -> ('el, [ `elt ]) t
>>
>>    let coerce (t : ('el, [< kind ]) t) : ('el, [< kind ]) t = Obj.magic t
>>
>>    let get_opt_elt : type a. ('el, a) t -> ('el, [ `elt ]) t option =
>> function
>>      | Empty -> None
>>      | Elt _ as elt -> Some elt
>>
>>    let cut : type a. ('el, a) t -> unit = function
>>      | Empty -> ()
>>      | Elt { prev = prev_elt; next = next_elt } ->
>>          match prev_elt, next_elt with
>>          | Empty, Empty -> ()
>>          | Empty, Elt next -> next.prev <- coerce Empty
>>          | Elt prev, Empty -> prev.next <- coerce Empty
>>          | Elt prev, Elt next ->
>>              prev.next <- coerce next_elt;
>>              next.prev <- coerce prev_elt
>> end  (* Link *)
>>
>> module Doubly_linked : sig
>>    type 'el t
>>    type 'el elt
>>
>>    val create : unit -> 'el t
>>    val first : 'el t -> 'el elt option
>>    val insert_first : 'el t -> 'el -> unit
>>    val remove : 'el elt -> unit
>> end = struct
>>    open Link
>>
>>    type 'el t = Head : { mutable head : ('el, [< Link.kind ]) Link.t } ->
>> 'el t
>>    type 'el elt = ('el, [ `elt ]) Link.t
>>
>>    let create () = Head { head = Empty }
>>
>>    let first (Head h) = Link.get_opt_elt h.head
>>
>>    let insert_first (Head h) el =
>>      h.head <-
>>        match h.head with
>>        | Empty ->
>>            let res = Elt { prev = Empty; el; next = Empty } in
>>            (* let Elt foo = res in *)
>>            (* foo.prev <- Empty; *)
>>            coerce res
>>        | Elt _ as next -> coerce (Elt { prev = Empty; el; next })
>>
>>    let remove = Link.cut
>> end  (* Doubly_linked *)
>> ----------
>>
>> Regards,
>> Markus
>>
>>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs



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