Re: [Caml-list] Covariant GADTs

[Yaron Minsky <yminsky@janestreet.com>]

This looks like a nice improvement. A PR would be very welcome...

y

On Thu, Sep 22, 2016 at 9:39 AM, Markus Mottl <markus.mottl@gmail.com> wrote:
> The direct comparison with the Jane Street implementation showed a 40%
> speed increase for some random things I tried, but that's not a fair
> comparison.  If I improve the JS code, e.g. to avoid allocations, the
> performance improvement due to the GADT + inlined records drops to
> only about 10%.
>
> In terms of memory, a freshly created set costs 7 machine words in the
> original code vs. 5 for the GADT.  Adding one rank costs 4 machine
> words in the standard implementation vs. only 2 for GADTs.  That's a
> pretty significant size reduction.  The GADT representation would
> surely help in programs that allocate a lot of these values, but the
> values don't tend to grow much internally due to the tree compression
> algorithm.  I'm sure there are better examples where a program would
> typically allocate GADT-based data structures of more significant
> size.
>
> Regards,
> Markus
>
> On Wed, Sep 21, 2016 at 5:40 PM, Gabriel Scherer
> <gabriel.scherer@gmail.com> wrote:
>> 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
>>
>>
>
>
>
> --
> 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