Re: [Caml-list] Covariant GADTs

[Gabriel Scherer <gabriel.scherer@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4519 bytes --]

Very nice. Would you have more precise numbers for the "considerably more
efficient" part? It's not always easy to find clear benefits to inline
records on representative macro-benchmarks.

On Thu, Sep 22, 2016 at 2:04 AM, Markus Mottl <markus.mottl@gmail.com>
wrote:

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

[-- Attachment #2: Type: text/html, Size: 6151 bytes --]