Re: [Caml-list] Covariant GADTs

[octachron <octa@polychoron.fr>]

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
>
>