Re: [Caml-list] Covariant GADTs

[Goswin von Brederlow <goswin-v-b@web.de>]

On Sun, Sep 18, 2016 at 09:52:24PM -0400, Markus Mottl wrote:
> 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

I think here you are trying to encode into the type system if the
next/prev point to Empty or Elt. But you don't encode this information
into the resulting type at all.  How will you know the type of prev/next
from an Elt? 

Problem is that you then need to do that recursively. You not only
need to know if next is Empty or Elt but how many Elt there are before
you hit Empty and in both directions. E.g.

    ('el, [`elt] -> [`empty], [`elt] -> [`elt] -> [`empty]) t

Also inserting into the list would change the type of every item in
the list. Since some other item could be stored somewhere it's type
would change and we can't have that. That would rule out using
mutables and you would have to copy the whole list on every change.

Seems to me like you are on a dead end here.

>   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

MfG
	Goswin