Re: [Caml-list] Covariant GADTs

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

Here is a complete working example of the advantages of using GADTs
with inline records.  It also uses the [@@unboxed] feature now
available with OCaml 4.04 as discussed before here, though it required
a little workaround due to an apparent bug in the current beta.

The below implementation of the union-find algorithm is considerably
more efficient (with the 4.04 beta only) than the Union_find
implementation in the Jane Street Core kernel.  The problem admittedly
lends itself to the GADT + inline record trick.

There is actually one advantage to using an intermediate, unboxed GADT
tag compared to records with existentially quantified fields (if they
were available): functions matching the tag don't require those
horrible type annotations for locally abstract types, because the
match automatically sets up the scope for you.  Having to write "Node
foo" instead of just "foo" in some places isn't too bad.  Not sure
it's possible to have the best of both worlds.

----------
module Union_find = struct
  (* This does not work yet due to an OCaml 4.04 beta bug
  type ('a, 'kind) tree =
    | Root : { mutable value : 'a; mutable rank : int } -> ('a, [ `root ]) tree
    | Inner : { mutable parent : 'a node } -> ('a, [ `inner ]) tree

  and 'a node = Node : ('a, _) tree -> 'a node  [@@ocaml.unboxed]

  type 'a t = ('a, [ `inner ]) tree
  *)

  type ('a, 'kind, 'parent) tree =
    | Root : { mutable value : 'a; mutable rank : int } ->
      ('a, [ `root ], 'parent) tree
    | Inner : { mutable parent : 'parent } -> ('a, [ `inner ], 'parent) tree

  type 'a node = Node : ('a, _, 'a node) tree -> 'a node  [@@ocaml.unboxed]

  type 'a t = ('a, [ `inner ], 'a node) tree

  let create v = Inner { parent = Node (Root { value = v; rank = 0 }) }

  let rec compress ~repr:(Inner inner as repr) = function
    | Node (Root _ as root) -> repr, root
    | Node (Inner next_inner as repr) ->
        let repr, _ as res = compress ~repr next_inner.parent in
        inner.parent <- Node repr;
        res

  let compress_inner (Inner inner as repr) = compress ~repr inner.parent

  let get_root (Inner inner) =
    match inner.parent with
    | Node (Root _ as root) -> root  (* Avoids compression call *)
    | Node (Inner _ as repr) ->
        let repr, root = compress_inner repr in
        inner.parent <- Node repr;
        root

  let get t = let Root r = get_root t in r.value

  let set t x = let Root r = get_root t in r.value <- x

  let same_class t1 t2 = get_root t1 == get_root t2

  let union t1 t2 =
    let Inner inner1 as repr1, (Root r1 as root1) = compress_inner t1 in
    let Inner inner2 as repr2, (Root r2 as root2) = compress_inner t2 in
    if root1 == root2 then ()
    else
      let n1 = r1.rank in
      let n2 = r2.rank in
      if n1 < n2 then inner1.parent <- Node repr2
      else begin
        inner2.parent <- Node repr1;
        if n1 = n2 then r1.rank <- r1.rank + 1
      end
end  (* Union_find *)
----------

Regards,
Markus

On Wed, Sep 21, 2016 at 6:14 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> On Wed, Sep 21, 2016 at 12:11 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
>>
>> A simple solution would be to "A-transform" (IIRC the term) accesses
>
> Sorry, I forgot to define this. I mean rewrite rules like:
> [f r.x] ==> [let x = r.x in f x]
> where subsequently the existential variable is introduced (unpacked)
> at the let-binding level. This corresponds to a single-variant GADT
> pattern match.
>
>> to fields with existential type variables. This would give a more
>> narrow scope on the expression level than you suggest, but a
>> well-defined one prior to type inference. To broaden the scope you
>> would need to let-bind the field access yourself at the appropriate
>> level.



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