Re: [Caml-list] Covariant GADTs

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

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

On Sun, Sep 18, 2016 at 4:17 AM, Petter A. Urkedal <paurkedal@gmail.com> wrote:
> Hi Markus,
>
> On 17 September 2016 at 19:38, Markus Mottl <markus.mottl@gmail.com> wrote:
>> Hi,
>>
>> GADTs currently do not allow for variance annotations so I wondered
>> whether there are any workarounds for what I want:
>>
>> -----
>> type +_ t =
>>   | Z : [ `z ] t
>>   | S : [ `z | `s ] t -> [ `s ] t
>>
>> let get_next (s : [ `s ] t) =
>>   match s with
>>   | S next -> next
>> -----
>>
>> The above compiles without the variance annotation, but then you
>> cannot express "S Z", because there is no way to coerce Z to be of
>> type [`z | `s] t.
>>
>> Another approach I tried is the following:
>>
>> -----
>> type _ t =
>>   | Z : [ `z ] t
>>   | S : [< `z | `s ] t -> [ `s ] t
>>
>> let get_next (s : [ `s ] t) : [< `z | `s ] t =
>>   match s with
>>   | S next -> next
>> -----
>>
>> The above gives the confusing error:
>>
>> -----
>> Error: This expression has type [< `s | `z ] t
>>        but an expression was expected of type [< `s | `z ] t
>>        The type constructor $S would escape its scope
>> -----
>>
>> There are apparently two type variables associated with [< `s | `z ]
>> t: the locally existential one introduced by matching the GADT, and
>> the one in the type restriction of the function, but the compiler
>> cannot figure out that these can be safely unified.  There is
>> currently no way of specifying locally abstract types that have type
>> constraints, which could possibly also help here.
>
> In this case, you can supply the needed type information to `get_next`
> with structural type matching:
>
>   type _ t = Z : [`z] t | S : 'a t -> [`s of 'a] t
>   let get_next : [`s of 'a] t -> 'a t = function S next -> next
>
> This gives you a richer type which also allows defining get_next_pair, etc.
>
>> Are there workarounds to achieve the above?  Are there any plans to
>> add variance annotations for GADTs?
>
> I had a similar problem myself and found a paper [1] explaining the
> issue and a possible solution.  Haven't really studied it, but as I
> understand the issue is that the current GADTs only introduce type
> equality, which is too strict to verify variance.  What is needed is
> more like (my ASCIIfication)
>
>   type +'a t =
>     | Z when 'a >= [`z]
>     | S when 'a >= [`s] of [< `z | `s] t
>
> allowing 'a in each case to be a supertype rather than equal to the
> specified type.  In that spirit, I tried
>
>   type +_ t =
>     | Z : [> `z] t
>     | S : [< `s | `z] t -> [> `s] t;;
>
> but that does not check for variance either.
>
> Best,
> Petter
>
> [1] https://arxiv.org/abs/1301.2903



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