From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 CFB637ED11 for ; Wed, 21 Sep 2016 19:04:04 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=markus.mottl@gmail.com; spf=Pass smtp.mailfrom=markus.mottl@gmail.com; spf=None smtp.helo=postmaster@mail-it0-f42.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.214.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.214.42 as permitted sender) identity=mailfrom; client-ip=209.85.214.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@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-it0-f42.google.com) identity=helo; client-ip=209.85.214.42; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-it0-f42.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AQtgi+Bz3EpaUxm/XCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0esQIJqq85mqBkHD//Il1AaPBtSBraoewLOO6OigATVGusnR9ihaMdRlbFwst4?= =?us-ascii?q?Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVIm?= =?us-ascii?q?bsy8IIPZjty22uau4NWTJlwQ3HvuKY91eTGrrgzKpIEtnYJsK6AwwxiB9n9VeP?= =?us-ascii?q?9KzG1pDV2Wlhf4oMy3+cgw3T5XvqcE/tRDTL6yWqMkUbgQWDEvKWMo/4vusgXf?= =?us-ascii?q?SSOA43IdViMdlR8eUFuN1w3zQpqk6niyjeF6wiTPeJSuFb0=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A+AQBmvOJXfyrWVdFeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgxABAQEBATw5bQ8HuG+CBByGAgKBXQc6EgEBAQEBAQEBAQEBEgE?= =?us-ascii?q?BCQsLCRcxgjIEARUBBIIRAQEEEhEEGQEUBx0BAwwGBQsDCgICJgICIQEBEQEFA?= =?us-ascii?q?RwGExsHiA4BAxegX4EyPjKLPYFrgl8Fg3YKGScNVIJeAQEBAQEFAQEBAQEaAgY?= =?us-ascii?q?QdoUxhFSCR4UBgloBBIg2kQo1gWWLCYJ0j2yIWIQPgjoTHoERJQaDNIIWIjSFB?= =?us-ascii?q?YFAAQEB?= X-IPAS-Result: =?us-ascii?q?A0A+AQBmvOJXfyrWVdFeHAEBBAEBCgEBFwEBBAEBCgEBgxA?= =?us-ascii?q?BAQEBATw5bQ8HuG+CBByGAgKBXQc6EgEBAQEBAQEBAQEBEgEBCQsLCRcxgjIEA?= =?us-ascii?q?RUBBIIRAQEEEhEEGQEUBx0BAwwGBQsDCgICJgICIQEBEQEFARwGExsHiA4BAxe?= =?us-ascii?q?gX4EyPjKLPYFrgl8Fg3YKGScNVIJeAQEBAQEFAQEBAQEaAgYQdoUxhFSCR4UBg?= =?us-ascii?q?loBBIg2kQo1gWWLCYJ0j2yIWIQPgjoTHoERJQaDNIIWIjSFBYFAAQEB?= X-IronPort-AV: E=Sophos;i="5.30,374,1470693600"; d="scan'208";a="237756839" Received: from mail-it0-f42.google.com ([209.85.214.42]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Sep 2016 19:04:03 +0200 Received: by mail-it0-f42.google.com with SMTP id 186so56780525itf.0 for ; Wed, 21 Sep 2016 10:04:03 -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=Zm7MDhbdO3eDDRgV0oaR9ZMWBj44UlqYUpnQ2hS4A8U=; b=nRuhKTxdztth9M1EhRbhHGkaLpN50iXkDsDDm9lHwBDv1lZSgHINqdGGSdrPchUP4Z HyBle5rQbuNeYkPw8o4FKDtizVqLsINPhUpegJ1LJGU2sr0T6iigSjPJ29CaV8Ten5/G cHzG0UMUBWa2+U32HIs87RyV01ZOtvepNLjTonAwc3OMx6qpirt0AAN02NNKVBlBqLgn 32KgEk5tHEO125tsb0In4bTJTuYBfWh5aZjqBbq+/msSwJTxUTBBLtmmM4MZAtvNPlNb CUtlExpaqzZ0Hgg9KcKVRBVEdhOMQ4VM+683OBSJFw7HE3nn7pFukEIqUNXo6MlyPC2v P1cA== 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=Zm7MDhbdO3eDDRgV0oaR9ZMWBj44UlqYUpnQ2hS4A8U=; b=lU773Ikd/TV07C4zj0moV5CCo8oDnV5noF9sXAquVR2fZjJkP/wUV+bgsQTxAexCFA acXQwLfmWscuW48LKnzePmBC+FS2Ehl8AgPO28FraPSAA9hsf8JFiHHWDrmH1lFJGAAf tdY+3wJNFoLR0mkKjp/dSMj9J3ljO55PxhcpBQrppAjZxIftZw4vlHoFfisJzO25hQXK zsFakdw1ORnkxuDek+NsHFgvPrjI7+vdoZDsMNkPO2U+NMjuSXWpttVi2mQ/bJnStS48 erG7m/3rPcskl46mVPJ+ZKN4aV/SEbdaU/l2ExpuRkjy3gfycEr3VbdAMm9JiaakT8fB Fu4A== X-Gm-Message-State: AE9vXwOlfjvNxcTVh2b5oIdzB+/nlPtgxnNniU8Bnf34YkqSW2MccXad8Q3qxO70pMDw+9/4h1/TMUHLuzjz7g== X-Received: by 10.36.13.5 with SMTP id 5mr5377076itx.79.1474477442803; Wed, 21 Sep 2016 10:04:02 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Wed, 21 Sep 2016 10:04:01 -0700 (PDT) In-Reply-To: References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> From: Markus Mottl Date: Wed, 21 Sep 2016 13:04:01 -0400 Message-ID: To: Lukasz Stafiniak Cc: OCaml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Covariant GADTs 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