From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 0BB827ED11 for ; Tue, 20 Sep 2016 23:08:03 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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-io0-f176.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.176 as permitted sender) identity=mailfrom; client-ip=209.85.223.176; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io0-f176.google.com) identity=helo; client-ip=209.85.223.176; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-io0-f176.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AIj2u+RFMSB+ptRGPz9j3eZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ75oMywAkXT6L1XgUPTWs2DsrQf2rCQ6/irADZZqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZv?= =?us-ascii?q?IaytQ8iJ3p7xj7j5oseKKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP?= =?us-ascii?q?5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+kjLK?= =?us-ascii?q?SA/HwnoHTi1CmRNNB03B7Qrmdpb3qCrz8ORnjnq0J8rzGJU9Qze/9O9OTwP0jG?= =?us-ascii?q?9TMjcj83zMzMl3kL5fiB2krh17hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkEW9vk?= =?us-ascii?q?Yg=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AqAQDTo+FXf7DfVdFdHAEBBAEBCgEBG?= =?us-ascii?q?AEFAQsBgxABAQEBAXV8B7huggQghX4CgVsHORMBAQEBAQEBAQEBARIBAQkLCwk?= =?us-ascii?q?XMYIyBAEVAQSCEAEBAQMBEhEEGQEUBx4DDAYDAgsNAgImAgIhAQERAQUBHAYTI?= =?us-ascii?q?ogNAQMPCA6THY9HgTI+Mos9gWuCXwWEAQoZJw1Ugl0BAQEHAQEBAQEaAgYQdoU?= =?us-ascii?q?xhFSCR4FFOIMCgloFmTw1gWWEQYZGgnKBbk6NL4cCgVOED4I5Ex6BESABgz4NG?= =?us-ascii?q?4FsIjSFSV+BQAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0AqAQDTo+FXf7DfVdFdHAEBBAEBCgEBGAEFAQsBgxABAQE?= =?us-ascii?q?BAXV8B7huggQghX4CgVsHORMBAQEBAQEBAQEBARIBAQkLCwkXMYIyBAEVAQSCE?= =?us-ascii?q?AEBAQMBEhEEGQEUBx4DDAYDAgsNAgImAgIhAQERAQUBHAYTIogNAQMPCA6THY9?= =?us-ascii?q?HgTI+Mos9gWuCXwWEAQoZJw1Ugl0BAQEHAQEBAQEaAgYQdoUxhFSCR4FFOIMCg?= =?us-ascii?q?loFmTw1gWWEQYZGgnKBbk6NL4cCgVOED4I5Ex6BESABgz4NG4FsIjSFSV+BQAE?= =?us-ascii?q?BAQ?= X-IronPort-AV: E=Sophos;i="5.30,370,1470693600"; d="scan'208";a="194097897" Received: from mail-io0-f176.google.com ([209.85.223.176]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Sep 2016 23:08:01 +0200 Received: by mail-io0-f176.google.com with SMTP id m186so33227960ioa.2 for ; Tue, 20 Sep 2016 14:08:01 -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 :content-transfer-encoding; bh=vKHO800ZRUWysnE16gnX3Y6nSQYQ2oaGmoHGRZVhQC0=; b=M4reBhWe7oC8vUUftDVIvR3xy5vxdtdOlenJELN1pO5fgpqUYeseZRsZNCfRZhQUsF UywCr4Gu7jIZ7/VuWaKfv0eQWYHWdGh6pHBeFBD7dhFqcE/2JuHlKVlSoLYRam/3z5EJ ql3J/eAKGKZIhVr8puUIy4D+Iu5U1Fhec+/CTiYBlugbBlI9OLPQ5h9DmFzIQK1c/wRd uFVzULlFf8irrxuAtk2SjaVr9KZp0qVPEdIs3DYQXuxBV+0ipKnKzK/hNUcIjlU4xuAN G9smvbmKXnGfKk6qRLBHJvrfWP7MxnzfO1Ju7q+Lc/Epdb5K/zLi1zdjOtvyt5jyAiCG H2jA== 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:content-transfer-encoding; bh=vKHO800ZRUWysnE16gnX3Y6nSQYQ2oaGmoHGRZVhQC0=; b=Ner4p0yptInfNSlV8K7NW9HcjLfoFb1s4eJ/IMkYjVp1+WJ/H9Eqqsk1aFRPMhkNhh zXJXjVjCc6szUz4xYyNb6XRcJoSAhu+BqM6e8sCcmJsm85JInev9KWZB+4r1600g4ckg ArZpkSorMj0TkcDxN7rjIFflo1k23OfsFnqyLI+IJuF7rMvLEb7KrggZlICNrhKarCP8 aSgCbWDklL9TEoN6vJ5Ltpm+niCYsyQg5Imm0CxJKbWun33SZX8nXa+iLEVHSL4Sb//W XeJ6JjBdUyeafVXcm0RSnWpogJoKxAQPtOV8eJLBnCoSU4gmgB1kiuOppSFL9qTiZWVq uI8w== X-Gm-Message-State: AE9vXwP33tw0OqtFspY3xrfqHQXB7sYakJWYGQ7atu2l3FNjNPbLTeIlPfZ50Ic81CCrFLEyXtLdWE5F0heyCQ== X-Received: by 10.107.168.225 with SMTP id e94mr48392728ioj.111.1474405680176; Tue, 20 Sep 2016 14:08:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.131.219 with HTTP; Tue, 20 Sep 2016 14:07:59 -0700 (PDT) In-Reply-To: References: <2161155.JggR3X9ZFM@molnar> <2324346.DfHVUap7Qc@molnar> From: Markus Mottl Date: Tue, 20 Sep 2016 17:07:59 -0400 Message-ID: To: OCaml List Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Covariant GADTs Has the OCaml team ever considered implementing existentially quantified type variables for record fields? Having given it some superficial thought, I didn't see any obvious reason why it would be impossible, though it would be admittedly more difficult than the usual (universally quantified) polymorphic record fields. Existentially quantified type variables need a well-defined scope. It's easy to define this scope with GADTs and first class modules: it starts with a pattern match or when unpacking the module. But accessing a record field as such doesn't create a binding. This would require some care when establishing the scope. Maybe one could define the start as the topmost binding whose type depends on a given existential type as obtained through field accesses. Another issue: when accessing an immutable field twice, one could assign the same existential type to bindings of their values. But accessing a mutable field twice would require two distinct existential types, because intermittent changes to the field could substitute values of incompatible types. Maybe there are even more awkward things that I haven't thought about. Any thoughts? Regards, Markus On Mon, Sep 19, 2016 at 11:03 AM, Markus Mottl wro= te: > Ah, thanks a lot, I totally missed following the link. Yes, this > OCaml feature would solve this problem efficiently, too. I guess an > existentially quantified record field would look neater, but I'd be > happy enough with GPR#606 getting into the next release. > > Regards, > Markus > > On Mon, Sep 19, 2016 at 10:53 AM, Mikhail Mandrykin = wrote: >> On =D0=BF=D0=BE=D0=BD=D0=B5=D0=B4=D0=B5=D0=BB=D1=8C=D0=BD=D0=B8=D0=BA, 1= 9 =D1=81=D0=B5=D0=BD=D1=82=D1=8F=D0=B1=D1=80=D1=8F 2016 =D0=B3. 10:46:22 MS= K Markus Mottl wrote: >> >>> Thanks, Mikhail, that's the correct way to solve this problem from a >> >>> typing perspective. Sadly, this encoding using a separate GADT >> >>> containing a "Link" tag defeats the purpose of the idea, which was to >> >>> save indirections and the associated memory overhead. I wish it was >> >>> possible to introduce existentially quantified variables within >> >>> records without having to go through another GADT. >> >> >> >> In fact the purpose of GPR#606 (https://github.com/ocaml/ocaml/pull/606)= is >> to avoid the indirection e.g. >> >> type t =3D A of string [@@unboxed] >> >> let x =3D A "toto" >> >> assert (Obj.repr x =3D=3D Obj.repr (match x with A s -> s)) >> >> It is also said in the comment that: >> >> >> >> This is useful (for example): >> >> >> >> --... >> >> -- when using a single-constructor, single-field GADT to introduce an >> existential type >> >> >> >> This is merged into trunk and should appear in 4.04.0: (from CHANGES) >> >> - GPR#606: optimized representation for immutable records with a single >> >> field, and concrete types with a single constructor with a single argume= nt. >> >> This is triggered with a [@@unboxed] attribute on the type definition. >> >> (Damien Doligez) >> >> >> >> Regards, Mikhail >> >> >> >>> >> >>> Regards, >> >>> Markus >> >>> >> >>> On Mon, Sep 19, 2016 at 6:18 AM, Mikhail Mandrykin >>> wrote: >> >>> > Hello, >> >>> > >> >>> > On =D0=BF=D0=BE=D0=BD=D0=B5=D0=B4=D0=B5=D0=BB=D1=8C=D0=BD=D0=B8=D0=BA= , 19 =D1=81=D0=B5=D0=BD=D1=82=D1=8F=D0=B1=D1=80=D1=8F 2016 =D0=B3. 10:58:29= MSK you wrote: >> >>> >> Hi Markus, >> >>> >> >> >>> >> >> >>> >> >> >>> >> Therefore, these fields are neither readable nor writable directly. A >> >>> >> >> >>> >> direct manifestation of the problem is that, as you observed, you >>> >> cannot >> >>> >> >> >>> >> assign new values to either prev or next without use of `Obj.magic`. >>> >> For >> >>> >> >> >>> >> instance, >> >>> > >> >>> > As far as I know quite common approach in this case is introduction of >> >>> > one-constructor wrapper types to hide the existential variable and al= low >> >>> > mutability e.g. >> >>> > >> >>> > >> >>> > >> >>> > type ('el, _) t =3D >> >>> > >> >>> > | Empty : ('el, [ `empty ]) t >> >>> > | >> >>> > | Elt : { >> >>> > >> >>> > mutable prev : 'el link; >> >>> > >> >>> > el : 'el; >> >>> > >> >>> > mutable next : 'el link; >> >>> > >> >>> > } -> ('el, [ `elt ]) t >> >>> > >> >>> > and 'el link =3D Link : ('el, _) t -> 'el link;; >> >>> > >> >>> > >> >>> > >> >>> > So the link type wraps the type parameter of the next element and thus >> >>> > allows safe mutation, otherwise it's only possible to update the field >> >>> > with >> >>> > the element of exactly same type that doesn't allow e.g. deleting an >> >>> > element at the end of the list without reallocating the corresponding >> >>> > record of the previous element (and if one decides to keep more preci= se >> >>> > information e.g. about the number of elements, the whole list needs to >>> > be >> >>> > re-allocated). With the link wrapper as above it's possible to define >> >>> > add, remove and also a get operation without and extra pattern matchi= ng: >> >>> > >> >>> > >> >>> > >> >>> > let add : type a. _ -> (_, a) t -> (_, [`elt]) t =3D fun el -> >> >>> > >> >>> > function >> >>> > >> >>> > | Empty -> Elt { el; prev =3D Link Empty; next =3D Link Empty } >> >>> > | >> >>> > | Elt _ as n -> Elt { el; prev =3D Link Empty; next =3D Link n };; >> >>> > >> >>> > let remove : type a. ('el, a) t -> 'el link =3D >> >>> > >> >>> > function >> >>> > >> >>> > | Empty -> Link Empty >> >>> > | >> >>> > | Elt { prev =3D Link p as prev; next =3D Link n as next} -> >> >>> > >> >>> > (match p with Empty -> () | Elt p -> p.next <- next); >> >>> > >> >>> > (match n with Empty -> () | Elt n -> n.prev <- prev); >> >>> > >> >>> > next;; >> >>> > >> >>> > >> >>> > >> >>> > let get : (_, [`elt]) t -> _ =3D function Elt { el; _ } -> el >> >>> > >> >>> > >> >>> > >> >>> > Also note the GPR#606(https://github.com/ocaml/ocaml/pull/606 ) that >> >>> > should >> >>> > allow constructing and deconstructing links (Link l) without overhead. >> >>> > >> >>> > >> >>> > >> >>> > Regards, Mikhail >> >>> > >> >>> > >> >>> > >> >>> > >> >>> > >> >>> > >> >>> > >> >>> > -- >> >>> > >> >>> > Mikhail Mandrykin >> >>> > >> >>> > Linux Verification Center, ISPRAS >> >>> > >> >>> > web: http://linuxtesting.org >> >>> > >> >>> > e-mail: mandrykin@ispras.ru >> >> >> >> >> >> -- >> >> Mikhail Mandrykin >> >> Linux Verification Center, ISPRAS >> >> web: http://linuxtesting.org >> >> e-mail: mandrykin@ispras.ru > > > > -- > Markus Mottl http://www.ocaml.info markus.mottl@gmail.com --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com