From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 3FE687ED11 for ; Wed, 21 Sep 2016 23:42:42 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f177.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.177 as permitted sender) identity=mailfrom; client-ip=209.85.223.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f177.google.com) identity=helo; client-ip=209.85.223.177; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DbAABK/uJXhrHfVdFdGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBgzsBAQEBAXVtDwemfolxiAGCBCSFegKBXwc5EwECAQEBAQEBARMBAQE?= =?us-ascii?q?ICwsJGS+EYQEBAQMBEhEEGQEUBxILAQMBCwYDAgsNDR0CAiEBAREBBQEKEgYTE?= =?us-ascii?q?gkHiA4BAw8IDpJkj0eBMj4yiz2Ba4JfBYN7ChknAwpUgl4BAQEBAQUBAQEBAQE?= =?us-ascii?q?BARcCBhCGJ4RUgkeCKoJXgloFhmoMgUCGdIoWNYFlhEKGR4J0gjyNMIhYhA+CO?= =?us-ascii?q?hMegREPEQODESsfgWovNIZFAQEB?= X-IPAS-Result: =?us-ascii?q?A0DbAABK/uJXhrHfVdFdGgEBAQECAQEBAQgBAQEBgzsBAQE?= =?us-ascii?q?BAXVtDwemfolxiAGCBCSFegKBXwc5EwECAQEBAQEBARMBAQEICwsJGS+EYQEBA?= =?us-ascii?q?QMBEhEEGQEUBxILAQMBCwYDAgsNDR0CAiEBAREBBQEKEgYTEgkHiA4BAw8IDpJ?= =?us-ascii?q?kj0eBMj4yiz2Ba4JfBYN7ChknAwpUgl4BAQEBAQUBAQEBAQEBARcCBhCGJ4RUg?= =?us-ascii?q?keCKoJXgloFhmoMgUCGdIoWNYFlhEKGR4J0gjyNMIhYhA+COhMegREPEQODESs?= =?us-ascii?q?fgWovNIZFAQEB?= X-IronPort-AV: E=Sophos;i="5.30,375,1470693600"; d="scan'208,217";a="237775649" Received: from mail-io0-f177.google.com ([209.85.223.177]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Sep 2016 23:41:37 +0200 Received: by mail-io0-f177.google.com with SMTP id m79so67142995ioo.3 for ; Wed, 21 Sep 2016 14:41:37 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=OJoQuTFBRL0MO0HrnwxIjSprMLWstsshBY6A24GR9Rs=; b=qJiJcqWeyb6ZBTZzrZCySHpKBCnryS9HCHNR2cT8LLv0yI5XOu+JTamxLXU6l48Ril O34UdyAxqfw5lF6rasYVuuPgWLmuc3Q/21Ya6Av26QtxRNSJDGiPUySBXTM6an53ak80 p61+FSdY0M7xBUDSzMjCtTCGEbbA6aK1MUUbuq8y/CEH6cLLpTMit4LTPqLsL4ckSLAf ICSjasDIC+juj9LDDk3uIjIvboZB34K3jUq9fFkS8bIGmJEghUMkn9/ZlJ8Q5KSCw6vO I0nqHo8N0IlpLP7JDI4Gw34o0KprBUXmQ3/VMwnowNso9Ko6QBSJgVohUesHEQESbqkE dCwQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=OJoQuTFBRL0MO0HrnwxIjSprMLWstsshBY6A24GR9Rs=; b=TWbkC6sk27J1/iBEaAvLy2v/o5qLaeoPNN5pM9dCeq9qG+OqVvZcVvhFUD21ZeV1U/ OeNrgAtMFAbiEeKblIYSa1qxJcNTuZ8FeRWYD7giFELG0HgKWPl2RdefH0hCre0h0RJS Apf9e2tzuNug5oAuWMGMAg3vwLE4X1DJtHaL8hdxPAowHr3TYImJcHjUoPAKUTEBucZy Zis4YFREHGJ7h1o6iTVZ7x80+o2UDPKN4YCmdfuioPmgJgfu0UpWcG5W6KpAZbACuGGM 6PQ/uzwr4MOuUIm+9y3M8rO9VwCZvLMXNNP+mT/+Y80Rs/sLV2uE1sjEC7J++G2smL5B EUfw== X-Gm-Message-State: AE9vXwMB1Z6rNhr5VYnJpT5xyjEwBEm1IrHRN6NZWkaJbOkWfXNwezJCgZR0wvVQzTVjRQ8EwiFBJKrcUlua0A== X-Received: by 10.107.157.69 with SMTP id g66mr51558086ioe.108.1474494095856; Wed, 21 Sep 2016 14:41:35 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.28.17 with HTTP; Wed, 21 Sep 2016 14:40:55 -0700 (PDT) In-Reply-To: References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> From: Gabriel Scherer Date: Thu, 22 Sep 2016 06:40:55 +0900 Message-ID: To: Markus Mottl Cc: Lukasz Stafiniak , OCaml List Content-Type: multipart/alternative; boundary=001a1140c532ce9a04053d0b68a6 Subject: Re: [Caml-list] Covariant GADTs --001a1140c532ce9a04053d0b68a6 Content-Type: text/plain; charset=UTF-8 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 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 > wrote: > > On Wed, Sep 21, 2016 at 12:11 PM, Lukasz Stafiniak > 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 > --001a1140c532ce9a04053d0b68a6 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Very nice. Would you have more precise numbers for the &qu= ot;considerably more efficient" part? It's not always easy to find= clear benefits to inline records on representative macro-benchmarks.

On Thu, Sep 2= 2, 2016 at 2:04 AM, Markus Mottl <markus.mottl@gmail.com> wrote:
Here is a complete working exam= ple of the advantages of using GADTs
with inline records.=C2=A0 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.=C2=A0 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.=C2=A0 Having to write "= Node
foo" instead of just "foo" in some places isn't too bad.= =C2=A0 Not sure
it's possible to have the best of both worlds.

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

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

=C2=A0 type 'a t =3D ('a, [ `inner ]) tree
=C2=A0 *)

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

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

=C2=A0 type 'a t =3D ('a, [ `inner ], 'a node) tree

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

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

=C2=A0 let compress_inner (Inner inner as repr) =3D compress ~repr inner.pa= rent

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

=C2=A0 let get t =3D let Root r =3D get_root t in r.value

=C2=A0 let set t x =3D let Root r =3D get_root t in r.value <- x

=C2=A0 let same_class t1 t2 =3D get_root t1 =3D=3D get_root t2

=C2=A0 let union t1 t2 =3D
=C2=A0 =C2=A0 let Inner inner1 as repr1, (Root r1 as root1) =3D compress_in= ner t1 in
=C2=A0 =C2=A0 let Inner inner2 as repr2, (Root r2 as root2) =3D compress_in= ner t2 in
=C2=A0 =C2=A0 if root1 =3D=3D root2 then ()
=C2=A0 =C2=A0 else
=C2=A0 =C2=A0 =C2=A0 let n1 =3D r1.rank in
=C2=A0 =C2=A0 =C2=A0 let n2 =3D r2.rank in
=C2=A0 =C2=A0 =C2=A0 if n1 < n2 then inner1.parent <- Node repr2
=C2=A0 =C2=A0 =C2=A0 else begin
=C2=A0 =C2=A0 =C2=A0 =C2=A0 inner2.parent <- Node repr1;
=C2=A0 =C2=A0 =C2=A0 =C2=A0 if n1 =3D n2 then r1.rank <- r1.rank + 1
=C2=A0 =C2=A0 =C2=A0 end
end=C2=A0 (* 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 te= rm) accesses
>
> Sorry, I forgot to define this. I mean rewrite rules like:
> [f r.x] =3D=3D> [let x =3D 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<= br> >> 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 appropriat= e
>> level.



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

--
Caml-list mailing list.=C2=A0 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

--001a1140c532ce9a04053d0b68a6--